mps-coderules/docs/content/example-lambdacalc.md

layout	title	menu	parent	weight	github-path
page	Typechecking Simply Typed Lambda Calculus	Typechecking STLC	examples	550	/tree/master/samples/lambdacalc

Typechecking STLC

Simply Typed Lambda Calculus is a famous example found in almost every textbook on type checking. This sample demonstrates how a classical type checking algorithm (Hindley-Milner¹) designed specifically for this language can be implemented using code rules. This sample has also been demonstrated in an article² published online.

For purposes of keeping this sample small, we keep the language confined to boolean values. Aside of boolean constants true and false, the mandatory lambda abstraction and application, let-in expression, and if-then-else, we have in addition defined fix operator to support recursion.

The dataform table contains obvious declarations for the only primitive type bool, the functional fun type, and universal type forall. The macros table responsible for constructing dataform instances is trivial.

(dataform table)

There is only one query of kind TYPECHECK, which launches types recovery. All the type checking is done by the automatic productions «on start».

Handlers are separated into types recovery, operations with universal type, and the rest, which is assigning types to expressions. Type checking follows the program’s syntactic structure.

(typing rule for lambda variable binding)

A variable introduced by lambda abstraction is assigned a type, which is a fresh logical variable.

(typing rule for lambda abstration)

A lambda expression is assigned a function type. This rule is a direct translation of the theoretic rule for lambda abstraction.

(typing rule for application expression)

Similarly, the type of an application expression is pretty much follows the standard textbook form with a notable addition of the else branch: this is the way errors are caught in case unification fails. Here, inst constraint ensures a universal type is unwrapped and the inner type dataform is copied, so that all free variables in the resulting type are fresh.

(typing rule for if-then-else)

The type checking for if-then-else ensures that the types of both branches unify, and assigns the resulting unified type to the whole expression.

(typing rule for fix operator)

Finally, the fix operator, which represents general recursion, is given the type forall.(a -> a) -> a.

A separate handler is dedicated to producing and instantiating universal type instances, which are represented by Forall() dataform.

(rule producing forall type)

This production assigns the output parameter G a new type universal type wrapping the T parameter.

(rule instantiating forall type)

The constraint inst is responsible for unwrapping (instantiating) an universal type. Here the copyOf() is a call to internal API, which makes a copy of the term passed as parameter, ensuring all logical variables within it are replaced with fresh ones.

The handler recover is responsible for translating the calculated types to SNode form and is pretty straightforward.

(recover var type)

The constraint varname is used to track the names of type variables, so that the resulting types have the form t1, t2, and so on.

(recover var type assigning name)

The above production ensures all free logical variables representing type variables are assigned unique name.

---

1. See for example: Cardelli, Luca. "Basic polymorphic typechecking." Science of computer programming 8.2 (1987): 147-172. ↩︎

2. Type Checking Lambda Calculus: https://github.com/fisakov/typechecking-lambdacalc ↩︎