From a141456b522d48527bb54f222f72bbe8081360ff Mon Sep 17 00:00:00 2001 From: ben Date: Wed, 16 Mar 2016 00:25:25 -0400 Subject: [PATCH] [icfp] explain tagging, kinda formally --- icfp-2016/intro.scrbl | 44 ++++++++++------------------------------ icfp-2016/solution.scrbl | 19 +++++++++++++++++ 2 files changed, 30 insertions(+), 33 deletions(-) diff --git a/icfp-2016/intro.scrbl b/icfp-2016/intro.scrbl index acaec0e..b066a67 100644 --- a/icfp-2016/intro.scrbl +++ b/icfp-2016/intro.scrbl @@ -1,13 +1,4 @@ #lang scribble/sigplan @onecolumn -@; TODO -@; - stephen: too vague! -@; - sam : too vague! -@; : can you give more example? -@; : too generous to other languages -- why didn't you do the entire paper in hs? -@; - a note on macro-land? where truthy & boolean monads are king? -@; - also, the untyped style of reasoning, the needing to unfold code -@; - transf vs. macro -@; - remove "OUR" @require["common.rkt"] @@ -19,12 +10,12 @@ Well-typed programs @emph{do} go wrong. All the time, in fact: @codeblock{ - > (vector-ref (build-vector 2 (λ (i) i)) 3) - ; vector-ref: index is out of range + > (vector-ref (make-vector 2) 3) + ==> vector-ref: index is out of range > (/ 1 0) - ; /: division by zero + ==> /: division by zero > (printf "~s") - ; printf: format string requires 1 arguments, given 0 + ==> printf: format string requires 1 arguments, given 0 } Of course, Milner's catchphrase was about preventing type errors. @@ -47,7 +38,7 @@ The standard work-around@~cite[fi-jfp-2000] is to maintain size-indexed These problems are well known, and are often used to motivate research on dependently typed programming languages@~cite[a-icfp-1999]. Short of abandoning ship for a completely new type system, languages including - Haskell, OCaml, Java, and Typed Racket have seen proposals for detecting + Haskell, Java, OCaml, and Typed Racket have seen proposals for detecting certain values errors or expressing the polymorphism in functions such as @racket[curry] with few (if any) changes to the existing type system@~cite[ddems-icse-2011 ks-plpv-2006 kkt-pldi-2016 lb-sigplan-2014]. What stands between these proposals and their adoption is the complexity or @@ -62,13 +53,13 @@ The key is to run a @emph{textualist}@note{A textualist interprets laws by evident from the program syntax to the type checker. In terms of the first example in this section, our elaborator infers that the @racket[vector-ref] at position @racket[3] is out of bounds because it knows that - @racket[(build-vector n f)] + @racket[(make-vector n)] constructs a vector with @racket[n] elements. Our implementation is a Typed Racket library that shadows functions such as @racket[build-vector] with textualist elaborators following the guidelines stated in @Secref{sec:solution}. -We make essential use of Racket's powerful macro system@~cite[fcdb-jfp-2012] +We make essential use of Racket's macro system@~cite[fcdb-jfp-2012] to reason locally, associate inferred data with bound identifiers, and cooperate with the rules of lexical scope. For the adventurous reader, @Secref{sec:implementation} describes the @@ -97,11 +88,12 @@ We have written an elaborator for @racket[regexp-match] that will statically The elaborator also handles the common case where the regular expression argument is a compile-time constant and respects @exact{$\alpha$}-equivalence. +In sum, the code below will compile using our library's @racket[regexp-match] + whereas Typed Racket cannot guarantee the call to @racket[second] will produce + a string. + @codeblock{ (define rx-case #rx"(.*) v\\. (.*),") - -; Other code here - (define r-m regexp-match) (define (get-plaintiff (s : String)) : String @@ -114,17 +106,3 @@ The elaborator also handles the common case where the regular expression @Secref{sec:usage} has more examples. @Secref{sec:conclusion} concludes. -@; ============================================================================= - -@parag{Lineage} - -Herman and Meunier demonstrated how Racket macros can propagate - data embedded in string values and syntax patterns to a - static analyzer@~cite[hm-icfp-2004]. -Their illustrative examples were format strings, regular expressions, - and database queries. -Relative to their pioneering work, we adapt Herman & Meunier's - transformations to a typed language by inserting type annotations and boolean - guards into the programs. -Our treatment of definition forms is also new. - diff --git a/icfp-2016/solution.scrbl b/icfp-2016/solution.scrbl index d5d4fcc..925ad84 100644 --- a/icfp-2016/solution.scrbl +++ b/icfp-2016/solution.scrbl @@ -101,3 +101,22 @@ In a perfect world both would diverge, but the fundamental limitations of At present, these correctness requirements must be checked manually by the author of a function in @exact{$\interp$} or @exact{$\elab$}. + +@; ============================================================================= +@section{Cooperative Elaboration} + +Suppose we implement a currying operation + @exact{$\elabf$} such that e.g. + @exact{$\llbracket$}@racket[(curry (λ (x y) x))]@exact{$\rrbracket~=~$}@racket[(curry_2 (λ (x y) x))]. +The arity of @racket[(λ (x y) x)] is clear from its representation. +The arity of the result could also be derived from its textual representation, + but it is simpler to @emph{tag} the result such that future elaborations + can retrieve the arity of @racket[(curry_2 (λ (x y) x))]. + +Our implementation uses a tagging protocol, and this lets us share information + between unrelated elaboration function in a bottom-up recursive style. +The same protocol helps us implement binding forms: when interpreting a variable, + we check for an associated tag. +Formally speaking, this either changes the codomain of functions in @exact{$\elab$} + or introduces an elaboration environment mapping expressions to values. +