Department of Computer Science and Technology

Technical reports

Some types with inclusion properties in ∀, →, μ

Jon Fairbairn

June 1989, 10 pages

DOI: 10.48456/tr-171

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.

Full text

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 = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-171.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-171},
  number = 	 {UCAM-CL-TR-171}
}