Computing at Glasgow University
Paper ID: 9276
DCS Tech Report Number: TR-2006-305

Subtyping between Standard and Linear Function Types

Publication Type: Tech Report (internal)
Appeared in: DCS Technical Report Series
Page Numbers :
Publisher: Dept of Computing Science, University of Glasgow
Year: 2006

As an abstraction of functional programming languages in which certain runtime entities are required to be uniquely referenced, we define a lambda-calculus with both linear and standard data types and consequently both linear and standard function types. We use a single syntax for both linear and standard functions, and rely on the typechecker to produce a linear function type only when necessary. To compensate for the typechecker's preference for standard function types, we include a subtyping relation in which the standard function type is a subtype of the linear function type. We prove that typing guarantees unique references to values of linear data types, that typing is preserved by the operational semantics, and that the typechecking algorithm is sound and complete with respect to the declarative typing rules.

Keywords: functional programming, linear types, subtyping

PDF Bibtex entry Endnote XML