# Computer Laboratory

Technical reports

# Some types with inclusion properties in ∀, →, μ

Jon Fairbairn

June 1989, 10 pages

## Abstract

This paper concerns the ∀, →, μ type system used in the non-strict functional programming language Ponder. While the type system is akin to the types of Second Order Lambda-calculus, the absence of type application makes it possible to construct types with useful inclusion relationships between them.

To illustrate this, the paper contains definitions of a natural numbers type with many definable subtypes, and of a record type with inheritance.

PDF (0.2 MB)

## BibTeX record

@TechReport{UCAM-CL-TR-171,
author =	 {Fairbairn, Jon},
title = 	 {{Some types with inclusion properties in $\forall$,
$\rightarrow$, $\mu$}},
year = 	 1989,
month = 	 jun,
url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-171.pdf},
institution =  {University of Cambridge, Computer Laboratory},
number = 	 {UCAM-CL-TR-171}
}