long2/long.tex

   1 \documentclass{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, a sand corn for example, enters
  27 their clam. A pearl is then formed around the irritation to encapsulate it and
  28 prevent it from doing more harm. \fps\ are elegant, instructive and fun columns
  29 of about 6 pages that present such a beautiful solution for a possible
  30 irritation. \fps\ should be readable by people with a general knowledge of
  31 functional programming but it should not require a lot of very specific domain
  32 knowledge. Several important persons in the functional programming academia
  33 have been editors of this famous 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 is enough. The macro
  45 system will automatically process the source code and provide errors and
  46 elaborations as needed.
  47
  48 \section{Proposal}
  49 \subsection{Untypable arity}
  50 Some functions can not be expressed in current non-dependant type systems. One
  51 of such function type is the curry function without a specific arity. One wants
  52 to be able to just use the curry function as is for all arities because from
  53 the structure of the function you know the arity and elaborate on the type on
  54 the fly. A problem in the same class could be the tuple selector first, second
  55 and friends.
  56
  57 \newpage
  58 The following sequence of racket expressions shows such curry expressions that
  59 are of unknown arity for the typechecker.
  60 \begin{minted}{racket}
  61 (curry (lambda (x y) x))
  62 (curry (lambda (x y z) x))
  63 (curry (lambda (x y z a) x))
  64 \end{minted}
  65
  66 After expanding the macros the elaborated form looks like the following
  67 snippet:
  68
  69 \begin{minted}{racket}
  70 (curry2 (lambda (x y) x))
  71 (curry3 (lambda (x y z) x))
  72 (curry4 (lambda (x y z a) x))
  73 \end{minted}
  74
  75 \subsection{Elaborate on printf type}
  76 The type of the \mintinline{racket}|printf| function is a peculiar one. Neither
  77 the number of arguments nor the types of the arguments are fixed because those
  78 two properties depend on the contents of the formatstring which is the first
  79 \mintinline{racket}|String| argument. The standard, unprocessed type of would
  80 be shaped as:
  81
  82 \mint{racket}|(printf :: String Any * -> Void)|
  83
  84 But when the string is a fixed constant or it can be derived at compile time
  85 the macro system can already infer or pinpoint the types of the arguments and
  86 thus of the function. Just as in other \emph{LISP} like languages the format
  87 string specifier is \mintinline{racket}|~|. For example the format string
  88 \mintinline{racket}|"~b"| tries to print the number given as the first argument
  89 as a binary number. The only valid argument for this is an Integer. When this
  90 formatstring is used the macro system can thus already elaborate on the type of
  91 the arguments and the function. The following function signature
  92 would then be the result of an elaboration
  93 \mintinline{racket}|printf "~b" 42|.
  94
  95 \mint{racket}|(printf :: String Integer -> Void)|
  96
  97 When the programmer does not provide an Integer as the first argument the
  98 elaboration results in a type error. Because of the elaborations the type
  99 checker can also infer types from the arguments when it was impossible before
 100 the elaborations
 101
 102 \subsection{Other examples}
 103 The author gives numerous other examples:
 104 \begin{enumerate}
 105         \item Pre-calculating numeric expressions into constants. This can be used
 106                 for example for catching division by zero errors.
 107         \item Regular expressions also have a certain knowledge embedded in the
 108                 syntax. For example extracting groups is a property on which the macro
 109                 system can elaborate on for example the length of the return vector
 110                 that stores the expressions.
 111         \item SQL queries have similar properties, the return type is completely
 112                 dependant on the structure of the SQL query and can often be inferred
 113                 and elaborated upon.
 114         \item Vector out of bound errors are very common errors in programming. In
 115                 a lot of cases the length of a vector is known at compile time and such
 116                 errors can be detected by the macro system. Of this particular example
 117                 a, partial, implementation will be shown in the following section.
 118 \end{enumerate}
 119
 120 \section{Evidence}
 121 As said, all the programmer has to do is import the library. The \emph{Typed
 122 Racket} macro system does all the elaborations and provides
 123 errors and elaborations. The elaboration functions runs via macros on the
 124 actual syntax itself. This is possible because the macro system of \emph{Typed
 125 Racket} runs recursively and has sophisticated matching techniques for
 126 syntactical objects. Such objects are classified as syntactical objects.
 127
 128 Let us present the example with fixed size vectors. Fixed size vectors can be
 129 defined in two ways in \emph{Typed Racket}. They can be defined literally using
 130 the \mintinline{racket}|#(4 42 1 0)| or an empty vector can be created with
 131 \mintinline{racket}|(make-vector 4)|. There are several functions available
 132 that can concatenate, lengthen, shorten and copy vectors. If the programmer
 133 only uses those operations it can be known at compiletime what the length of
 134 the vector is and thus if the programmers goes out of bounds.
 135
 136 All syntactical objects adhering to the above precondition are getting
 137 classified as \\\mintinline{racket}|vector/length| syntax class objects and
 138 those class objects are used in pattern matching. For example the following
 139 macro aliases the \mintinline{racket}|vector-length| function so that it either
 140 contains the literal length or the original function. The
 141 \mintinline{racket}|syntax-parser| calls the literal syntax objects and the two
 142 statements after are pattern-match like statements that when the vector is of
 143 syntax class \mintinline{racket}|vector/length| the evidence for that object is
 144 returned and otherwise the function is undefined and thus the original meaning
 145 stays.
 146
 147 \begin{minted}{racket}
 148 (make-alias #'vector-length
 149     (syntax-parser
 150         [(_ v:vector/length)
 151             #''v.evidence]
 152         [_ #false]))
 153 \end{minted}
 154
 155 Determining the syntax class is yet another macro that again from the
 156 \mintinline{racket}|syntax-parser| constructs either such objects or is
 157 undefined. The following function shows the macro that elaborates on vector
 158 construction constructs. The macro matches either the literal vector
 159 notation, in which it can just count the elements. Or the macro matches a
 160 \mintinline{racket}|make-vector| construct with as an argument an object of the
 161 syntax class \mintinline{racket}|num/value| which is a class created for
 162 literal ints. Note that literal ints can also be the result of an expression.
 163 In all other cases the macro does not elaborate.
 164
 165 \begin{minted}{racket}
 166 (define vector?
 167     (syntax-parser #:literals (make-vector)
 168         [#(e* ...)
 169             (length (syntax->datum #'(e* ...)))]
 170         [(make-vector n:num/value)
 171             (syntax->datum #'n.evidence)]
 172         [_ #false]))
 173 \end{minted}
 174
 175 While the examples are given the author notes that they could be easily
 176 translated to languages that have a similar macro system like \emph{Typed
 177 Clojure} or \emph{Rust}. The system can also, with some adaptations, be ported
 178 to languages with template systems like \emph{Template Haskell} or
 179 \emph{OCaml}.
 180
 181 \section{Writing}
 182 The general writing style of the pearl starts out very good. The first section
 183 is very interestingly written and makes the reader very curious about the
 184 implementation and consequences. The implementation itself comes quite late in
 185 the paper and there are only proposed elaboration macros for the vector example
 186 given. The other examples are left to the imagination. The examples given in
 187 this review are only a small part of the examples in the pearl and even they
 188 are not very easy to understand which should not be in the nature of a pearl.
 189
 190 The implementation language used is not a very popular language in academia
 191 compared to other functional languages like \emph{Haskell} or \emph{Lisp}.
 192
 193 \section{Discussion}
 194 The examples given are one showing pretty trivial functionality which makes me
 195 wonder whether the proposed solution is scalable to more real world programming
 196 errors instead of simple ones. Even for the simple examples the macros are very
 197 complicated and that makes me worry if the solution will be useful or just
 198 produce obfuscated compiler errors.
 199
 200 The implementation is very complex and there should be more elaboration on it
 201 to guide the reader more in the process. Maybe even a short \emph{Typed Racket}
 202 macro language introduction.
 203
 204 Lastly the paper should benefit from having been written in more famous
 205 language or the language should be introduced more. It is not clear what the
 206 benefits are at the moment.
 207
 208 \section{Verdict}
 209 I would advice to give a conditional accept to the paper. When more elaboration
 210 is given on the implementation and the scalability is assessed it is a good
 211 \emph{Functional Pearl}.
 212 \end{document}