Defunctionalization with dependent types

Source Language (CC)

Target Language (DCC)

Context Label Context
Type Context
Term Term
Type
(Output) 		Type
(Output)
Examples
Identity Identity application Non-dependent composition Fully dependent composition Eta-equivalence
Free-variables in types New function in type Dependent pair

Syntax

Variables and universes
Variable names may use lower- and upper-case letters, numbers, underscores(_), and quotation marks('), and must begin with a letter.
Universes are U0, U1, etc.

Pi types
Pi types are Pi x:A.M. Write A -> B for non-dependent types, which are interpreted as Pi _:A.B.

Lambdas and applications
Lambda abstractions are \x:A.M. Applications in CC are M N; applications in DCC are M @ N.

Type contexts
Type contexts are x1:A1, x2:A2, ... , xn:An.

Label contexts
An entry in the label context is L({x1:A1, ... , xn:An}, x:A --> M:B). Entries in the label context are separated with commas.

Unicode
Support λ, Π, → for \, Pi, -> .

Let-bindings
An experimental let-binding syntax let x=M in N is supported for illustration purpose.
Note: the let-binding is interpreted as N[M/x], so, it might accept nonsense programs like let x=nonsense in U0.