Technical reports
Some types with inclusion properties in ∀, →, μ
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} }