\documentclass{article}

\usepackage[a4paper]{geometry}
\usepackage{hyperref}
\usepackage{minted}

\title{Do you see what I see?\\{\large\emph{Functional pearl} (2016)}}
\author{M.~Lubbers}
\date{\today}

\newcommand{\fps}{\emph{Functional Pearls}}

\hypersetup{%
    pdftitle={Do you see what I see?},
    pdfauthor={Mart Lubbers},
    pdfcreator={Mart Lubbers},
    pdfproducer={Mart Lubbers},
	hidelinks
}
\begin{document}
\maketitle
\section{Objective}
\subsection{About functional pearls\ldots}
\fps\ were first introduced in 1993 as a column in the \emph{Journal of
Functional Programming}. In the natural world a pearl is created by a living
shelled mollusk when an irritating object, a sand corn for example, enters
their clam. A pearl is then formed around the irritation to encapsulate it and
prevent it from doing more harm. \fps\ are elegant, instructive and fun columns
of about 6 pages that present such a beautiful solution for a possible
irritation. \fps\ should be readable by people with a general knowledge of
functional programming but it should not require a lot of very specific domain
knowledge. Several important persons in the functional programming academia
have been editors of this famous column.

\subsection{Sand corn}
Dependant types in type systems are very expensive and often require the
programmer to provide proofs or elaborations on the type specification. Also,
contrary to popular beliefs, when a program passes the type checker it is not
guaranteed to be correct. Moreover, some programs that are correct can not be
expressed in current type systems.

This pearl provides solutions for the problems that does not require the
programmer to use annotations. The implementation is done in the \emph{Typed
Racket} macro language and just importing the library is enough. The macro
system will automatically process the source code and provide errors and
elaborations as needed.

\section{Proposal}
\subsection{Untypable arity}
Some functions can not be expressed in current non-dependant type systems. One
of such function type is the curry function without a specific arity. One wants
to be able to just use the curry function as is for all arities because from
the structure of the function you know the arity and elaborate on the type on
the fly. A problem in the same class could be the tuple selector first, second
and friends. 

\newpage
The following sequence of racket expressions shows such curry expressions that
are of unknown arity for the typechecker.
\begin{minted}{racket}
(curry (lambda (x y) x))
(curry (lambda (x y z) x))
(curry (lambda (x y z a) x))
\end{minted}

After expanding the macros the elaborated form looks like the following
snippet:

\begin{minted}{racket}
(curry2 (lambda (x y) x))
(curry3 (lambda (x y z) x))
(curry4 (lambda (x y z a) x))
\end{minted}

\subsection{Elaborate on printf type}
The type of the \mintinline{racket}|printf| function is a peculiar one. Neither
the number of arguments nor the types of the arguments are fixed because those
two properties depend on the contents of the formatstring which is the first
\mintinline{racket}|String| argument. The standard, unprocessed type of would
be shaped as:

\mint{racket}|(printf :: String Any * -> Void)|

But when the string is a fixed constant or it can be derived at compile time
the macro system can already infer or pinpoint the types of the arguments and
thus of the function. Just as in other \emph{LISP} like languages the format
string specifier is \mintinline{racket}|~|. For example the format string
\mintinline{racket}|"~b"| tries to print the number given as the first argument
as a binary number. The only valid argument for this is an Integer. When this
formatstring is used the macro system can thus already elaborate on the type of
the arguments and the function. The following function signature
would then be the result of an elaboration 
\mintinline{racket}|printf "~b" 42|.

\mint{racket}|(printf :: String Integer -> Void)|

When the programmer does not provide an Integer as the first argument the
elaboration results in a type error. Because of the elaborations the type
checker can also infer types from the arguments when it was impossible before
the elaborations

\subsection{Other examples}
The author gives numerous other examples:
\begin{enumerate}
	\item Pre-calculating numeric expressions into constants. This can be used
		for example for catching division by zero errors.
	\item Regular expressions also have a certain knowledge embedded in the
		syntax. For example extracting groups is a property on which the macro
		system can elaborate on for example the length of the return vector
		that stores the expressions.
	\item SQL queries have similar properties, the return type is completely
		dependant on the structure of the SQL query and can often be inferred
		and elaborated upon.
	\item Vector out of bound errors are very common errors in programming. In
		a lot of cases the length of a vector is known at compile time and such
		errors can be detected by the macro system. Of this particular example
		a, partial, implementation will be shown in the following section.
\end{enumerate}

\section{Evidence}
As said, all the programmer has to do is import the library. The \emph{Typed
Racket} macro system does all the elaborations and provides
errors and elaborations. The elaboration functions runs via macros on the
actual syntax itself. This is possible because the macro system of \emph{Typed
Racket} runs recursively and has sophisticated matching techniques for
syntactical objects. Such objects are classified as syntactical objects.

Let us present the example with fixed size vectors. Fixed size vectors can be
defined in two ways in \emph{Typed Racket}. They can be defined literally using
the \mintinline{racket}|#(4 42 1 0)| or an empty vector can be created with
\mintinline{racket}|(make-vector 4)|. There are several functions available
that can concatenate, lengthen, shorten and copy vectors. If the programmer
only uses those operations it can be known at compiletime what the length of
the vector is and thus if the programmers goes out of bounds.

All syntactical objects adhering to the above precondition are getting
classified as \\\mintinline{racket}|vector/length| syntax class objects and
those class objects are used in pattern matching. For example the following
macro aliases the \mintinline{racket}|vector-length| function so that it either
contains the literal length or the original function. The
\mintinline{racket}|syntax-parser| calls the literal syntax objects and the two
statements after are pattern-match like statements that when the vector is of
syntax class \mintinline{racket}|vector/length| the evidence for that object is
returned and otherwise the function is undefined and thus the original meaning
stays.

\begin{minted}{racket}
(make-alias #'vector-length
    (syntax-parser
        [(_ v:vector/length)
            #''v.evidence]
        [_ #false]))
\end{minted}

Determining the syntax class is yet another macro that again from the
\mintinline{racket}|syntax-parser| constructs either such objects or is
undefined. The following function shows the macro that elaborates on vector
construction constructs. The macro matches either the literal vector
notation, in which it can just count the elements. Or the macro matches a
\mintinline{racket}|make-vector| construct with as an argument an object of the
syntax class \mintinline{racket}|num/value| which is a class created for
literal ints. Note that literal ints can also be the result of an expression.
In all other cases the macro does not elaborate.

\begin{minted}{racket}
(define vector?
    (syntax-parser #:literals (make-vector)
        [#(e* ...)
            (length (syntax->datum #'(e* ...)))]
        [(make-vector n:num/value)
            (syntax->datum #'n.evidence)]
        [_ #false]))
\end{minted}

While the examples are given the author notes that they could be easily
translated to languages that have a similar macro system like \emph{Typed
Clojure} or \emph{Rust}. The system can also, with some adaptations, be ported
to languages with template systems like \emph{Template Haskell} or
\emph{OCaml}.

\section{Writing}
The general writing style of the pearl starts out very good. The first section
is very interestingly written and makes the reader very curious about the
implementation and consequences. The implementation itself comes quite late in
the paper and there are only proposed elaboration macros for the vector example
given. The other examples are left to the imagination. The examples given in
this review are only a small part of the examples in the pearl and even they
are not very easy to understand which should not be in the nature of a pearl.

The implementation language used is not a very popular language in academia
compared to other functional languages like \emph{Haskell} or \emph{Lisp}.

\section{Discussion}
The examples given are one showing pretty trivial functionality which makes me
wonder whether the proposed solution is scalable to more real world programming
errors instead of simple ones. Even for the simple examples the macros are very
complicated and that makes me worry if the solution will be useful or just
produce obfuscated compiler errors.

The implementation is very complex and there should be more elaboration on it
to guide the reader more in the process. Maybe even a short \emph{Typed Racket}
macro language introduction.

Lastly the paper should benefit from having been written in more famous
language or the language should be introduced more. It is not clear what the
benefits are at the moment.

\section{Verdict}
I would advice to give a conditional accept to the paper. When more elaboration
is given on the implementation and the scalability is assessed it is a good
\emph{Functional Pearl}.
\end{document}
