long2/long.tex

   1 \documentclass[draft]{article}
   2
   3 \usepackage[a4paper]{geometry}
   4 \usepackage{hyperref}
   5 \usepackage{minted}
   6
   7 \title{Do you see what I see?\\{\large\emph{Functional pearl} (2016)}}
   8 \author{M.~Lubbers}
   9 \date{\today}
  10
  11 \newcommand{\fps}{\emph{Functional Pearls}}
  12
  13 \hypersetup{%
  14     pdftitle={Do you see what I see?},
  15     pdfauthor={Mart Lubbers},
  16     pdfcreator={Mart Lubbers},
  17     pdfproducer={Mart Lubbers},
  18         hidelinks
  19 }
  20 \begin{document}
  21 \maketitle
  22 \section{Objective}
  23 \subsection{About functional pearls\ldots}
  24 \fps\ were first introduced in 1993 as a column in the \emph{Journal of
  25 Functional Programming}. In the natural world a pearl is created by a living
  26 shelled mollusk when an irritating object enters their clam. A pearl is then
  27 formed around the irritation to encapsulate it and prevent it from doing more
  28 harm. \fps\ are elegant, instructive and fun columns of about 6 pages that
  29 present such a beautiful solution for a possible irritation. \fps\ should be
  30 readable by people with a general knowledge of functional programming but it
  31 should not require a lot of very specific domain knowledge. Several important
  32 persons in the functional programming academia have been editors of this
  33 column.
  34
  35 \subsection{Sand corn}
  36 Dependant types in type systems are very expensive and often require the
  37 programmer to provide proofs or elaborations on the type specification. Also,
  38 contrary to popular beliefs, when a program passes the type checker it is not
  39 guaranteed to be correct. Moreover, some programs that are correct can not be
  40 expressed in current type systems.
  41
  42 This pearl provides solutions for the problems that does not require the
  43 programmer to use annotations. The implementation is done in the \emph{Typed
  44 Racket} macro language and just importing the library already makes it work.
  45
  46 \section{Proposal}
  47 \subsection{Untypable arity}
  48 Some functions are not typeable in current non-dependant type systems. One of
  49 such function type is the universal curry function. One wants to be able to
  50 just use the curry function as is for all arities because from the structure of
  51 the function you can see the arity and elaborate on the type on the fly. For
  52 example the following sequence of racket expressions.
  53 \begin{minted}{racket}
  54 (curry (lambda (x y) x))
  55 (curry (lambda (x y z) x))
  56 (curry (lambda (x y z a) x))
  57 \end{minted}
  58
  59 Expands by macro expansion to:
  60
  61 \begin{minted}{racket}
  62 (curry2 (lambda (x y) x))
  63 (curry3 (lambda (x y z) x))
  64 (curry4 (lambda (x y z a) x))
  65 \end{minted}
  66
  67 \subsection{Elaborate on printf type}
  68 The type of the \mintinline{racket}|printf| function is again untypeable
  69 because it depends on the contents of the first \mintinline{racket}|String|
  70 argument. The unelaborated type of would be something like:
  71
  72 \mint{racket}|(printf :: String Any * -> Void)|
  73
  74 But when the string is already known, for example at compiletime, you can
  75 already elaborate a lot on the type. For example the string
  76 \mintinline{racket}|"~b"| depicts the format string for a binary number. The
  77 only valid argument for this is an Integer. The following function signature
  78 would then be the result of an elaboration using the macro system on
  79 \mintinline{racket}|printf "~b" 42|.
  80
  81 \mint{racket}|(printf :: String Integer -> Void)|
  82
  83 \subsection{Other examples}
  84 The author gives numerous other examples ranging from extracting the number of
  85 return groups in regular expression matching. Detecting the return type in
  86 database queries. precalculating numeric expressions and catch errors like
  87 divison by zero. Moreover the author proposes a set of macros that can
  88 elaborate on the length of a fixed size vector to remove the need for bounds
  89 checking and index errors. On said example we will show some of the
  90 implementation.
  91
  92 \section{Evidence}
  93 As said, all the programmer has to do is import the library. The \emph{Typed
  94 Racket} macro system does all the elaborations and provides
  95 errors and elaborations. The elaboration functions runs via macros on the
  96 actual syntax itself. This is possible because the macro system of \emph{Typed
  97 Racket} runs recursively and has sophisticated matching techniques for
  98 syntactical objects. Such objects are classified as syntactical objects.
  99
 100 Let us present the example with fixed size vectors. Fixed size vectors can be
 101 defined in two ways in \emph{Typed Racket}. They can be defined literally using
 102 the \mintinline{racket}|#(4 42 1 0)| or an empty vector can be created with
 103 \mintinline{racket}|(make-vector 4)|. There are several functions available
 104 that can concatenate, lengthen, shorten and copy vectors. If the programmer
 105 only uses those operations it can be known at compiletime what the length of
 106 the vector is and thus if the programmers goes out of bounds.
 107
 108 All syntactical objects adhering to the above precondition are getting
 109 classified as \mintinline{racket}|vector/length| syntax class objects and those
 110 class objects are used in pattern matching. For example the following macro
 111 aliasses the \mintinline{racket}|vector-length| function so that it either
 112 contains the literal length or the original function. The
 113 \mintinline{racket}|syntax-parser| calls the literal syntax objects and the two
 114 statements after are pattern-match like statements that when the vector is of
 115 syntax class \mintinline{racket}|vector/length| the evidence for that object is
 116 returned and otherwise the function is undefined and thus the original meaning
 117 stays.
 118
 119 \begin{minted}{racket}
 120 (make-alias #'vector-length
 121     (syntax-parser
 122         [(_ v:vector/length)
 123             #''v.evidence]
 124         [_ #false]))
 125 \end{minted}
 126
 127 Determining the syntax class is yet another macro that again from the
 128 \mintinline{racket}|syntax-parser| constructs either such objects or is
 129 undefined. The following function shows the macro that elaborates on vector
 130 construction constructs. The macro matches either the literal vector
 131 notation, in which it can just count the elements. Or the macro matches a
 132 \mintinline{racket}|make-vector| construct with as an argument an object of the
 133 syntax class \mintinline{racket}|num/value| which is a class created for
 134 literal ints. Note that literal ints can also be the result of an expression.
 135 In all other cases the macro does not elaborate.
 136
 137 \begin{minted}{racket}
 138 (define vector?
 139     (syntax-parser #:literals (make-vector)
 140         [#(e* ...)
 141             (length (syntax->datum #'(e* ...)))]
 142         [(make-vector n:num/value)
 143             (syntax->datum #'n.evidence)]
 144         [_ #false]))
 145 \end{minted}
 146
 147 While the examples are given the author notes that they could be easily
 148 translated to languages that have a similar macro system or to template-like
 149 macro systems when adapted.
 150
 151 \section{Writing}
 152 The general writing style of the pearl starts out very good. The first section
 153 is very interestingly written and makes the reader very curious about the
 154 implementation and consequences.
 155 The author only shows implementation of such elaboration macros for the vector
 156 example. The examples given are only a small part of the examples in the pearl
 157 and even they are not very easy to understand.
 158
 159 Also there are only a few examples given and while they can help the programmer
 160 they all seem trivial in functionality.
 161
 162 The implementation language used is not a very popular language in academia
 163 compared to other functional languages like \emph{Haskell} or \emph{Lisp}.
 164
 165 Another critique on the pearl is that the implementation comes quite late in
 166 the article and is very complex. A certain kind of beauty is incorporated in
 167 the automatic elaboration but one has to wait for quite some time to finally
 168 get to know the implementation.
 169
 170 \section{Discullion}
 171 %% Discussion points: end with questions which you think should arise
 172 %\begin{frame}
 173 %       \frametitle{Discussion points}
 174 %       \begin{itemize}
 175 %               \item There should be more elaboration on the implementation.
 176 %               \item Is the addition really helpful or does it just produce more
 177 %                       obfuscated compiler errors.
 178 %               \item Paper should have been written in a more famous language.
 179 %       \end{itemize}
 180 %\end{frame}
 181 \end{document}