suzanne.soy/trivial
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[icfp] new deal intro, going slow but well

Browse Source
This commit is contained in:
ben 2016-03-03 23:13:29 -05:00
parent 82927b6d17
commit 5db0b3a5ed
3 changed files with 105 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

148
icfp-2016/intro.scrbl
View File

@ -1,73 +1,115 @@
#lang scribble/sigplan #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"] @require["common.rkt"]
@title{Introduction} @title{Introduction}
@; format/printf : played out @; tautology checker
@; regexp-match : complicated, from HM @; curry
@; + : way too simple @; deep
@; vector-length : boring @; regexp match
Suppose @racket[regexp-match] is a function for matching a Many useful functions do not have simple types.
regular expression pattern against a string value. For example, one cannot write a general procedure for currying functions
If the match succeeds then the function returns a list containing the or accessing the first element of an arbitrarily-sized tuple in OCaml or Haskell.
part of the string that was matched and all matched groups @; TODO don't mention ML/Hask ... use System F?
corresponding to parenthesized sub-patterns of the regular expression. Nevertheless, specialized versions of @racket[curry] and @racket[first] are
Otherwise, it returns a value indicating the match failed. easy to define and type.
@; 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[ @racketblock[
(regexp-match pattern str) > curry (λ (x y) x) > first (x, y)
(λ (x) (λ (y) x)) x
] ]
One simple answer is @racket[(Option (Listof String))]. That is, once some basic structure of the input is fixed, the general
If all goes well the resulting value will be a list of strings (of unspecified problem becomes a much simpler, specific problem.
length), but we know ahead of time that the match may fail. 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 In general, we consider functions like @racket[curry] and @racket[first] for
the relationship between @racket[pattern] and @racket[str] and give a very arbitrarily-sized
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 @; Introduce name? Talk about indexed families?
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. @;These functions behave in a straightforward manner, but depend on
Thus if the match succeeds we get a list of two elements: the first being @; characteristics of their input that most type systems do not express generically.
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.
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} @section{Prior & Current Work}

16
icfp-2016/paper.scrbl
View File

@ -3,7 +3,7 @@
@(require "common.rkt") @(require "common.rkt")
@authorinfo["Ben Greenman" @authorinfo["Ben Greenman"
"Northeastern University, Boston, USA" "PLT @ Northeastern University, Boston, USA"
""] ""]
@title{Functional Pearl: Do you see what I see?} @title{Functional Pearl: Do you see what I see?}
@ -29,13 +29,13 @@
@;@keywords{Gradual typing, performance evaluation} @;@keywords{Gradual typing, performance evaluation}
@include-section{intro.scrbl} @include-section{intro.scrbl}
@include-section{solution.scrbl} @;@include-section{solution.scrbl}
@include-section{usage.scrbl} @;@include-section{usage.scrbl}
@include-section{experience.scrbl} @; Merge with usage? @;@include-section{experience.scrbl} @; Merge with usage?
@include-section{implementation.scrbl} @;@include-section{implementation.scrbl}
@include-section{correctness.scrbl} @;@include-section{correctness.scrbl}
@include-section{related.scrbl} @;@include-section{related.scrbl}
@include-section{conclusion.scrbl} @;@include-section{conclusion.scrbl}
@section[#:style 'unnumbered]{Acknowledgments} @section[#:style 'unnumbered]{Acknowledgments}

3
icfp-2016/texstyle.tex
View File

@ -1,6 +1,7 @@
% Better horizontal rules % Better horizontal rules
\usepackage{booktabs} \usepackage{booktabs}
\usepackage{listings}
\lstset{language=ML}
\usepackage[usenames,dvipsnames]{xcolor} \usepackage[usenames,dvipsnames]{xcolor}
\usepackage{multicol} \usepackage{multicol}