_Lambda-Gradual_ _lambda-gradual_ This collection provides two files: _lambda-gradual.ss_: the gradually typed lambda calculus _gui.ss_: graphical tools for interactive evaluation This library contains a PLT Redex model of the gradually typed lambda calculi of Siek and Taha and Herman, Tomb, and Flanagan. @InProceedings{ Siek06:gradual, author = {Jeremy G. Siek and Walid Taha}, title = {Gradual typing for functional languages}, booktitle = {Scheme and Functional Programming Workshop}, year = 2006, month = {September} } @InProceedings{ Herman07:gradual, author = {David Herman and Aaron Tomb and Cormac Flanagan}, title = {Space-Efficient Gradual Typing}, booktitle = {Trends in Functional Programming}, year = 2007, month = {April} } The details of the program semantics can be found in the internal modules found in the following source files: _static-semantics.ss_: type checking and cast insertion _core-language.ss_: core language definitions and functions _siek-taha.ss_: the Siek-Taha calculus _herman-tomb-flanagan.ss_: the Herman-Tomb-Flanagan calculus ====================================================================== lambda-gradual.ss ----------------- > type semantics > (semantics? x) : any -> boolean > st : semantics The gradually typed lambda calculus of Siek and Taha [Siek06:gradual]. > htf : semantics The space-efficient gradually typed lambda calculus of Herman, Tomb and Flanagan [Herman07:gradual]. > type source-expression An s-expression representing a gradually typed source program. The program may omit type annotations and does not yet contain explicit casts. source-expression ::= symbol | boolean | integer | (source-expression source-expression) | (if source-expression source-expression source-expression) | (op source-expression source-expression) | (let binding source-expression) | (letrec (binding ...) source-expression) | (lambda (symbol) source-expression) | (lambda (symbol : type) source-expression) binding ::= (symbol = source-expression) | (symbol : type = source-expression) type ::= dynamic | int | bool | (type -> type) op ::= + | - | = > type annotated-expression An s-expression representing a well-typed gradually typed program. The program may not omit type annotations and may contain explicit casts. > (type-check s e) : semantics * source-expression -> annotated-expression Type checks a gradually typed expression, inserting all casts and type annotations. > (next s e) : semantics * annotated-expression -> (optional annotated-expression) Performs a single reduction step. > (trace s e [cutoff]) : semantics * source-expression [* nat] -> (listof annotated-expression) Produces a program trace as a list of intermediate reduction steps for a gradually typed program. Reduction stops after `cutoff' steps or when a value is obtained, whichever comes first. The default value of `cutoff' is +inf.0. If the program does not terminate and `cutoff' is infinite, this procedure does not terminate. > (count s e [cutoff]) : semantics * source-expression [* nat] -> nat Counts the number of reduction steps in the reduction sequence to evaluate a gradually typed program. Reduction stops after `cutoff' steps or when a value is obtained, whichever comes first. The default value of `cutoff' is +inf.0. This procedure is typically faster than taking the _length_ of the result of _trace_. If the program does not terminate and `cutoff' is infinite, this procedure does not terminate. > (pretty s e [cutoff]) : semantics * source-expression [* nat] -> any Pretty-prints a program trace for a gradually typed program to the current output port. Reduction stops after `cutoff' steps or when a value is obtained, whichever comes first. The default value of `cutoff' is +inf.0. If the program does not terminate and `cutoff' is infinite, this procedure does not terminate. EXAMPLES ------------------------------------------------------------- > omega : source-expression The (non-terminating) expression omega. > untyped-example : source-expression A simple dynamically typed expression. > typed-example : source-expression A simple statically typed expression. > cormacs-example : source-expression A gradually typed program using the untyped Y combinator. > even/odd : source-expression A simple program with mutual recursion. > (tail-recursion-example size) : nat -> source-expression Creates a tail-recursive program with `size' tail-recursive calls, demonstrating the lack of space safety w.r.t. tail recursion for naive gradual typing. > (cast-growth-example size) : nat -> source-expression Creates a program with a function proxy growing on the order of `size', demonstrating the lack of space safety w.r.t. proxy size for naive gradual typing. > (time-complexity-example size) : nat -> source-expression Creates a program with `size' tail-recursive calls and a proxy growing without bound, demonstrating the lack of time safety w.r.t. dynamic checks resulting from proxies in native gradual typing. gui.ss ------ > (graph s e [cutoff]) : semantics * source-expression [* nat] -> any Produces a GUI window with a reduction graph for a gradually typed program. The valueof `cutoff' is used to parameterize the _reduction-steps-cutoff_ parameter to PLT Redex. The default value of `cutoff' is +inf.0. > (step s e) : semantics * source-expression -> any Produces a stepper GUI for stepping through a gradually typed program. EXAMPLE SHELL ONE-LINERS --------------------------------------------- % mzscheme -mvP lambda-gradual dherman -e '(pretty st untyped-example)' % mzscheme -mvP lambda-gradual dherman -e '(pretty st (cast-growth-example 5))' % mzscheme -mvP lambda-gradual dherman -e '(pretty htf (cast-growth-example 5))' % mzscheme -mvP lambda-gradual dherman -e '(printf "~a~n" (count st (time-complexity-example 10)))' % mzscheme -mvP lambda-gradual dherman -e '(printf "~a~n" (count htf (time-complexity-example 10)))'