Encoding types in ML-like languages

1Citations
Citations of this article
10Readers
Mendeley users who have this article in their library.

Abstract

This article presents several general approaches to programming with type-indexed families of values within a Hindley-Milner type system. A type-indexed family of values is a function that maps a family of types to a family of values. The function performs a case analysis on the input types and returns values of possibly different types. Such a case analysis on types seems to be prohibited by the Hindley-Milner type system. Our approaches solve the problem by using type encodings. The compile-time types of the type encodings reflect the types themselves, thereby making the approaches type-safe, in the sense that the underlying type system statically prevents any mismatch between the input type and the function arguments that depend on this type. A type encoding could be either value-dependent, meaning that the type encoding is tied to a specific type-indexed family, or value-independent, meaning that the type encoding can be shared by various type-indexed families. Our first approach is value-dependent: we simply interpret a type as its corresponding value. Our second approach provides value-independent type encodings through embedding and projection functions; they are universal type interpretations, in that they can be used to compute other type interpretations. We also present an alternative approach to value-independent type encodings, using higher-order functors. We demonstrate our techniques through applications such as C printf-like formatting, type-directed partial evaluation, and subtype coercions. © 2003 Elsevier B.V. All rights reserved.

Cite

CITATION STYLE

APA

Yang, Z. (2004). Encoding types in ML-like languages. In Theoretical Computer Science (Vol. 315, pp. 151–190). https://doi.org/10.1016/j.tcs.2003.11.017

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free