George Kuan, David MacQueen, and Robert Bruce Findler
When students begin to 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 paper, we begin to build the theoretical underpinnings for treating type checking in a manner much 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.
We first introduce the idea for the simply-typed lambda calculus, and follow up with type inference and let-bound polymorphism. For the latter two systems we start with a simple, intuitive model that, if implemented directly, would be tremendously inefficient. Then, we refine those models and show how to handle them efficiently, all without leaving the basic operational model.
PLT Redex Implementation [For Redex v3.26, For Redex v2]
The run the implementation, please download the latest version of DrScheme.
Master's Paper (Expanded Version of Conference Paper)