From 72d40fcfd427f81d7228be068746417b556734fc Mon Sep 17 00:00:00 2001 From: ben Date: Tue, 1 Mar 2016 19:56:20 -0500 Subject: [PATCH] [icfp] draft intro --- icfp-2016/bib.rkt | 13 ++++++ icfp-2016/common.rkt | 3 ++ icfp-2016/intro.scrbl | 97 +++++++++++++++++++++++++++++++++++++++++++ icfp-2016/paper.scrbl | 35 ++++++++-------- 4 files changed, 130 insertions(+), 18 deletions(-) create mode 100644 icfp-2016/intro.scrbl diff --git a/icfp-2016/bib.rkt b/icfp-2016/bib.rkt index 5f41c0f..4d1da5a 100644 --- a/icfp-2016/bib.rkt +++ b/icfp-2016/bib.rkt @@ -1038,3 +1038,16 @@ #:title "MACLISP Reference Manual" #:date 1974)) +(define f-scp-1991 + (make-bib + #:author "Matthias Felleisen" + #:title "On the Expressive Power of Programming Languages" + ;#:location (proceedings-location "Science of Computer Programming") + #:date 1991)) + +(define hm-icfp-2004 + (make-bib + #:author "David Herman and Philippe Meunier" + #:title "Improving the Static Analysis of Embedded Languages via Partial Evaluation" + #:location (proceedings-location icfp) ;#:pages '() + #:date 2004)) diff --git a/icfp-2016/common.rkt b/icfp-2016/common.rkt index dcec205..fe0f4a0 100644 --- a/icfp-2016/common.rkt +++ b/icfp-2016/common.rkt @@ -16,6 +16,7 @@ parag sf id + todo ) (require "bib.rkt" @@ -133,3 +134,5 @@ (define (id x) (make-element plain @format["~a" x])) +(define (todo . x) + (make-element 'bold (list x))) diff --git a/icfp-2016/intro.scrbl b/icfp-2016/intro.scrbl new file mode 100644 index 0000000..b3f743c --- /dev/null +++ b/icfp-2016/intro.scrbl @@ -0,0 +1,97 @@ +#lang scribble/sigplan + +@require["common.rkt"] + + +@title{Introduction} +@; format/printf : played out +@; regexp-match : complicated, from HM +@; + : way too simple +@; vector-length : boring + +Suppose @racket[regexp-match] is a function for matching a + regular expression pattern against a string value. +If the match succeeds then the function returns a list containing the + part of the string that was matched and all matched groups + corresponding to parenthesized sub-patterns of the regular expression. +Otherwise, it returns a value indicating the match failed. +@; TODO Specify the type system? +Suppose also that @racket[pattern] and @racket[group] are variables + bound to string values at run-time. +Given these premises, what is the type of this expression? + +@racketblock[ + (regexp-match pattern str) +] + +One simple answer is @racket[(Option (Listof String))]. +If all goes well the resulting value will be a list of strings (of unspecified + length), but we know ahead of time that the match may fail. + +In a programming language with the full power of dependent types, we can encode + the relationship between @racket[pattern] and @racket[str] and give a very + specific type relating the number of groups in @racket[pattern] to the number + of elements in the result list. +Dependent types, however, typically require strategic use of type annotations + and carefully-selected data representations. +One relatively simple type for the expression above is + @racket[(Option (List[N] String))] where @racket[N] is the number of groups + in @racket[pattern], but this requires the type @racket[List] to carry length + information and a type for regular expressions that counts groups. +Building the infrastructure necessary to express that particular type of + the call to @racket[regexp-match] may give more trouble than relief. + +This paper explores a solution between simple and dependent types that + should apply in any typed language with sufficiently powerful + @emph{syntax extensions}, or macros. +The key idea is to refine types based on values apparent in the program text. +When the parameters to @racket[regexp-match] are bound at run-time, we + conservatively assign the type @racket[(Option (Listof String))]. +But if there is more information at hand, we use it. +For instance, both these expressions have the type + @racket[(Option (List String String))] in our system.@note{Where @racket[List] + is Typed Racket's type for heterogenous, sized lists; akin to tuple types in ML.} + +@racketblock[ + (regexp-match "hello(o*)" str) + + (let ([pattern "hello(o*)"]) + (regexp-match pattern str)) +] + +The pattern here has exactly one group, delimited by the parentheses. +Thus if the match succeeds we get a list of two elements: the first being + the entire matched substring and the second a string matching the regular + expression @racket{o*}. +All this is clear from the program text to the programmer; our contribution + is parsing the relevant information and forwarding it to the type checker. + +@;Additionally replacing @racket[str] with a value gives an even more precise type by +@; evaluating the expression while type checking. + + +@section{Prior & Current Work} + +A macro system provides a general framework for transforming and analyzing + program syntax. +Languages with strong macro systems are surprisingly expressive@~cite[f-scp-1991]. +Case in point, Herman and Meunier demonstrated how macros can propogate + information embedded in string values and syntax patterns to a + static analyzer@~cite[hm-icfp-2004]. +Their illustrative examples were format strings, regular expression patterns, + and database queries. +We adapt these examples to a typed programming language + and give additional examples inspired by the literature on dependent types. +By inserting type annotations and boolean guards our macros indirectly + facilitate type-checking. +Quite often---but not always---the inferred types can remove the need for + run-time assertions. + +Contents: +@itemlist[ + @item{A language-agnostic framework for value-dependent macros (Section 2).} + @item{Diverse motivating examples, from a type-safe @racket[printf] to a basic typeclass system (Section 3).} + @item{Description and evaluation of a Typed Racket implementation (Section 4).} + @item{Correctness requirements for transformations (Section 5).} + @item{Related work and conclusion (Section 6).} +] diff --git a/icfp-2016/paper.scrbl b/icfp-2016/paper.scrbl index b672848..740ead2 100644 --- a/icfp-2016/paper.scrbl +++ b/icfp-2016/paper.scrbl @@ -1,5 +1,4 @@ -#lang scribble/manual -@;#lang scribble/sigplan @onecolumn +#lang scribble/sigplan @onecolumn @preprint @(require "common.rkt") @@ -7,32 +6,32 @@ "Northeastern University, Boston, USA" ""] -@title{Functional Pearl: Do we @emph{really} need Dependent Types?} -@; Trivial differences, little things that count -@; Recall 'fexprs are trivial'? -@; Syntactically dependent types +@title{Functional Pearl: Do you see what I see?} +@subtitle{Improving a simple type system with dependent macros} +@; should say "value-dependent"? +@; TODO subtitle doesn't appear in the right place @abstract{ - The transformative @emph{and} analytic power of macros can turn - a polymorphic type system into a dependent type system, at least - for common programming tasks. - By analyzing program syntax and propogating known information about program - @emph{values} at compile-time, we can express many of the practical - motivations for dependent types without requiring programmer annotations - or changes to the underlying type system. - - Our macro-expanded types are not proving new theorems, - but they recognize facts obvious to the programmer and hopefully - give a nice programming experience. + A simple type system with macros is nearly as good as a dependent type + system, at least for some common programming tasks. + By analyzing program syntax and propogating constants + before type-checking, we can express many of the practical + motivations for dependent types without any programmer annotations + or extensions to the underlying type system. + Our syntax-dependent subtypes are not proving theorems, + but they detect certain run-time errors at compile-time and + cooperate with type inference. } @;@category["D.3.3" "Programming Languages" "Language Constructs and Features"] @;@terms{Performance, Experimentation, Measurement} @;@keywords{Gradual typing, performance evaluation} -@include-section{outline.scrbl} +@include-section{intro.scrbl} +@include-section{solution.scrbl} @;@section[#:style 'unnumbered]{Acknowledgments} +@; acks here @generate-bibliography[#:sec-title "References"]