From: Mart Lubbers Date: Mon, 30 May 2016 20:04:44 +0000 (+0200) Subject: update X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=e12b75f6015cdb8a591ac0e24e90516e80da9b95;p=rsss1516.git update --- diff --git a/long2/Makefile b/long2/Makefile index 6b3888c..ab6ed10 100644 --- a/long2/Makefile +++ b/long2/Makefile @@ -4,8 +4,8 @@ DOCUMENT:=long all: long.pdf slides.pdf %.pdf: %.tex - $(LATEX) $< - $(LATEX) $< + $(LATEX) -shell-escape $< + $(LATEX) -shell-escape $< clean: - $(RM) -v *.fmt *.aux *.log *.out *.toc *.pdf + $(RM) -rv *.fmt *.aux *.log *.out *.toc *.pdf _minted* diff --git a/long2/long.tex b/long2/long.tex index 7a2a664..26614a7 100644 --- a/long2/long.tex +++ b/long2/long.tex @@ -1,12 +1,15 @@ -\documentclass{article} +\documentclass[draft]{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}, @@ -16,30 +19,160 @@ } \begin{document} \maketitle -\tableofcontents \section{Objective} -% what is the goal of this work, what problem is addressed, what was the -% current state of the art, who is the work aimed at? +\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 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 +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 already makes it work. \section{Proposal} -% if the paper presents a new idea, what, in a nutshell, is it? +\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. +\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: + +\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 again untypeable +because it depends on the contents of the first \mintinline{racket}|String| +argument. The unelaborated type of would be something like: + +\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 +\mintinline{racket}|printf "~b" 42|. + +\mint{racket}|(printf :: String Integer -> Void)| + +\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. \section{Evidence} -% Support for claims - Theorems? Case studies? Simulations? Benchmarks? Does -% evidence address issues needed to support claims? +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 +aliasses 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. -\section{Shoulders of giants\ldots} -% what previous research does this work build on? What are the key underlying -% theoretical ideas? Software infrastructure? +\begin{minted}{racket} +(make-alias #'vector-length + (syntax-parser + [(_ v:vector/length) + #''v.evidence] + [_ #false])) +\end{minted} -\section{Impact} -% has this work been influential? When later research papers cite it, what -% contribution is being referred to? +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 or to template-like +macro systems when adapted. \section{Writing} -% analyse the writing +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. + +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 points} -% end with questions which you think should arise +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} \end{document}