[icfp] anon. functions done
This commit is contained in:
parent
b509908ad9
commit
a5d63661a6
|
@ -1203,3 +1203,9 @@
|
||||||
#:location (journal-location hosc #:volume 25 #:number 1 #:pages '(165 207))
|
#:location (journal-location hosc #:volume 25 #:number 1 #:pages '(165 207))
|
||||||
#:date 2012))
|
#:date 2012))
|
||||||
|
|
||||||
|
(define stf-esop-2009
|
||||||
|
(make-bib
|
||||||
|
#:title "Practical Variable-Arity Polymorphism"
|
||||||
|
#:author (authors "T. Stephen Strickland" "Sam Tobin-Hochstadt" "Matthias Felleisen")
|
||||||
|
#:location (proceedings-location esop #:pages '(32 46))
|
||||||
|
#:date 2009))
|
||||||
|
|
|
@ -668,3 +668,4 @@
|
||||||
#:author (authors "André Murbach Maidl" "Fabio Mascarenhas" "Roberto Ierusalimschy")
|
#:author (authors "André Murbach Maidl" "Fabio Mascarenhas" "Roberto Ierusalimschy")
|
||||||
#:location (proceedings-location dyla #:pages '(1 10))
|
#:location (proceedings-location dyla #:pages '(1 10))
|
||||||
#:date 2014))
|
#:date 2014))
|
||||||
|
|
||||||
|
|
|
@ -84,8 +84,8 @@ For a sense of the practical use-cases we envision, consider the function
|
||||||
|
|
||||||
@racketblock[
|
@racketblock[
|
||||||
> (regexp-match #rx"(.*) v\\. (.*),"
|
> (regexp-match #rx"(.*) v\\. (.*),"
|
||||||
"Chisom v. Roemer, 501 U.S. 380")
|
"Morrison v. Olson, 487 U.S. 654")
|
||||||
'("Chisom v. Roemer," "Chisom" "Roemer")
|
'("Morrison v. Olson" "Morrison" "Olson")
|
||||||
]
|
]
|
||||||
|
|
||||||
The parentheses in the regular expression delimit groups to match and
|
The parentheses in the regular expression delimit groups to match and
|
||||||
|
|
|
@ -121,7 +121,7 @@ In Typed Racket this function is rather simple because the most common
|
||||||
Now to use @racket[fmt->types] in an elaboration.
|
Now to use @racket[fmt->types] in an elaboration.
|
||||||
Given a call to @racket[printf], we check the number of arguments and
|
Given a call to @racket[printf], we check the number of arguments and
|
||||||
add type annotations using the inferred types.
|
add type annotations using the inferred types.
|
||||||
For all other syntax patterns, @racket[t-printf] is the identity transformation.
|
For all other syntax patterns, @racket[t-printf] is the identity elaboration.
|
||||||
|
|
||||||
@exact|{
|
@exact|{
|
||||||
\hfill\fbox{$\elabf \in \interp$}
|
\hfill\fbox{$\elabf \in \interp$}
|
||||||
|
@ -140,7 +140,7 @@ For all other syntax patterns, @racket[t-printf] is the identity transformation.
|
||||||
}|
|
}|
|
||||||
|
|
||||||
The first example is rejected immediately as a syntax error.
|
The first example is rejected immediately as a syntax error.
|
||||||
The second is a valid translation, but will lead to a static type error.
|
The second is a valid elaboration, but will lead to a static type error.
|
||||||
Put another way, the format string @racket{~b} specializes the type of
|
Put another way, the format string @racket{~b} specializes the type of
|
||||||
@racket[printf] from @racket[(String Any * -> Void)] to @racket[(String Integer -> Void)].
|
@racket[printf] from @racket[(String Any * -> Void)] to @racket[(String Integer -> Void)].
|
||||||
The third example demonstrates that higher-order
|
The third example demonstrates that higher-order
|
||||||
|
@ -201,9 +201,13 @@ Using this general type is cumbersome for simple patterns
|
||||||
\end{SingleColumn}\end{RktBlk}\end{SCodeFlow}
|
\end{SingleColumn}\end{RktBlk}\end{SCodeFlow}
|
||||||
}|
|
}|
|
||||||
|
|
||||||
@; TODO
|
|
||||||
We implement a parentheses-counting interpretation that parses regular expressions
|
We alleviate the need for casts and guards in simple patterns
|
||||||
|
with a parentheses-counting
|
||||||
|
interpretation that parses regular expressions
|
||||||
and returns the number of groups.
|
and returns the number of groups.
|
||||||
|
If there is any doubt whether a group will capture, we default to the general
|
||||||
|
@racket[regexp-match] type.
|
||||||
|
|
||||||
@todo{fbox} @racket[rx->groups] @exact|{$\in \interp$}|
|
@todo{fbox} @racket[rx->groups] @exact|{$\in \interp$}|
|
||||||
|
|
||||||
|
@ -216,7 +220,7 @@ We implement a parentheses-counting interpretation that parses regular expressio
|
||||||
#false
|
#false
|
||||||
]
|
]
|
||||||
|
|
||||||
The corresponding transformation
|
The corresponding elaboration
|
||||||
inserts casts to subtype the result of calls to @racket[regexp-match].
|
inserts casts to subtype the result of calls to @racket[regexp-match].
|
||||||
It also raises syntax errors when an uncompiled regular expression contains
|
It also raises syntax errors when an uncompiled regular expression contains
|
||||||
unmatched parentheses.
|
unmatched parentheses.
|
||||||
|
@ -239,31 +243,45 @@ By tokenizing symbolic λ-expressions, we can interpret their domain
|
||||||
statically. @todo{fbox} @racket[fun->domain] @exact|{$\in \interp$}|
|
statically. @todo{fbox} @racket[fun->domain] @exact|{$\in \interp$}|
|
||||||
|
|
||||||
@racketblock[
|
@racketblock[
|
||||||
> (fun->arity '(λ (x y z) (x (z y) y)))
|
> (fun->domain '(λ (x y z) (x (z y) y)))
|
||||||
'[Any Any Any]
|
'[Any Any Any]
|
||||||
> (fun->arity '(λ ([x : Real] [y : Real]) x))
|
> (fun->domain '(λ ([x : Real] [y : Real]) x))
|
||||||
'[Real Real]
|
'[Real Real]
|
||||||
]
|
]
|
||||||
|
|
||||||
When domain information is available at call sites to a @racket[curry] function,
|
When domain information is available at calls to a @racket[curry] function,
|
||||||
we can produce code that will pass typechecking.
|
we elaborate to a type-correct, indexed version of @racket[curry].
|
||||||
One method is to swap @racket[curry] with an indexed version,
|
Conceptually, we give @racket[curry] the unusable type @racket[(⊥ -> ⊤)] and
|
||||||
as demonstrated by @racket[t-swap] @exact|{$\in \trans$}|
|
elaboration produces a subtype @racket[curry_i].
|
||||||
|
|
||||||
|
@todo{fbox} @exact|{$\in \elab$}|
|
||||||
|
|
||||||
@racketblock[
|
@racketblock[
|
||||||
> (t-swap '(curry (λ (x y) x)))
|
> ('(curry (λ (x y) x)))
|
||||||
'(curry_1 (λ (x y) x))
|
'(curry_2 (λ (x y) x))
|
||||||
]
|
]
|
||||||
|
|
||||||
Another option is to implement @racket[curry] with unsafe tools from
|
@;Our implementation generates each @racket[curry_i] at compile-time by folding
|
||||||
the language runtime and assign it the trivial type @racket[(⊥ -> ⊤)]
|
@; over the interpreted domain.
|
||||||
A transformation would replace this type with a subtype where possible
|
This same technique can be used to implement generalized @racket[map] in
|
||||||
and let the type checker reject other calls.
|
languages without variable-arity polymorphism@~cite[stf-esop-2009].
|
||||||
Our implementation employs the first strategy, but generates a new @racket[curry_i]
|
|
||||||
at each call site by folding over the inferred function domain.
|
|
||||||
@; Mention this later, or show code?
|
|
||||||
|
|
||||||
TODO same goes for zipWith in a language without polydots
|
@racketblock[
|
||||||
|
> (define (cite (p : String) (d : String))
|
||||||
|
(printf "~a v. ~a, U.S.\n" p d))
|
||||||
|
> (define plaintiff*
|
||||||
|
'("Rasul" "Chisholm"))
|
||||||
|
> (define defendant*
|
||||||
|
'("Bush" "Georgia"))
|
||||||
|
> (map cite plaintiff* defendant*)
|
||||||
|
Rasul v. Bush, U.S.
|
||||||
|
Chisholm v. Georgia, U.S.
|
||||||
|
]
|
||||||
|
|
||||||
|
Leaving out an argument to @racket[printf] or passing an extra list
|
||||||
|
when calling @racket[map] will raise an arity error during elaboration.
|
||||||
|
On the other hand, if we modified @racket[cite] to take a third argument
|
||||||
|
then the above call to @racket[map] would fail to compile.
|
||||||
|
|
||||||
|
|
||||||
@; =============================================================================
|
@; =============================================================================
|
||||||
|
|
Loading…
Reference in New Issue
Block a user