Department of Computer Science and Technology

Technical reports

Design and implementation of a simple typed language based on the lambda-calculus

Jon Fairbairn

May 1985, 107 pages

This technical report is based on a dissertation submitted December 1984 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Gonville & Caius College.

DOI: 10.48456/tr-75

Abstract

Despite the work of Landin and others as long ago as 1966, almost all recent programming languages are large and difficult to understand. This thesis is a re-examination of the possibility of designing and implementing a small but practical language based on very few primitive constructs.

The text records the syntax and informal semantics of a new language called Ponder. The most notable features of the work are a powerful type-system and an efficient implementation of normal order reduction.

In contrast to Landin’s ISWIM, Ponder is statically typed, an expedient that increases the simplicity of the language by removing the requirement that operations must be defined for incorrect arguments. The type system is a powerful extension of Milner’s polymorphic type system for ML in that it allows local quantification of types. This extension has the advantage that types that would otherwise need to be primitive may be defined.

The criteria for the well-typedness of Ponder programmes are presented in the form of a natural deduction system in terms of a relation of generality between types. A new type checking algorithm derived from these rules is proposed.

Ponder is built on the λ-calculus without the need for additional computation rules. In spite of this abstract foundation an efficient implementation based on Hughes’ super-combinator approach is described. Some evidence of the speed of Ponder programmes is included.

The same strictures have been applied to the design of the syntax of Ponder, which, rather than having many pre-defined clauses, allows the addition of new constructs by the use of a simple extension mechanism.

Full text

PDF (0.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-75,
  author =	 {Fairbairn, Jon},
  title = 	 {{Design and implementation of a simple typed language based
         	   on the lambda-calculus}},
  year = 	 1985,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-75.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-75},
  number = 	 {UCAM-CL-TR-75}
}