From: Mart Lubbers Date: Wed, 1 Jun 2016 18:55:54 +0000 (+0200) Subject: d X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=2a6e65b62ab1de3377e7bb2adf9272627a4c162b;p=rsss1516.git d --- diff --git a/long2/long.tex b/long2/long.tex index 75beb7a..3f94ae0 100644 --- a/long2/long.tex +++ b/long2/long.tex @@ -1,4 +1,4 @@ -\documentclass[draft]{article} +\documentclass{article} \usepackage[a4paper]{geometry} \usepackage{hyperref} @@ -41,22 +41,30 @@ 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 already makes it work. +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 are not typeable in current non-dependant type systems. One of -such function type is the universal curry function. One wants to be able to -just use the curry function as is for all arities because from the structure of -the function you can see the arity and elaborate on the type on the fly. For -example the following sequence of racket expressions. +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} -Expands by macro expansion to: +After expanding the macros the elaborated form looks like the following +snippet: \begin{minted}{racket} (curry2 (lambda (x y) x)) @@ -65,29 +73,49 @@ Expands by macro expansion to: \end{minted} \subsection{Elaborate on printf type} -The type of the \mintinline{racket}|printf| function is again untypeable -because it depends on the contents of the first \mintinline{racket}|String| -argument. The unelaborated type of would be something like: +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 already known, for example at compiletime, you can -already elaborate a lot on the type. For example the string -\mintinline{racket}|"~b"| depicts the format string for a binary number. The -only valid argument for this is an Integer. The following function signature -would then be the result of an elaboration using the macro system on +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 ranging from extracting the number of -return groups in regular expression matching. Detecting the return type in -database queries. precalculating numeric expressions and catch errors like -divison by zero. Moreover the author proposes a set of macros that can -elaborate on the length of a fixed size vector to remove the need for bounds -checking and index errors. On said example we will show some of the -implementation. +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 @@ -106,9 +134,9 @@ 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 -aliasses the \mintinline{racket}|vector-length| function so that it either +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 @@ -145,37 +173,40 @@ In all other cases the macro does not elaborate. \end{minted} While the examples are given the author notes that they could be easily -translated to languages that have a similar macro system or to template-like -macro systems when adapted. +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 author only shows implementation of such elaboration macros for the vector -example. The examples given are only a small part of the examples in the pearl -and even they are not very easy to understand. - -Also there are only a few examples given and while they can help the programmer -they all seem trivial in functionality. +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}. -Another critique on the pearl is that the implementation comes quite late in -the article and is very complex. A certain kind of beauty is incorporated in -the automatic elaboration but one has to wait for quite some time to finally -get to know the implementation. - -\section{Discullion} -%% Discussion points: end with questions which you think should arise -%\begin{frame} -% \frametitle{Discussion points} -% \begin{itemize} -% \item There should be more elaboration on the implementation. -% \item Is the addition really helpful or does it just produce more -% obfuscated compiler errors. -% \item Paper should have been written in a more famous language. -% \end{itemize} -%\end{frame} +\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}