From 5db0b3a5ed83c80babe900d45353ad99ba3c9673 Mon Sep 17 00:00:00 2001 From: ben Date: Thu, 3 Mar 2016 23:13:29 -0500 Subject: [PATCH] [icfp] new deal intro, going slow but well --- icfp-2016/intro.scrbl | 148 ++++++++++++++++++++++++++--------------- icfp-2016/paper.scrbl | 16 ++--- icfp-2016/texstyle.tex | 3 +- 3 files changed, 105 insertions(+), 62 deletions(-) diff --git a/icfp-2016/intro.scrbl b/icfp-2016/intro.scrbl index 405a6fc..161ced9 100644 --- a/icfp-2016/intro.scrbl +++ b/icfp-2016/intro.scrbl @@ -1,73 +1,115 @@ #lang scribble/sigplan +@; Tuples in Haskell http://hackage.haskell.org/package/tuple +@; Regexp +@; - ocaml http://caml.inria.fr/pub/docs/manual-ocaml/libref/Str.html +@; - haskell https://hackage.haskell.org/package/regex-compat/docs/Text-Regex.html + @require["common.rkt"] @title{Introduction} -@; format/printf : played out -@; regexp-match : complicated, from HM -@; + : way too simple -@; vector-length : boring +@; tautology checker +@; curry +@; deep +@; regexp match -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? +Many useful functions do not have simple types. +For example, one cannot write a general procedure for currying functions + or accessing the first element of an arbitrarily-sized tuple in OCaml or Haskell. +@; TODO don't mention ML/Hask ... use System F? +Nevertheless, specialized versions of @racket[curry] and @racket[first] are + easy to define and type. @racketblock[ - (regexp-match pattern str) + > curry (λ (x y) x) > first (x, y) + (λ (x) (λ (y) x)) x + ] -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. +That is, once some basic structure of the input is fixed, the general + problem becomes a much simpler, specific problem. +If ever a 16-argument function needs currying, we can write a new function for + the task. +@; This pearl explains how ... +By creating the specific @racket[curry] or @racket[first] for each size of + function or tuple value in a program, we -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. +In general, we consider functions like @racket[curry] and @racket[first] for + arbitrarily-sized -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.} +@; Introduce name? Talk about indexed families? -@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. +@;These functions behave in a straightforward manner, but depend on +@; characteristics of their input that most type systems do not express generically. -@;Additionally replacing @racket[str] with a value gives an even more precise type by -@; evaluating the expression while type checking. + + + +Many workarounds = polydots, pi-types, printf-types, ... + + +@; 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} diff --git a/icfp-2016/paper.scrbl b/icfp-2016/paper.scrbl index d472b01..76a2f56 100644 --- a/icfp-2016/paper.scrbl +++ b/icfp-2016/paper.scrbl @@ -3,7 +3,7 @@ @(require "common.rkt") @authorinfo["Ben Greenman" - "Northeastern University, Boston, USA" + "PLT @ Northeastern University, Boston, USA" ""] @title{Functional Pearl: Do you see what I see?} @@ -29,13 +29,13 @@ @;@keywords{Gradual typing, performance evaluation} @include-section{intro.scrbl} -@include-section{solution.scrbl} -@include-section{usage.scrbl} -@include-section{experience.scrbl} @; Merge with usage? -@include-section{implementation.scrbl} -@include-section{correctness.scrbl} -@include-section{related.scrbl} -@include-section{conclusion.scrbl} +@;@include-section{solution.scrbl} +@;@include-section{usage.scrbl} +@;@include-section{experience.scrbl} @; Merge with usage? +@;@include-section{implementation.scrbl} +@;@include-section{correctness.scrbl} +@;@include-section{related.scrbl} +@;@include-section{conclusion.scrbl} @section[#:style 'unnumbered]{Acknowledgments} diff --git a/icfp-2016/texstyle.tex b/icfp-2016/texstyle.tex index d3295b6..6676b4e 100644 --- a/icfp-2016/texstyle.tex +++ b/icfp-2016/texstyle.tex @@ -1,6 +1,7 @@ % Better horizontal rules \usepackage{booktabs} - +\usepackage{listings} +\lstset{language=ML} \usepackage[usenames,dvipsnames]{xcolor} \usepackage{multicol}