Lambda-Gradual

_Lambda-Gradual_
_lambda-gradual_

This collection provides one file:

 _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.