Intensional Polymorphism in Type-Erasure Semantics

Karl Crary  Stephanie Weirich  Greg Morrisett

Cornell University

Abstract

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks; it requires duplication of constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion.

We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place thereby avoiding certain betaexpansions required by other frameworks.

1 Introduction

Type-directed compilers use type information to enable optimizations and transformations that are impossible (or prohibitively difficult) without such information [12, 10, 16, 1, 22, 24, etc.]. However, type-directed compilers for some languages such as Modula-3 and ML face the difficulty that some type information cannot be known at compile time. For example, polymorphic code in ML may operate on inputs of type α where α is not only unknown, but may in fact be instantiated by a variety of different types.

In order to use type information in contexts where it cannot be provided statically, a number of advanced implementation techniques process type information at run time [10, 16, 27, 18, 24]. Such type information is used in two ways: behind the scenes, typically by tagfree garbage collectors [27], and explicitly in program code, for a variety of purposes such as efficient data representation and marshalling [16, 10]. In this paper we focus on the latter area of applications.

To lay a solid foundation for programs that analyze types at run time, Harper and Morrisett devised an internal language, called λi^{ML}, that supports the first-class intensional analysis^{1} of types (following earlier work by Constable [2, 3]). The λi^{ML} language and its derivatives were then used extensively in the high-performance ML compilers TIL/ML [26, 19] and FLINT [25]. The primary novelty of λi^{ML} is the presence of “typecase” operators at the level of terms and types, that allow computations and type expressions to depend upon the values of other type expressions at run time.

Supporting intensional type analysis (and the use of type information at run time in general) seems to require semantics where types are constructed and passed to polymorphic functions during computation. However, there are a number of practical and theoretical reasons why type-passing is unattractive:

• A type-passing language such as λi^{ML} requires that type information always be constructed and passed to polymorphic functions. This can result in considerable overhead if types are rarely examined at run time, and, as we discuss later, it makes abstraction impossible.

• Type passing results in considerable complexity in language semantics, due in large part to the number of semantic devices that must be duplicated for both terms and types. For example, in semantics that make memory allocation explicit [17, 18] a central device is a formal heap in which data is stored; in a type-erasure framework one such heap suffices, but when types are passed it is necessary to add a second heap (and all the attendant machinery) for type data.

1“Intensional” since types are analyzed by the structure of their names, rather than by what terms they contain. This is critical for practicality.

• Type passing also greatly complicates low-level intermediate languages, again due in large part to the duplication of computational devices at the type level, and also to the need to support mixed-phase devices (constructs with both type and term level components). This can pose a serious problem for typed intermediate languages, because these devices can disrupt the essential symmetries on which elegant type systems depend. For example, a typepassing semantics for Typed Assembly Language [20] requires additional instructions for allocating and initializing types, which in turn requires the typing machinery for allocation and initialization to be lifted an additional level into the kind structure.

• As a particularly important example of the preceding issue, type passing severely complicates typed closure conversion (compare the type-passing system of Minamide et al. [14] to the type-erasure system of Morrisett et al. [20]). In a type-erasure framework, the partial application of a polymorphic function to a type may still be considered a value (since the application has no run-time significance), which means that closed code may simply be instantiated with its type environment when a closure is created. In a type-passing framework, the instantiation with a type environment can have some run-time effect, so it must be delayed until the function is invoked. Consequently, closures must include a type environment, necessitating complicated mechanisms including abstract kinds and translucent types [14].

In this paper we propose a typed calculus, called λ_{R}, that ameliorates the problems of type passing without sacrificing intensional type analysis. If run-time type dispatch is to be supported, then clearly on some level types must be passed. The fundamental idea behind our approach is to construct and pass terms that represent types instead of the types themselves. The connection between a type τ and its term representation e is made in the static semantics by assigning e the special type R(τ). Semantically, we may interpret R(τ) as a singleton type that contains only the representation of τ.

This framework resolves the difficulties with type passing semantics discussed above. In particular, as representations of types are simply terms, we can use the pre-existing term operations to deal with run-time type information in languages and their semantics. Furthermore, we can eliminate the difficulties associated with polymorphic closure conversion, as we show in Section 4. Finally, our approach enables the choice not to pass representations. In turn, this allows us to eliminate the overhead of constructing and passing representations of types where it is not necessary.

Perhaps more importantly, the ability not to pass types allows abstraction and parametricity to be recovered. In most type systems abstraction may be achieved by hiding the identity of types either through parametric polymorphism [21] or through existential types [15]. However, when all types are passed and may be analyzed (as in λi^{ML}), the identity of types cannot be hidden and consequently abstraction is impossible. In contrast, in λ_{R} a type can be analyzed only when its representation is available at run time, so abstraction can be achieved simply by not supplying type representations.

For example, consider the type ∃α.α. When all types may be analyzed, this type implements a dynamic type; an expression of this type provides an object of some unknown type, and that unknown type’s identity can be determined at run time by analyzing α. In λ_{R}, as in most other type systems, this implements an abstract type (in this particular example, a useless abstract type), because no representation of α is provided. Dynamic types are implemented in λ_{R} by including a representation of the unknown type, as in ∃α. R(α) × α.

1.1 Expressiveness

In the interest of clarity of presentation, we express λ_{R} as an extension of Harper and Morrisett’s λi^{ML} and focus on their differences. The principal difference is the restriction of type analysis to those types for which representations are provided. This does not diminish the expressiveness of our calculus; λi^{ML} may be translated in a straightforward syntax-directed manner into λ_{R}.

Moreover, the λ_{R} calculus incorporates an additional improvement in expressiveness over λi^{ML} that is independent of explicit type passing: In λi^{ML}, information gained by analyzing a type is not propagated to other variables having that type. Consequently, when analyzing a type α with the interest of processing an object with type α, it is necessary to create a function with argument type α and then apply that function to the object of interest. In other words, the type system of λi^{ML} requires the use of beta-expansions that are not operationally necessary. In λ_{R} we resolve this shortcoming by strengthening the typing rule for typecase so that it refines types in place.

1.2 Overview

The remainder of this paper is organized as follows: In Section 2 we review the λi^{ML} calculus. We then present, in Section 3, our λ_{R} calculus and discuss its formal semantics, including representation terms, R-types, and the strengthened typecase rule. In Section 4, we discuss the simplification of polymorphic closure conversion by explicit type passing. We end with related work and conclusions in Sections 5 and 6. In the appendices we relate our typed semantics to an untyped one through type erasure (Appendix A), discuss the analysis of quantified types (Appendix B), and provide the complete dynamic and static semantics.

2 Intensional Type Analysis

Suppose we wanted to store an array of booleans. Most computer architectures require that memory accesses are a word at a time, but it is a terrible waste of space to store booleans as integers. The solution is to “pack” 32 booleans into one word and use bit manipulations to retrieve the correct value. So, to subscript from a boolean array, we would use the following function:

  val bitsub :  array[int] * int -> bool =
    fn (a,i) =>
      sub(a,i div 32) && (1<<(i mod 32)) <> 0

This is fine when we know a given array contains boolean values, but we would like code that is polymorphic over the type of array to be able to use this mechanism. In essence, we need to define a new array constructor, PackedArray, which will produce an array of integers to hold booleans, and an ordinary array for other types. We also need an associated subscript operation, packedsub, so that when the array is of booleans, bitsub is called. This can be done with intensional type analysis, where in both cases an argument type is examined with a “typecase” form:

type PackedArray[α] =
  Typecase α of
    bool => array[int]
    |   => array[α]
val packedsub : ∀α. PackedArray[α] * int -> α =
  Fn [α] =>
    typecase α of
      bool => bitsub
      |   => sub

2.1 The λi^{ML} calculus

To formalize the tools of intensional type analysis, we begin by summarizing Harper and Morrisett’s λi^{ML} calculus [10]. The λi^{ML} calculus provides these tools in a form that is relatively simple, but already quite powerful.

The syntax of λi^{ML} appears below (modified slightly for presentation). The backbone of λi^{ML} is a predicative variant of Girard’s F_{ω} [8, 7] in which the quantified type ∀α:κ.σ ranges only over type constructors and “small” types (i.e., monotypes), which do not include the quantified types. The type analysis operators are Typerec and typecase at the constructor and term levels.

(kinds) κ :: = Type | κ_{1} → κ_{2}
(con′s) c :: = α | int | c_{1} → c_{2} | c_{1} × c_{2} |

λα:κ.c | c_{1}c_{2} |

                                                                       Typerec c (c_{int}, c_{→}, c_{×})

(types) σ :: = c | σ_{1} → σ_{2} | σ_{1} × σ_{2} | ∀α:κ.σ
(terms) e :: = x | i | λx:σ.e | fix f:σ.v | e_{1}e_{2} |

⟨e_{1}, e_{2}⟩ | π_{1}e | π_{2}e |

Λα:κ.v | e[c] |

                                                                       typecase[α.σ] c of

int ⇒ e_{int} β → γ ⇒ e_{→} β × γ ⇒ e_{×}

(values) v :: = x | i | λx:σ.e | fix x:σ.v |

⟨v_{1}, v_{2}⟩ | Λα:κ.v

Occasionally, for brevity, we will write typecase terms as typecase[α.σ] c (e_{int}, βγ.e_{→}, βγ.e_{×}).

As an example of the use of type analysis in λi^{ML}, consider the function tostring, presented in Figure 1. With the addition of another base type, string, to the language, this function uses typecase to produce a string representation of a data object. For example, the call tostring [int] 3 returns the string “3”. As we cannot provide any information about the implementation of functions, we just return the word “function” when one is encountered, as in the call:

tostring [(int → int) × int] ⟨λx:int. x + 1, 3⟩

which returns “⟨function, 3⟩”.

When the argument to tostring is a product type, the function calls itself recursively. In this branch, the type variables β and γ are bound to the types of the first and second components of the tuple, so that the recursive call can be instantiated with the correct type.

fix tostring : (∀α:Type. α → string).

Λα:Type.

typecase[δ.δ → string] α of int ⇒ int2string string ⇒ λobj :string.obj β → γ ⇒

λobj :(β → γ)."function" β × γ ⇒

λobj :(β × γ).

"<"^(tostring[β](π_{1} obj ))^ ","^(tostring[γ](π_{2} obj ))^">"

Figure 1: The function tostring

The typecase form also has a type annotation to make it possible to type check it without type inference; the annotation [α.σ] indicates that given a type argument τ, the typecase computes a value with type σ[τ/α] (where this denotes the capture-avoiding substitution of τ for α in σ). In this example, each arm returns a function from δ to string, where δ is replaced by the appropriate type, such as int in the int branch, and β × γ in the product branch.

With this intuition, the typing rule for typecase is the natural one (but we will see that this is somewhat restrictive):

Γ ⊢ c : Type Γ, α:Type ⊢ σ type Γ ⊢ e_{int} : σ[int/α] Γ, β:Type, γ:Type ⊢ e_{→} : σ[β → γ/α] Γ, β:Type, γ:Type ⊢ e_{×} : σ[β × γ/α]

Γ ⊢ (\begin{matrix}typecase[α.σ] c of \\ int ⇒ e_{int} \\ β → γ ⇒ e_{→} \\ β × γ ⇒ e_{×} \end{matrix}) : σ[c/α]

Often, to compute the result type σ of a typecase expression the constructor-level Typerec on the argument α will be required. Typerec allows the creation of new types by similar intensional analysis. Several examples of this appear in Harper and Morrisett [10], including type-directed data layout, marshalling and unboxing.

While recursion in the term-level typecase is handled by fix, at the the constructor level there is no such mechanism. For this reason, Typerec is essentially a “fold” operation (or catamorphism) over inductively defined types. It provides primitive recursion by calling itself recursively on all of the components of the argument type. Also unlike typecase, where the branches explicitly bind arguments for the components of the type, the c_{→} and c_{×} branches of Typerec are constructor functions. For example, if the argument of a Typerec operation is c_{1} × c_{2}, then that operation reduces to its c_{×} branch (a constructor function of four arguments) applied to the components c_{1} and c_{2}, and to the result of recursively computing the Typerec operation on those components.

Typerec (c_{1} × c_{2}) (c_{int}, c_{→}, c_{×}) =
c_{×} c_{1} c_{2}
(Typerec c_{1} (c_{int}, c_{→}, c_{×}))
(Typerec c_{2} (c_{int}, c_{→}, c_{×}))

The kinding rule for Typerec is again the natural one. To compute a constructor of kind κ, present a type argument and three branches returning κ constructors:

Γ ⊢ c : Type Γ ⊢ c_{int} : κ
Γ ⊢ c_{→} : Type → Type → κ → κ → κ
Γ ⊢ c_{×} : Type → Type → κ → κ → κ
Γ ⊢ Typerec c (c_{int}, c_{→}, c_{×}) : κ

3 The λ_{R} calculus

Figure 2 presents the syntax of λ_{R}, which we describe in detail in the following section.

(kinds) κ ::= Type | κ → κ
(con′s) c ::= int | α | λα:κ.c | c_{1}c_{2} | c_{1} → c_{2} |

c_{1} × c_{2} | ∀α:κ.c | ∃α:κ.c | R(c) | Typerec c (c_{int}, c_{×}, c_{→}, c_{R}, c_{∀}, c_{∃})

(terms) e ::= x | i | ⟨e_{1}, e_{2}⟩ | π_{1}e | π_{2}e | e_{1}e_{2} |

e[c] | λx:c.e | Λα:κ.v | fix f:c.v |

                                                                     pack e as ∃α.c_{1} hiding c_{2} |

unpack ⟨α, x⟩ = e_{1} in e_{2} |

R_{int} | R_{→}(e_{1}, e_{2}) | R_{×}(e_{1}, e_{2}) | R_{R}(e) | R_{∀}(c) | R_{∃}(c) |

                                                                     typecase[δ.c] e of
                                                                       R_{int} ⇒ e_{int}

R_{→}(x, y) as (β → γ) ⇒ e_{→} R_{×}(x, y) as (β × γ) ⇒ e_{×} R_{R}(x) as R(β) ⇒ e_{R} R_{∀} ⇒ e_{∀} R_{∃} ⇒ e_{∃}

(values) v ::= x | i | ⟨v_{1}, v_{2}⟩ | v[c] |

λx:c.e | Λα:κ.v | fix f:c.v |

                                                                     pack v as ∃α.c_{1} hiding c_{2} |

R_{int} | R_{→}(v_{1}, v_{2}) | R_{×}(v_{1}, v_{2}) | R_{R}(v) | R_{∀}(c) | R_{∃}(c)

Figure 2: Syntax of λ_{R}

3.1 Term Representations of Types

The key feature we add to the term language of λ_{R} is the representations of types as terms, which remain when the types themselves are ultimately erased. The base type, int, has a corresponding representation constant R_{int}. Likewise, inductive types have inductively defined representations; the type int → int is represented by the term R_{→}(R_{int}, R_{int}).

Accordingly, the argument to the term level typecase is the representation of a type, instead of a type. For example, if the argument e is of the form R_{→}(e_{1}, e_{2}), the arrow branch (e_{→}) is taken. The type variables β and γ are still bound to the types that e_{1} and e_{2} represent, but, because we need not only the component types but also their representations, x and y are bound to to e_{1} and e_{2}. This is reflected in the following rule of the operational semantics:

typecase[δ.c] (R_{→}(e_{1}, e_{2})) (e_{int}, βγxy.e_{→}, …)
↦ e_{→}[D(e_{1}), D(e_{2}), e_{1}, e_{2}/β, γ, x, y]

The operation D(·) in this rule converts a representation to the type that it denotes (Appendix, Figure 5). The rest of our dynamic semantics is formalized in Figure 4. It is presented as a call-by-value, small step operational semantics.

In order to assign a type to these representations of types, we have extended the type level of λ_{R} with the R construct, where the representation of a type τ is given the type R(τ), and extended the static semantics accordingly. For example, the formation rule for the representation of function types is

\begin{matrix}Γ ⊢ e_{1} : R(τ_{1}) & Γ ⊢ e_{2} : R(τ_{2}) \\ Γ ⊢ R_{→}(e_{1}, e_{2}) : R(τ_{1} → τ_{2}) \end{matrix} (rep_{→})

which says that if the two subterms, e_{1} and e_{2}, are type representations of τ_{1} and τ_{2}, then R_{→}(e_{1}, e_{2}) will be a representation of τ_{1} → τ_{2}.

As an example of the use of λ_{R}, the tostring function from the previous section can be transliterated into λ_{R} by requiring it to take an additional term argument, x_{α} for the representation of the argument type:

fix tostring : (∀α:Type. R(α) → α → string).

Λα:Type. λx_{α}:R(α).

typecase[δ.α → string] x_{α} of R_{int} ⇒ int2string R_{string} ⇒ λobj :string.obj R_{→}(x, y) as β → γ ⇒

λobj :β → γ."function"

R_{×}(x, y) as β × γ ⇒

λobj :β × γ.

"<"^(tostring [β] x (π_{1} obj ))^ ","^(tostring [γ] y (π_{2} obj ))^">"

The static semantics we have defined ensures that these R-types are singular types; for each one there is exactly one value which inhabits it. This allows us to express constraints between types and their representations at a very fine level. For instance, in the tostring example, the representation argument must be the representation of the type of the object.

Furthermore, as we have added a new way to form types to the constructor language, we must add another term construct, R_{R}(·), to form the representation of representation types. We also extend typecase with an extra branch to handle these terms and Typerec to handle R-types.

3.2 In-place Refinement of Types

The typing rules of λi^{ML} quite often forces an inefficient use of typecase. In the tostring example in section 2, we were required to create closures in each of the branches of the typecase. It would be more efficient if we could lift the lambdas outside of the typecase and have each branch of the typecase return a string. We could then write this function as:

fix tostring : (∀α:Type. R(α) → α → string).

Λα:Type. λx_{α}:R(α). λ obj :α.

typecase[δ.string] x_{α} of R_{int} ⇒ int2string obj

R_{string} ⇒ obj

R_{→}(x, y) as β → γ ⇒

"function"

R_{×}(x, y) as β × γ ⇒ "<"^(tostring [β] x (π_{1} obj ))^ ","^(tostring [γ] y (π_{2} obj ))^">" The reason we could not do this in λi^{ML} is that we need the type of obj to change based upon which branch of the typecase is selected. All we know in the product branch is that obj is of type α, not a tuple. In order to project from it in the recursive calls, we need to update the type of obj to reflect the fact that we know that α is β × γ in the product branch.

With the right enhancement to the static semantics this is possible. We have held off the discussion of the λ_{R}’s typecase formation rule in order to emphasize this point. The basic idea is that in some cases typecase increases our knowledge of the argument type. We separate the formation rule into situations where typecase gives us new information, such as when the argument is of type R(α), and when it does not, such as when the argument is of type R(τ_{1} → τ_{2}). In the inference rule for type checking a typecase term, when the argument is of type R(α), we refine types containing α to reflect the gain in information, as shown below. For simplicity, only some of the rule is included (the complete rule can be found in Figure 8):

Γ, α:Type, Γ′ ⊢ e : R(α)
Γ, Γ′[int/α] ⊢ e_{int}[int/α] : c[int, ∫ /α, δ]
Γ, β:Type, γ:Type, Γ′[β → γ/α], x:R(β),

y:R(γ) ⊢ e_{→}[β → γ/α] : c[β → γ, β → γ/α, δ]

⋮

Γ, α:Type, Γ′ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, …) : c[α/δ]

For example, to typecheck the e_{→} branch, we substitute β × γ for α everywhere, including the surrounding context.^{2} Consequently the types of the variables bound in the context will be refined by that substitution. Because λi^{ML} only makes this substitution in the return type of the branch, and not in the context, in order to propagate this information one must abstract over all variables of interest.

When we know more about the argument because of the singularity of the R-types, we can deduce statically which branch of the typecase will be taken. Therefore we do not need to typecheck the other branches at all, leading to a much simpler rule. For example, if we know the argument is of type R(τ_{1} → τ_{2}), we only need to examine the e_{→} branch, as in the rule:

\begin{matrix}Γ ⊢ e : R(τ_{1} → τ_{2}) \\ Γ, x:R(τ_{1}), y:R(τ_{2}) ⊢ e_{→}[τ_{1}, τ_{2}/β, γ] : c[τ_{1} → τ_{2}/δ] \end{matrix}

Γ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, …) : c[τ_{1} → τ_{2}/δ]

3.3 Impredicativity

A final minor difference between λ_{R} and λi^{ML} is that we have chosen to make λ_{R} impredicative. We do this because our interest in λ_{R} is for compilation where it is difficult in some cases (such as typed closure conversion,

2The substitution for α is applied within the branches themselves in order to avoid creating a hole in the scope of α. In practice, a typechecker would implement this by a local type definition, rather than by substitution.

\underline{Judgment}  \underline{Meaning}
Γ ⊢ c : κ  c is a valid constructor of kind κ
Γ ⊢ c_{1} = c_{2} : κ c_{1} and c_{2} are equal constructors
Γ ⊢ e : τ  e is a term of type τ

Figure 3: Judgments of λ_{R}

see Section 4) to avoid impredicativity. Also for the support of closure conversion we have added existential types.

So, unlike λi^{ML}, there is no distinction between types and constructors; everything is a constructor. Because of this increase in the number of constructors, Typerec must now include branches for universal and existential types. However, in order to retain strong normalization, this analysis is limited only to the outermost operator, and does not provide any information about the body of the type. We have also added R_{∀} and R_{∃} to the term level to represent these types, and have extended typecase to include branches for them. These constructs are essentially base representations and cannot provide any further information, so typecase as well is limited to the outermost operator. We discuss how to relax this in Appendix B.

3.4 Properties of the Formal Semantics

Formally, the static semantics of λ_{R} consists of a collection of rules for deriving judgments of the forms shown in Figure 3. In these judgments, Γ is a unified type and kind context, mapping either constructor variables (α, β, ...) to kinds, or term variables (x, y, ...) to types. The full formal static and operational semantics of λ_{R} appear in Figures 4–9, and from them we can prove several useful properties about λ_{R}.

First, we would like to prove the decidability of λ_{R} typechecking. The difficult part of the that is equivalence checking for constructors. Based upon the equivalence rules in Figure 7 we can define a notion of constructor reduction to a normal form in an obvious manner. This reduction relation can be proved to be strongly normalizing and confluent (in a manner similar to Morrisett [16]) from which it follows that constructor equivalence is decidable. Therefore we can state the following theorem:

Theorem 3.1 (Decidability) It is decidable whether or not Γ ⊢ e : τ is derivable in λ_{R}.

Next, we would like to show that the static semantics guarantees safety; that is, if a term type checks, then the operational semantics will not get stuck, where a term that is not a value, and for which no rule of our operational semantics applies, is stuck:

Theorem 3.2 (Type Safety) If ∅ ⊢ e : τ and e ↦^{∗} e′ then e′ is not stuck.

The proof of this theorem is standard, relying on the usual progress, subject reduction and substitution lemmas.

4 Polymorphic Typed Closure Conversion

As a final example, we consider typed closure conversion in a λ_{R}-like framework. The key idea behind closure conversion is to shift from a substitution-based model of execution to an environment-based model via a source-to-source translation. In particular, all functions are replaced with explicit closures which are represented within the language as pairs consisting of a λ-abstraction (the code of the closure), and a tuple (the environment of the closure). The environment contains values for the free variables of the function. The code abstracts the environment as well as the arguments of the function and is thus closed. Hence, the code may be hoisted to the top-level, allocated at compile time, and shared among all substitution instances. Application is rewritten so that the code of a closure is first applied to its environment and then to its arguments.

In the monomorphic case no discrepancy arises between type-passing [14] and type-erasure [20] closure conversion. An existential type is used to hold the type of the closure’s environment abstract, so a closure for a τ_{1} → τ_{2} function is given the type ∃α.((τ_{1}×α) → τ_{2})×α.

However, with the introduction of polymorphism, significant differences arise between type-passing and typeerasure. The issue stems from the fact that functions may contain not only free value variables, but also free type variables, and closed code must abstract these as well. Closures must then provide somehow for applying such code to the appropriate type variables. In a type-erasure setting, application to type arguments has no run-time effect, so the partial application of code to the appropriate type variables may be performed when closures are created. Consequently, the possibility of free type variables does not figure into the type of a closure, and so closures have the same type (∃α.((τ_{1} × α) → τ_{2}) × α) as before.

However, in a type-passing semantics, the application to type arguments is a run-time operation and so such applications must be suspended until the closure is called. Thus, it is necessary for the closure to include a type environment as well as a value environment. The kind of the type environment must be hidden (as did the type of the value environment in the monomorphic case), and the closure’s type must enforce the requirement that the code be applied only to the proper type environment (see Minamide et al. [14] for detailed explanations of why). The former requires the use of abstract kinds and the latter requires the use of translucent types [9]. This results in a closure having the considerably more complicated type (again, see Minamide et al. [14] for a formalization of the necessary type theory):

∃k_{tenv}:Kind. ∃α_{venv}:Type. ∃β_{tenv}:k_{tenv}. (∀γ:k_{tenv}=β_{tenv}. (τ_{1} × α_{venv}) → τ_{2}) × α_{venv}

In the above type, k_{tenv} abstracts the kind of the type environment, α_{venv} abstracts the type of the value of the value environment, and β_{tenv} provides the type environment. The code type then takes a type environment γ of kind k_{tenv} as an argument, but γ is constrained (using translucent types) to be the appropriate environment, β_{tenv}.

Since our framework is one of type-erasure, type environments may be resolved by partial application, resulting in the simpler type for closures. However, it is instructive to examine the details. Suppose the function to be closure converted is the function f = λx:τ_{1}.e with type τ_{1} → τ_{2} and suppose further that the function contains free occurrences of the type variable α and its representation x_{α}:R(α).

First the function is rewritten in closed form as:

\begin{aligned}f′ & : & ∀α. (τ_{1} × R(α)) → τ_{2} \\ & = & Λα. λy:(τ_{1} × R(α)). e[π_{1}y, π_{2}y/x, x_{α}] \end{aligned}

Then (at run time) f′ is instantiated with the type environment (that is, α):

f′′ : (τ_{1} × R(α)) → τ_{2} = f′[α]

Finally, a closure is created:

f′′′ = pack ⟨f′′, x_{α}⟩ as ∃β. ((τ_{1} × β) → τ_{2}) × β hiding R(α)

Consider what has become of the mechanisms for typepassing closure conversion: The type of f′′ requires that it be applied (for its second argument) only to the representation of α. So the translucency mechanism appears again, suggesting that translucency is inherent in type-passing closure conversion. However, this version of translucency has two advantages; the necessary type theory is simpler, and the translucency is completely hidden by the existential packaging in the eventual closure. On the other hand, abstract kinds do not appear in the process, suggesting them to be an artifact of true type-passing (but see Appendix B).

5 Related Work

Closely related to our work is the work of Minamide on lifting of type parameters for tag-free garbage collection [13]. Minamide was interested in lifting type parameters out of code so they could be preallocated at compile time. His lifting procedure required the maintenance of interrelated constraints between type parameters to retain type soundness, and he used a system similar to ours that makes explicit the passing of type parameters in order to simplify the expression of such constraints. The principal difference between Minamide’s system and ours is that Minamide did not consider intensional type analysis or first-class polymorphism. Minamide’s system also makes a distinction between type representations (which he calls evidence, following Jones [11]) and ordinary terms, while λ_{R} type representations are fully first-class.

The issue of type parameter lifting is an important one for compilers based on λ_{R}. The construction of type representations at run time would likely lead to significant cost and should in practice be lifted out to compile time whenever possible. (Unfortunately, in the presence of polymorphic recursion, which λ_{R} supports, it cannot always be possible.) Mechanisms for lifting such lifting have been developed by Minamide (in the work discussed above) and by Saha and Shao [23].

Dubois at al. [5] also pass explicit type representations to polymorphic functions when compiling ad-hoc polymorphism. However, their system differs from ours and Minamide’s in that no mechanism is provided for connecting representations to the types they denote, and consequently, information gained by analyzing type representations does not propagate into the type system.

Duggan [6] proposes another typed framework for intensional type analysis that is similar in some ways to λi^{ML}. Like λi^{ML}, Duggan’s system passes types implicitly and allows for the intensional analysis of types at the term level. Duggan’s system does not support intensional type analysis at the constructor level, as λi^{ML} and λ_{R} do, but it adds a facility for defining type classes (using union and recursive kinds) and allows type analysis to be restricted to members of such classes.

6 Conclusions and Future Directions

We have presented a type-theoretic framework that supports the passing and analysis of type information at run time, but that avoids the shortcomings associated with previous such frameworks (e.g., duplication of constructs, lack of abstraction, and complication of closure conversion). This new framework makes it feasible to use intensional type analysis in settings where the shortcomings previously made it impractical.

For example, Morrisett et al. [20] developed typing mechanisms for low-level intermediate and target languages that allow type information to be used all the way to the end of compilation. It would be desirable, in a system based on those mechanisms, to be able to exploit fully that type information using intensional type analysis. Unfortunately, the shortcomings of typepassing semantics made it incompatible with some of those low-level typing mechanisms. This unfortunate incompatibility has made it infeasible to use the mechanisms of Morrisett et al. in type-analyzing compilers such as TIL/ML [26, 19] and FLINT [25], and has made it infeasible to use intensional type analysis in the endto-end typed compiler TALC [20]. This framework in this paper makes it possible to unify these two lines of work for the first time.

In pursuance of this aim, an important direction for future work is to extend the mechanisms of λ_{R} into lowerlevel typed intermediate languages such as typed assembly language [20]. Among the issues to be explored in such research is how to analyze the more complicated types used in typed assembly language, and how to perform type-directed dispatch without an atomic typecase construct. Another issue to explore is better mechanisms for analysis of quantified types (some initial ideas appear in Appendix B), and whether such mechanisms are merited in practice.

Another important question is whether a parametricity theorem like that of Reynolds [21] can be shown for λ_{R}. Polymorphism is clearly non-parametric in λi^{ML}, but the lowering of type analysis to explicit term-level representatives makes it plausible that some sort of parametricity could be shown for λ_{R}. In other words, we discussed at an intuitive level in Section 1 how the explicit passing of types restores the ability to abstract types that was discarded by λi^{ML}; it would be interesting to explore how that intuition may be formalized.

References

[1] L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to von Neumann machines via region representation inference. In Twenty-Third ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 171–183, St. Petersburg, Jan. 1996.

[2] R. L. Constable. Intensional analysis of functions and types. Technical Report CSR-118-82, Department of Computer Science, University of Edinburgh, June 1982.

[3] R. L. Constable and D. R. Zlatin. The type theory of PL/CV3. ACM Transactions on Programming Languages and Systems, 6(1):94–117, Jan. 1984.

[4] J. Despeyroux, F. Pfenning, and Carsten Schürmann. Primitive recursion for higherorder abstract syntax. In Third International Conference on Typed Lambda Calculi and Applications, volume 1210 of Lecture Notes in Computer Science, pages 147–163, Nancy, France, Apr. 1997. Springer-Verlag. Extended version published as Carnegie Mellon University technical report CMU-CS-96-172.

[5] C. Dubois, F. Rouaix, and P. Weis. Extensional polymorphism. In Twenty-Second ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 118–129, San Francisco, Jan. 1995.

[6] D. Duggan. A type-based semantics for userdefined marshalling in polymorphic languages. In Second Workshop on Types in Compilation, Mar. 1998.

[7] J.-Y. Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63–92. North-Holland Publishing Co., 1971.

[8] J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.

[9] R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Twenty-First ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 123–137, Portland, Oregon, Jan. 1994.

[10] R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Twenty-Second ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 130– 141, San Francisco, Jan. 1995.

[11] M. P. Jones. A theory of qualified types. In Fourth European Symposium on Programming, volume 582 of Lecture Notes in Computer Science, Rennes, France, 1992. Springer-Verlag.

[12] X. Leroy. Unboxed objects and polymorphic typing. In Nineteenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 177–188, 1992.

[13] Y. Minamide. Full lifting of type parameters. Submitted for publication. Earlier version published as “Compilation Based on a Calculus for Explicit Type-Passing” in the Second Fuji International Workshop on Functional and Logic Programming, 1996.

[14] Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Twenty-Third ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 271–283, St. Petersburg, Florida, Jan. 1996.

[15] J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470–502, July 1988.

[16] G. Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania, Dec. 1995.

[17] G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In Conference on Functional Programming Languages and Computer Architecture, 1995.

[18] G. Morrisett and R. Harper. Semantics of memory management for polymorphic languages. In A. D. Gordon and A. M. Pitts, editors, Higher Order Operational Techniques in Semantics. Cambridge University Press, 1997.

[19] G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. In Workshop on Compiler Support for Systems Software, Tucson, Feb. 1996.

[20] G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Twenty-Fifth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 85–97, San Diego, Jan. 1998. Extended version published as Cornell University technical report TR97-1651.

[21] J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing ’83, pages 513–523. North-Holland, 1983. Proceedings of the IFIP 9th World Computer Congress.

[22] E. Ruf. Partitioning dataflow analyses using types. In Twenty-Fourth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 15–26, Paris, Jan. 1997.

[23] B. Saha and Z. Shao. Optimal type lifting. In Second Workshop on Types in Compilation, Mar. 1998.

[24] Z. Shao. Flexible representation analysis. In 1997 ACM SIGPLAN International Conference on Functional Programming, pages 85–98, Amsterdam, June 1997.

[25] Z. Shao. An overview of the FLINT/ML compiler. In 1997 Workshop on Types in Compilation, Amsterdam, June 1997. ACM SIGPLAN. Published as Boston College Computer Science Department Technical Report BCCS-97-03.

[26] D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 181–192, May 1996.

[27] A. Tolmach. Tag-free garbage collection using explicit type parameters. In ACM Conference on Lisp and Functional Programming, pages 1–11, Orlando, June 1994.

A Untyped Calculus

Although the formal static and operational semantics for λ_{R} are for a typed language, we would like to emphasize the point that types are unnecessary for computation and can safely be erased. To do this we exhibit an untyped language, λ_{R}^{∘}, a translation of λ_{R} to this language through type erasure, and the following theorem, which states that execution in the untyped language mirrors execution in the typed language:

Theorem A.1 1. If e_{1} ↦^{∗} e_{2} then e_{1}^{∘} ↦^{∗} e_{2}^{∘}.

2. If ∅ ⊢ e_{1} : τ and e_{1}^{∘} ↦^{∗} u then there exists e_{2} such that e_{1} ↦^{∗} e_{2} and e_{2}^{∘} = u.

From this theorem and type safety for λ_{R} it follows that our untyped semantics is safe.

Corollary A.2 If ∅ ⊢ e : τ and e^{∘} ↦^{∗} u then u is not stuck.

A.1 Syntax of Untyped Calculus

(terms) u :: = x | i | λx.u | fix f.w | u_{1}u_{2} |

⟨u_{1}, u_{2}⟩ | π_{1}u | π_{2}u |

R_{int} | R_{→}(u_{1}, u_{2}) | R_{×}(u_{1}, u_{2}) | R_{R}(u) | R_{∀} | R_{∃} |

                                                                   typecase u of
                                                                    R_{int} ⇒ u_{int}

R_{→}(x, y) ⇒ u_{→} R_{×}(x, y) ⇒ u_{×} R_{R}(x) ⇒ u_{R} R_{∀} ⇒ u_{∀} R_{∃} ⇒ u_{∃}

(values) w :: = x | i | ⟨w_{1}, w_{2}⟩ | λx.u | fix f.w |

R_{int} | R_{×}(w_{1}, w_{2}) | R_{→}(w_{1}, w_{2}) | R_{R}(w) | R_{∀} | R_{∃}

A.2 Type Erasure

x^{∘} = x
i^{∘} = i
⟨e_{1}, e_{2}⟩^{∘} = ⟨e_{1}^{∘}, e_{2}^{∘}⟩
(π_{i}e)^{∘} = π_{i}e^{∘}
(λx:c.e)^{∘} = λx.e^{∘}
(Λα:κ.v)^{∘} = v^{∘}
(fix f:c.v)^{∘} = fix f.v^{∘}
(e_{1}e_{2})^{∘} = e_{1}^{∘}e_{2}^{∘}
e[c]^{∘} = e^{∘}

                                                      pack e as c hiding c′^{∘} = e^{∘}

unpack ⟨α, x⟩ = e_{1} in e_{2}^{∘} = (λx.e_{2}^{∘}) e_{1}^{∘}

                                                                   R_{int}^{∘} = R_{int}

R_{→}(e_{1}, e_{2})^{∘} = R_{→}(e_{1}^{∘}, e_{2}^{∘})
R_{×}(e_{1}, e_{2})^{∘} = R_{×}(e_{1}^{∘}, e_{2}^{∘})
R_{R}(e_{1})^{∘} = R_{R}(e_{1}^{∘})
R_{∀}(c)^{∘} = R_{∀}
R_{∃}(c)^{∘} = R_{∃}

                                                       (typecase[δ.c] e of
                                                         R_{int} ⇒ e_{int}

R_{→}(x, y) as

(β → γ) ⇒ e_{→}

R_{×}(x, y) as

(β × γ) ⇒ e_{×}

R_{R}(x) as

R(β) ⇒ e_{R}

R_{∀} ⇒ e_{∀} R_{∃} ⇒ e_{∃})^{∘}

                                                                          = typecase e^{∘}of
                                                                              R_{int} ⇒ e_{int}^{∘}

R_{→}(x, y) ⇒ e_{→}^{∘} R_{×}(x, y) ⇒ e_{×}^{∘} R_{R}(x) ⇒ e_{R}^{∘}

R_{∀} ⇒ e_{∀}^{∘}
R_{∃} ⇒ e_{∃}^{∘}

A.3 Operational Semantics of λ_{R}^{∘}

(λx:c.u)w ↦ u[w/x]
(fix f:c.w)w′ ↦ (w[fix f:c.w/f])w′
π_{1}⟨w_{1}, w_{2}⟩ ↦ w_{1} π_{2}⟨w_{1}, w_{2}⟩ ↦ w_{2}

                                                           typecase R_{int} (u_{int}, xy.u_{×},

xy.u_{→}, x.u_{R}, u_{∀}, u_{∃}) ↦ u_{int}

typecase (R_{∀})) (u_{int}, xy.u_{×}, xy.u_{→}, x.u_{R}, u_{∀}, u_{∃}) ↦ u_{∀}

typecase (R_{∃}) (u_{int}, xy.u_{×}, xy.u_{→}, x.u_{R}, u_{∀}, u_{∃}) ↦ u_{∃}

typecase (R_{×}(w_{1}, w_{2})) (u_{int}, xy.u_{×}, xy.u_{→}, x.u_{R}, u_{∀}, u_{∃}) ↦ u_{×}[w_{1}, w_{2}/x, y]

typecase (R_{→}(w_{1}, w_{2})) (u_{int}, xy.u_{×}, xy.u_{→}, x.u_{R}, u_{∀}, u_{∃}) ↦ u_{→}[w_{1}, w_{2}/x, y]

typecase (R_{R}(w)) (u_{int}, xy.u_{×}, xy.u_{→}, x.u_{R}, u_{∀}, u_{∃}) ↦ u_{R}[w/x]

{u_{1} ↦ u′_{1} \atop u_{1}u_{2} ↦ u′_{1}u_{2}}  {u ↦ u′ \atop wu ↦ wu′}

{u_{1} ↦ u′_{1} \atop ⟨u_{1}, u_{2}⟩ ↦ ⟨u′_{1}, u_{2}⟩}  {u ↦ u′ \atop ⟨w, u⟩ ↦ ⟨w, u′⟩}

{u ↦ u′ \atop π_{1}u ↦ π_{1}u′}  {u ↦ u′ \atop π_{2}u ↦ π_{2}u′}

{u_{1} ↦ u′_{1} \atop R_{→}(u_{1}, u_{2}) ↦ R_{→}(u′_{1}, u_{2})} {u ↦ u′ \atop R_{→}(w, u) ↦ R_{→}(w, u′)}

{u_{1} ↦ u′_{1} \atop R_{×}(u_{1}, u_{2}) ↦ R_{×}(u′_{1}, u_{2})}  {u ↦ u \atop R_{×}(w, u) ↦ R_{×}(w, u′)}

{u ↦ u′ \atop R_{R}(u) ↦ R_{R}(u′)}

u ↦ u′

typecase u (u_{int}, xy.u_{×}, xy.u_{→}, x.u_{R}, u_{∀}, u_{∃}) ↦ typecase u′ (u_{int}, xy.u_{×}, xy.u_{→}, x.u_{R}, u_{∀}, u_{∃})

B Analysis of Quantified Types

The analysis of quantified types in λ_{R}, as presented in this paper, is limited to the outermost operator; that is, a Typerec or typecase will determine that a type is a ∀ or ∃ type, but will not provide any information about the body of the type. The principal reasons for this decision are that support for full analysis of quantified types detracts from the elegance of the type theory, and that experience from the TIL/ML compiler suggests that such support may not be needed in practice. (In fact, the TIL/ML compiler uses a variant of λi^{ML} that handles quantified types in a manner relatively similar to λ_{R}.) In this section we briefly explore what would be required to extend λ_{R} to support full analysis of quantified types.

Adding term-level representations for quantified types is straightforward. The representation for ∀α:κ.c must carry information expressing how to produce the appropriate c given an appropriate α of kind κ. For example, a member of R(∀α:Type.c) would be built by a constructor R_{∀Type} that takes a function with type ∀α:Type. R(α) → R(c). Representations of polymorphic types at any other kind κ would be built by an analogous constructor R_{∀κ} or R_{∃κ}. Note that this requires an infinite collection of such constructors, two for each kind.

Analysis of types is also straightforward if quantification is restricted to Type, or to any finite set of kinds. In that case, the appropriate branches can be added to the Typerec and typecase operations, and each branch would return the appropriate representation function discussed above. General quantification could be handled, at the expense of additional complexity, by adding kind variables, term representations of kinds, and a Kindrec facility for analyzing such representations. With such additions, the quantifier branches would return a kind representation and the appropriate representation function.

However, with such a mechanism in place, the amount of useful analysis that can be performed is still quite limited. Type analyzing code may apply the representation function to an argument and analyze its output, but it could not analyze the function itself. This makes it impossible, for example, to print quantified types. The modal type theory of Despeyroux et al. [4] is intended for precisely this sort of application; it provides mechanisms for primitive recursion on higher-order syntax and might provide a solution to this problem.

Also, allowing any analysis of quantified tyes by Typerec sacrifices strong normalizations of type expressions. (An isomorphism between Type and Type → Type can be built, permitting the encoding of the untyped lambda calculus.) A modal type discipline holds some promise of a solution to this problem as well.

(λx:c.e)v ↦ e[v/x]  (Λα:κ.v)[c] ↦ v[c/α]  π_{1}⟨v_{1}, v_{2}⟩ ↦ v_{1}  π_{2}⟨v_{1}, v_{2}⟩ ↦ v_{2}

(fix f:c.v)v′ ↦ (v[fix f:c.v/f])v′ (fix f:c.v)[c′] ↦ (v[fix f:c.v/f])[c′] unpack ⟨α, x⟩ = (pack v as ∃β.c_{1} hiding c_{2}) in e_{2} ↦ e_{2}[c_{2}, v/α, x] typecase[δ.c] R_{int} (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) ↦ e_{int} typecase[δ.c] (R_{∀}(c′)) (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) ↦ e_{∀} typecase[δ.c] (R_{∃}(c′)) (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) ↦ e_{∃}

typecase[δ.c] (R_{→}(v_{1}, v_{2})) (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) ↦ e_{→}[D(v_{1}), D(v_{2}), v_{1}, v_{2}/β, γ, x, y] typecase[δ.c] (R_{×}(v_{1}, v_{2})) (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) ↦ e_{×}[D(v_{2}), D(v_{2}), v_{1}, v_{2}/β, γ, x, y]

typecase[δ.c] (R_{R}(v)) (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) ↦ e_{R}[D(v), v/β, x]

{e_{1} ↦ e′_{1} \atop e_{1}e_{2} ↦ e′_{1}e_{2}} {e ↦ e′ \atop ve ↦ ve′} {e ↦ e′ \atop e[c] ↦ e′[c]} {e ↦ e′ \atop π_{i}e ↦ π_{i}e′} {e_{1} ↦ e′_{1} \atop ⟨e_{1}, e_{2}⟩ ↦ ⟨e′_{1}, e_{2}⟩} {e ↦ e′ \atop ⟨v, e⟩ ↦ ⟨v, e′⟩}

e ↦ e′

pack e as ∃β.c_{1} hiding c_{2} ↦ pack e′ as ∃β.c_{1} hiding c_{2}

e ↦ e′
unpack ⟨α, x⟩ = e in e_{2} ↦ unpack ⟨α, x⟩ = e′ in e_{2}
e ↦ e′

typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) ↦ typecase[δ.c] e′ (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃})

e_{1} ↦ e′_{1} R_{→}(e_{1}, e_{2}) ↦ R_{→}(e′_{1}, e_{2})
{e ↦ e′ \atop R_{→}(v, e) ↦ R_{→}(v, e′)} {e_{1} ↦ e′_{1} \atop R_{×}(e_{1}, e_{2}) ↦ R_{×}(e′_{1}, e_{2})} {e ↦ e′ \atop R_{×}(v, e) ↦ R_{×}(v, e′)} {e ↦ e′ \atop R_{R}(e) ↦ R_{R}(e′)}

Figure 4: Operational Semantics for λ_{R}

\begin{aligned}D(R_{int}) & = & int \\ D(R_{×}(e_{1}, e_{2})) & = & D(e_{1}) × D(e_{2}) \\ D(R_{→}(e_{1}, e_{2})) & = & D(e_{1}) → D(e_{2}) \\ D(R_{R}(e)) & = & R(D(e)) \\ D(R_{∀}(c)) & = & c \\ D(R_{∃}(c)) & = & c \end{aligned}

Figure 5: Translating representations to types

Γ ⊢ c : κ

Γ ⊢ int : Type (int)  Γ ⊢ α : κ (Γ(α) = κ) (var)  Γ ⊢ c_{1} : Type  Γ ⊢ c_{2} : Type Γ ⊢ c_{1} → c_{2} : Type (arrow)

Γ ⊢ c_{1} : Type  Γ ⊢ c_{2} : Type Γ ⊢ c_{1} × c_{2} : Type (prod)  {Γ, α:κ_{1} ⊢ c : κ_{2} \atop Γ ⊢ λα:κ_{1}.c : κ_{1} → κ_{2}} (fn)  {Γ ⊢ c_{1} : κ_{1} → κ_{2}  Γ ⊢ c_{2} : κ_{1} \atop Γ ⊢ c_{1}c_{2} : κ_{2}} (app)

Γ ⊢ c : Type Γ ⊢ R(c) : Type (R)  Γ, α:κ ⊢ c : Type Γ ⊢ ∀α:κ.c : Type (∀)  Γ, α:κ ⊢ c : Type Γ ⊢ ∃α:κ.c : Type (∃)
Γ ⊢ c : Type  Γ ⊢ c_{int} : κ  Γ ⊢ c_{→} : Type → Type → κ → κ → κ
Γ ⊢ c_{×} : Type → Type → κ → κ → κ  Γ ⊢ c_{R} : Type → κ → κ  Γ ⊢ c_{∀} : κ  Γ ⊢ c_{∃} : κ

Γ ⊢ Typerec c(c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}) : κ

(trec)

Figure 6: Constructor formation

Γ ⊢ c_{1} = c_{2} : κ

\begin{matrix}Γ, α:κ′ ⊢ c_{1} : κ & Γ ⊢ c_{2} : κ′ \\ Γ ⊢ (λα:κ′.c_{1})c_{2} = c_{1}[c_{2}/α] : κ \end{matrix}  {Γ ⊢ c : κ_{1} → κ_{2} \atop Γ ⊢ λα:κ_{1}.cα = c : κ_{1} → κ_{2}} α ∉ Dom(Γ)

Γ ⊢ c_{int} : κ

Γ ⊢ c_{→} : Type → Type → κ → κ → κ Γ ⊢ c_{×} : Type → Type → κ → κ → κ

Γ ⊢ c_{R} : Type → κ → κ  Γ ⊢ c_{∀} : κ  Γ ⊢ c_{∃} : κ
\{ \begin{matrix}Γ ⊢ Typerec(int) (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}) = c_{int} : κ \\ Γ ⊢ Typerec(∀α:κ.c) (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}) = c_{∀} : κ \\ Γ ⊢ Typerec(∃α:κ.c) (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}) = c_{∃} : κ \end{matrix} \}

Γ ⊢ c_{1} : Type  Γ ⊢ c_{2} : Type  Γ ⊢ c_{int} : κ

Γ ⊢ c_{→} : Type → Type → κ → κ → κ Γ ⊢ c_{×} : Type → Type → κ → κ → κ

Γ ⊢ c_{R} : Type → κ → κ  Γ ⊢ c_{∀} : κ  Γ ⊢ c_{∃} : κ

Γ ⊢ Typerec(c_{1} → c_{2}) (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}) =

c_{→} c_{1} c_{2}(Typerec c_{1} (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}))(Typerec c_{2} (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃})) : κ Γ ⊢ Typerec(c_{1} × c_{2}) (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}) =

c_{×} c_{1} c_{2}(Typerec c_{1} (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}))(Typerec c_{2} (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃})) : κ

Γ ⊢ c : Type Γ ⊢ c_{int} : κ

Γ ⊢ c_{→} : Type → Type → κ → κ → κ Γ ⊢ c_{×} : Type → Type → κ → κ → κ

Γ ⊢ c_{R} : Type → κ → κ  Γ ⊢ c_{∀} : κ  Γ ⊢ c_{∃} : κ

Γ ⊢ Typerec (R(c)) (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃}) = c_{R} c (Typerec c (c_{int}, c_{→}, c_{×}, c_{R}, c_{∀}, c_{∃})) : κ

Figure 7: Constructor equivalence (selected rules)

Γ ⊢ e : c

Γ ⊢ i : int (int)  Γ ⊢ x : c (Γ(x) = c) (var)  \begin{matrix}Γ ⊢ e_{1} : c_{1} & Γ ⊢ e_{2} : c_{2} \\ Γ ⊢ ⟨e_{1}, e_{2}⟩ : c_{1} × c_{2} \end{matrix} (pair)  {Γ ⊢ e : c_{1} × c_{2} \atop Γ ⊢ π_{i}e : c_{i}} (sel_{i})
\begin{matrix}Γ ⊢ e_{1} : c′ → c & Γ ⊢ e_{2} : c′ \\ Γ ⊢ e_{1}e_{2} : c \end{matrix} (app)  \begin{matrix}Γ ⊢ e : ∀α:κ.c′ & Γ ⊢ c : κ \\ Γ ⊢ e[c] : c′[c/α] \end{matrix} (tapp)  \begin{matrix}Γ, x:c′ ⊢ e : c & Γ ⊢ c′ : Type \\ Γ ⊢ λx:c′.e : c′ → c \end{matrix} (fn)
{Γ, α:κ ⊢ e : c \atop Γ ⊢ Λα:κ.e : ∀α:κ.c} (tfn)  Γ, f:c ⊢ e : c Γ ⊢ c : Type Γ ⊢ fix f:c. e : c (c = ∀α_{1}:κ_{1} ⋯ α_{n}:κ_{n}.c′ → c′′, n ≥ 0) (fix)
Γ, α:κ ⊢ c : Type Γ ⊢ c′ : κ Γ ⊢ e : c[c′/α] Γ ⊢ pack e as ∃α:κ.c hiding c′ : ∃α:κ.c (pack)  Γ ⊢ e_{1} : ∃α:κ.c′ Γ, α:κ, x:c′ ⊢ e_{2} : c Γ ⊢ unpack ⟨α, x⟩ = e_{1} in e_{2} : c (unpack)
Γ ⊢ R_{int} : R(int) (rep_{int})  \begin{matrix}Γ ⊢ e_{1} : R(c_{1}) & Γ ⊢ e_{2} : R(c_{2}) \\ Γ ⊢ R_{→}(e_{1}, e_{2}) : R(c_{1} → c_{2}) \end{matrix} (rep_{→})  \begin{matrix}Γ ⊢ e_{1} : R(c_{1}) & Γ ⊢ e_{2} : R(c_{2}) \\ Γ ⊢ R_{×}(e_{1}, e_{2}) : R(c_{1} × c_{2}) \end{matrix} (rep_{×})
{Γ ⊢ e : R(c) \atop Γ ⊢ R_{R}(e) : R(R(c))} (rep_{R})  {Γ ⊢ ∀α:κ.c : Type \atop Γ ⊢ R_{∀}(∀α:κ.c) : R(∀α:κ.c)} (rep_{∀})  {Γ ⊢ ∃α:κ.c : Type \atop Γ ⊢ R_{∃}(∃α:κ.c) : R(∃α:κ.c)} (rep_{∃})
\begin{matrix}Γ ⊢ e : c′ & Γ ⊢ c = c′ : κ \\ Γ ⊢ e : c \end{matrix} (equiv)

Figure 8: Term formation (except typecase)

Γ ⊢ e : c

Γ ⊢ e : R(int) Γ ⊢ e_{int} : c[int/β]

Γ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) : c[int/δ] (tcase_{int})

Γ ⊢ e : R(c_{1} → c_{2}) Γ, x:R(c_{1}), y:R(c_{2}) ⊢ e_{→}[c_{1}, c_{2}/β, γ] : c[c_{1} → c_{2}/δ]

Γ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) : c[c_{1} → c_{2}/δ] (tcase_{→})

Γ ⊢ e : R(c_{1} × c_{2}) Γ, x:R(c_{1}), y:R(c_{2}) ⊢ e_{×}[c_{1}, c_{2}/β, γ] : c[c_{1} × c_{2}/δ]

Γ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) : c[c_{1} × c_{2}/δ] (tcase_{×})

Γ ⊢ e : R(R(c′)) Γ, x:R(c′) ⊢ e_{R}[c′/β] : c[R(c′)/δ]

Γ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) : c[R(c′)/δ] (tcase_{R})

Γ ⊢ e : R(∀α:κ.c′) Γ ⊢ e_{∀} : c[∀α:κ.c′/δ]

Γ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) : c[∀α:κ.c′/δ] (tcase_{∀})

Γ ⊢ e : R(∃α:κ.c′) Γ ⊢ e_{∃} : c[∃α:κ.c′/δ]

Γ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) : c[∃α:κ.c′/δ] (tcase_{∃})

Γ, α:Type, Γ′ ⊢ e : R(α) Γ(Γ′[int/α]) ⊢ e_{int}[int/α] : c[int, int/α, δ] Γ, β:Type, γ:Type, (Γ′[β → γ/α]), x:R(β), y:R(γ) ⊢ e_{→}[β → γ/α] : c[β → γ, β → γ/α, δ] Γ, β:Type, γ:Type, (Γ′[β × γ/α]), x:R(β), y:R(γ) ⊢ e_{×}[β × γ/α] : c[β × γ, β × γ/α, δ]

Γ, β:Type, (Γ′[R(β)/α]), x:R(β) ⊢ e_{R}[R(β)/α] : c[R(β), R(β)/α, δ]

Γ, α:Type, Γ′ ⊢ e_{∀} : c[α/δ] Γ, α:Type, Γ′ ⊢ e_{∃} : c[α/δ]

Γ, α:Type, Γ′ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) : c[α/δ] (tcase_{α})

Γ ⊢ e : R(c′) Γ ⊢ e_{int} : c[int/δ] Γ, β:Type, γ:Type, x:R(β), y:R(γ) ⊢ e_{→} : c[β → γ/δ] Γ, β:Type, γ:Type, x:R(β), y:R(γ) ⊢ e_{×} : c[β × γ/δ]

Γ, β:Type, x:R(β) ⊢ e_{R} : c[R(β)/δ]

Γ ⊢ e_{∀} : c[c′/δ] Γ ⊢ e_{∃} : c[c′/δ]

Γ ⊢ typecase[δ.c] e (e_{int}, βγxy.e_{→}, βγxy.e_{×}, βx.e_{R}, e_{∀}, e_{∃}) : c[c′/δ] (tcase)

Figure 9: Term Formation (typecase)