λL: A Calculus for Intensional Type Analysis and Generative Types

Ad-hoc polymorphism allows functions to vary their execution according to their type arguments. There are two different forms of ad-hoc polymorphism; with the nominal form, the execution of an operation is determined solely by the name of the type argument, whereas with the structural form, operations are defined by case analysis on the structure of types.

The two approaches treat user-defined types differently. Operations defined by the nominal approach are considered ``open''---the programmer can add cases for new types without modifying existing code. The operations must be extended however with specialized code for the new types, and it may be tedious and even difficult to add extensions that apply to a potentially large universe of user-defined types. On the other hand, structurally defined operations apply in a straightforward way to new types by treating them as equal to their underlying definitions, so no new cases for new types are necessary. However this form is considered ``closed'' to extension, as the behaviour of the operations cannot be differentiated for the new types. This form destroys the distinctions that user-defined types are designed to express.

Both approaches have their benefits, so it is important to provide both capabilities in a single language that is expressive enough to decouple the ``openness'' issue from the way that user-defined types are treated. The λ<sub>L</sub> language achieves this goal by supporting both forms of ad-hoc polymorphism. Among the language features are the ability to define both ``open'' and ``closed'' operations with a single mechanism, the ability to naturally restrict the domain of type-analyzing operations, and new mechanisms for defining higher-order polytypism and manipulating generative type definitions.

In principle, the language is an explicitly typed calculus based on the ω-order polymorphic λ-calculus, augmented with an extensible type analysis operator and new type definitions.

Even though this language is intended to be an intermediate representation for languages that support type-directed operations, we have also developed a surface language that exposes the advanced characteristics of λ_L.

• Stephanie Weirich
• Dimitrios Vytiniotis
• Geoffrey Washburn

• Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich. An Open and Shut Typecase. TLDI 2005. September 2004. (ps)
• Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich. An Open and Shut Typecase. UPenn CIS Technical Report MS-CIS-04-26. November 2004. (ps)

A current implementation, including most of the examples in the paper and other examples, can be found in:

• itaname-impl.tar.gz

The implementation requires an installation of the OCaml system and also includes a Vim syntax file. The syntax of the language is very close to the actual calculus. Here are some characteristic examples of programs written in the language

• count.ita:

  Counting the number of integers in a data structure.

• equality.ita:

  Extensible equality examples.

• examples.ita:

  Various examples, including flavors of type-safe casts.

• extensibletypesafecast.ita:

  A rather complex extensible higher-order based type-safe cast.

• fancycount.ita:

  Hinze's higher-order based counter of useful data inside a complex data structure.