A Type-preserving Interpreter for Simply Typed Lambda-Calculus

• Main Author: Hongwei Xi
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Subjects: Harper; Haskell; Lambda; Tofte; DML
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.2708; http://www.ececs.uc.edu/~hwxi/academic/papers/TPINT.ps

Dependent ML (DML) is an extension of ML with a restricted form of dependent types where type index objects are drawn from some given constraint domain. In this paper, we present an implementation in DML which implements a type-preserving interpreter for the simply typed lambda-calculus. The most significant feature of this implementation is that we can establish in the type system of DML that the implementation is type-preserving. 1 Introduction Pattern matching is an important feature in many functional programming languages such as Standard ML (Milner, Tofte, Harper, and MacQueen 1997) and Haskell (Hudak, Peyton Jones, and Wadler 1992). The mechanism that supports pattern matching is based on userdeclared datatypes, which can be model with free algebra. In practice, we often encounter situations where the declared datatypes cannot accurately capture what we really need. For instance, if what we need is a data structure for the pairs of integer lists of the same length, the best app.