A Rewriting Semantics for Type Inference

George Kuan. 23 March, 2007.
Communicated by Dave MacQueen.
Supersedes: TR-2007-01 (updated 03/23/07)


When students first learn programming, they often rely on a simple operational model of a programís behavior to explain how particular features work. Because such models build on their earlier training in algebra, students find them intuitive, even obvious. Students learning type systems, however, have to confront an entirely different notation with a different semantics that many find difficult to understand.

In this work, I begin to build the theoretical underpinnings for treating typechecking in a manner like the operational semantics of execution. Intuitively, each term is incrementally rewritten to its type. For example, each basic constant rewrites directly to its type and each lambda expression rewrites to an arrow type whose domain is the type of the lambdaís formal parameter and whose range is the body of the lambda expression which, in turn, rewrites to the range type.

Original Document

The original document is available in PDF (uploaded 23 March, 2007 by Dave MacQueen).