Changeset 2414


Ignore:
Timestamp:
Oct 23, 2012, 2:43:58 PM (7 years ago)
Author:
mulligan
Message:

Added bib file, done a little bit of rearrangement.

Location:
Papers/polymorphic-variants-2012
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

    r2410 r2414  
    55\usepackage[english]{babel}
    66\usepackage[colorlinks]{hyperref}
     7\usepackage{listings}
    78\usepackage{microtype}
    89
     10\lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
     11        keywordstyle=\color{red}\bfseries,
     12        keywordstyle=[2]\color{blue},
     13        commentstyle=\color{green},
     14        stringstyle=\color{blue},
     15        showspaces=false,showstringspaces=false,
     16        xleftmargin=1em}
     17
     18\bibliographystyle{spphys}
    919
    1020\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
     
    4656\label{sect.polymorphic.variants}
    4757
    48 In this section we provide a self-contained \emph{pr\'ecis} of polymorphic variants.
    49 For a more complete summary, we refer the reader to Garrigue's publications on the subject~\cite{dpm: todo}.
     58In this section we will attempt to provide a self-contained \emph{pr\'ecis} of polymorphic variants for the unfamiliar reader.
     59Those readers who wish to survey a more complete introduction to the subject are referred to Garrigue's original publications on the subject matter~\cite{garrigue:programming:1998,garrigue:code:2000}.
    5060
    51 Most mainstream functional programming languages, such as OCaml and Haskell, have mechanisms for inductively defining types through the use of \emph{algebraic data types}.
    52 Each algebraic data type can be described as a sum-of-products, wherein we associate a fixed number of distinct \emph{constructors} to the type being introduced, all of whom expect a product of arguments.
    53 Inductive data, modelled as an algebraic data type, is built incrementally from the ground-up using the constructors of that type.
     61Most mainstream functional programming languages, such as OCaml and Haskell, have mechanisms for defining new inductive types from old through the use of algebraic data type definitions.
     62Each algebraic data type may be described as a sum-of-products.
     63The programmer provides a fixed number of distinct \emph{constructors} with each constructor expects a (potentially empty) product of arguments.
     64Values of a given inductive data type are built using a data type's constructors.
    5465Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism.
    5566
    56 Having built data using constructors, to complete the picture we now need some facility for picking said data apart.
    57 Functional languages employ \emph{pattern matching} for this task.
    58 Given any inhabitant of an inductive type, by the aforementioned sum-of-products property, we know that it must consist of some constructor of that type applied to various arguments.
     67Having built data from various combinations of constructors, to complete the picture we now need some facility for picking said data apart, in order to build functions that operate over that data.
     68Functional languages almost uniformly employ \emph{pattern matching} for this task.
     69Given any inhabitant of an algebraic data type, by the aforementioned sum-of-products property, we know that it must consist of some constructor applied to various arguments.
    5970Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type.
    6071
    6172The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages.
    62 Further, using pattern matching it is easy to define new functions that consume algebraic data---the set of operations that can be defined for any given algebraic type is unbounded.
    63 Unfortunately, when it comes to extending algebraic data types with new constructors these types are essentially `closed'.
    64 We cannot simply extend an algebraic type with a new constructor.
    65 We must introduce a new algebraic type with the additional constructor, lifting the old type---and any functions defined over it---into this type.
     73Furthermore, using pattern matching it is easy to define new functions that consume algebraic data---the set of operations that can be defined for any given algebraic type is practically without bound.
    6674
    67 Moving sideways, we can compare and contrast functional programming languages' use of algebraic data paired with pattern matching with the approach taken by object-oriented languages, or extending the root object.
     75Unfortunately, in practical programming, we often want to expand a previously defined algebraic data type, adding more constructors.
     76When it comes to extending algebraic data types with new constructors in this way, we hit a problem: these types are `closed'.
     77In order to circumvent this restriction, we must introduce a new algebraic type with the additional constructor, lifting the old type---and any functions defined over it---into this type.
     78
     79\begin{figure}[ht]
     80\begin{minipage}[b]{0.45\linewidth}
     81\begin{lstlisting}
     82data Term
     83  = Lit Int
     84  | Add Term Term
     85  | Mul Term Term
     86
     87evaluate :: Term -> Int
     88evaluate (Lit i)   = i
     89evaluate (Add l r) = evaluate l + evaluate r
     90evaluate (Mul l r) = evaluate l * evaluate r
     91\end{lstlisting}
     92\end{minipage}
     93\hspace{0.5cm}
     94\begin{minipage}[b]{0.45\linewidth}
     95\begin{lstlisting}
     96\end{lstlisting}
     97\end{minipage}
     98\label{fig.pattern-matching.vs.oop}
     99\caption{A simple language of integer arithmetic embedded as an algebraic data type and as a class hierarchy.}
     100\end{figure}
     101
     102We can compare and contrast functional programming languages' use of algebraic data and pattern matching with the approach taken by object-oriented languages (see Figure~\ref{fig.pattern-matching.vs.oop} for a concrete example).
    68103In mainstream object-oriented languages such as Java algebraic data types correspond to interfaces, or some base object.
    69 Constructors correspond to classes implementing this interface; pattern matching is emulated using the language's dynamic dispatch mechanism.
    70 The interface specifies the permitted operations defined for the type.
    71 In contrast to the functional approach, it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy.
     104Constructors correspond to classes implementing this interface; branching by pattern matching is emulated using the language's dynamic dispatch mechanism.
     105The base interface of the object hierarchy specifies the permitted operations defined for the type.
     106
     107As all operations
     108it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy.
    72109If the interface changes so must every class implementing it.
    73110However, note it is easy to extend the hierarchy to new cases, corresponding to the introduction of a new constructor in the functional world, by merely adding another class corresponding to that constructor implementing the interface.
     
    80117 \item Bounded vs not-bounded.
    81118\end{itemize}
     119
     120%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     121% Section
     122%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     123\subsection{Matita}
     124\label{subsect.matita}
    82125
    83126\subsection{Subtyping as instantiation vs subtyping as safe static cast}
     
    119162\section{Appendix: interface of library functions used to implement everything}
    120163
     164\bibliography{polymorphic-variants}
     165
    121166\end{document}
Note: See TracChangeset for help on using the changeset viewer.