Programming Language Semantics in Foundational Type Theory

Karl Crary^{∗}

Cornell University

February 28, 1998

Abstract

There are compelling benefits to using foundational type theory as a framework for programming language semantics. I give a semantics of an expressive programming calculus in the foundational type theory of Nuprl. Previous type-theoretic semantics have used less expressive type theories, or have sacrificed important programming constructs such as recursion and modules. The primary mechanisms of this semantics for the core calculus are partial types, for typing recursion, set types, for encoding power and singleton kinds, which are used for subtyping and module programming, and very dependent function types, for encoding signatures. I then extend the semantics to modules using phase-splitting.

1 Introduction

Type theory has become a popular framework for formal reasoning in computer science [7, 38, 21] and has formed the basis for a number of automated deduction systems, including Automath, Nuprl, HOL and Coq [18, 5, 22, 2], among others. In addition to formalizing mathematics, these systems are widely used for the analysis and verification of computer programs. To do this, one must draw a connection between the programming language used and the language of type theory; however, these connections have typically been informal translations, diminishing the significance of the formal verification results.

Formal connections have been drawn in the work of Reynolds [48] and Harper and Mitchell [26], each of whom sought to use type-theoretic analysis to explain an entire programming language. Reynolds gave a type-theoretic interpretation of Idealized Algol, and Harper and Mitchell did the same for a simplified fragment of Standard ML. Recently, Harper and Stone [29] have given such an interpretation of full Standard ML (Revised) [42]. However, in each of these cases, the type theories used were not sufficiently rich to form a foundation for mathematical reasoning; for example, they were unable to express equality or induction principles. On the other hand, Kreitz [34] gave an embedding of a fragment of Objective CAML [37] into the foundational type theory of Nuprl. However, this fragment omitted some important constructs, such as recursion and modules.

∗This material is based on work supported in part by ARPA/AF grant F30602-95-1-0047, NSF grant CCR-9244739, and AASERT grant N00014-95-1-0985. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not reflect the views of these agencies.

The difficulty has been that the same features of foundational type theories that make them so expressive also restrict the constructs that may be introduced into them. For example, as I will discuss below, the existence of induction principles precludes the typing of fix that is typical in programming languages. In this paper I show how to give a semantics to practical programming languages in foundational type theory. In particular, I give an embedding of a small but expressive programming language into a Martin-Löf-style type theory. This embedding is simple and syntaxdirected, which has been vital for its use in practical reasoning.

The applications of type-theoretic semantics are not limited to formal reasoning about programs. Using such a semantics it can be considerably easier to prove desirable properties about a programming language, such as type preservation, than with other means. We will see two such examples in Section 4.5. The usefulness of such semantics is also not limited to one particular programming language at a time. If two languages are given type-theoretic semantics, then one may use type theory to show relationships between the two, and when the semantics are simple, those relationships need be no more complicated than the inherent differences between the two. This is particularly useful in the area of type-directed compilation [52, 43, 36, 24, 44]. The process of type-directed compilation consists (in part) of translations between various typed intermediate languages. Embedding each into a common foundational type theory provides an ideal framework for showing the invariance of program meaning throughout the compilation process.

This semantics is also useful even if one ultimately desires a semantics in some framework other than type theory. Martin-Löf type theory is closely tied to a structured operational semantics and has denotational models in many frameworks including partial equivalence relations [1, 23], set theory [33] and domain theory [49, 46, 45]. Thus, foundational type theory may be used as a “semantic intermediate language.”

The paper is organized as follows: Section 2 presents the paper’s object language, λ^{K}. This object language is a small programming calculus, not a practical programming language, so a formal elaborator must be invoked to relate these results to a full programming language. I do not present such an elaborator in this paper, but see Harper and Stone [29, 28] for a presentation of such an elaborator. Section 3 contains an overview of Nuprl, the foundational type theory I use in this paper. Section 4 contains the embedding that is the central technical contribution of the paper. Section 5 discusses promising directions for future work. Finally, Section 6 contains brief concluding remarks.

2 The Lambda-K Programming Calculus

As a case study to illustrate my technique, I use a predicative variant of λ^{K}, the high-level typed intermediate language in the KML compiler [17]. In this section I discuss λ^{K}. In the interest of brevity, the discussion assumes knowledge of several well-known programming constructs. Further discussion of the design of λ^{K} appears in Crary [17].

The syntax rules of λ^{K} appear in Figure 1. The overall structure of the core calculus (that is, λ^{K} minus modules and signatures) is similar to the higher-order polymorphic lambda calculus [19, 20] augmented with records at the term and type constructor level (and their corresponding types and kinds), and a fixpoint operator at the term level. In addition to the kind Type, the kind level also includes, for any type τ, the power kind P(τ), which includes all subtypes of τ, and the singleton

kinds  κ ::= Type_{i} | Πα:κ_{1}.κ_{2} | P_{i}(c) | S_{i}(c) | {ℓ_{1} ▷ α_{1} : κ_{1}, …, ℓ_{n} ▷ α_{n} : κ_{n}}
constructors  c ::= α | λα:κ.c | c_{1}[c_{2}] | {ℓ_{1} = c_{1}, …, ℓ_{n} = c_{n}} | π_{ℓ}(c) | c_{1} → c_{2} | c_{1} ⇒ c_{2} |

∀α:κ.c | {ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}} | ext(m)

terms  e ::= x | λx:c.e | e_{1}e_{2} | Λα:κ.e | e[c] | {ℓ_{1} = e_{1}, …, ℓ_{n} = e_{n}} | π_{ℓ}(e) | fix_{c}(e) | ext(m)
signatures  σ ::= ⟨κ⟩ | ⟨⟨c⟩⟩ | Πs:σ_{1}.σ_{2} | {ℓ_{1} ▷ s_{1} : σ_{1}, …, ℓ_{n} ▷ s_{n} : σ_{n}}
modules  m ::= s | ⟨c⟩ | ⟨⟨e⟩⟩ | λs:σ.m | m_{1}m_{2} | {ℓ_{1} = m_{1}, …, ℓ_{n} = m_{n}} | π_{ℓ}(m) | m : σ
contexts  Γ ::= • | Γ[α : κ] | Γ[x : c] | Γ[s : σ]

Figure 1: λ^{K} Syntax

kind S(τ), which includes only τ. The kind level also contains the dependent function kind Πα:κ_{1}.κ_{2} and the dependent record kind {ℓ_{1} ▷ α_{1} : κ_{1}, …, ℓ_{n} ▷ α_{n} : κ_{n}} where each ℓ_{i} is an external name (or label) and each α_{i} is an internal name (or binding occurrence; see Harper and Lillibridge [25] for discussion of internal and external names). Evaluation is intended to be call-by-value. The type level includes a type constructor ⇒ for total functions and polymorphic functions are also required to be total.^{1} Expressions that differ only by alpha-variation are considered to be identical, as are expressions that differ only by permuting fields in a record (so long as no field of a dependent record kind is permuted to before a field on which it depends).

To make this calculus predicative, the type-oriented kinds have level annotations i (i.e., Type_{i}, P_{i}(τ) and S_{i}(τ)), which are integers ≥ 1. Each kind contains only types whose levels are strictly less than the given annotation, where the level of a type is the highest level annotation used within it. For P_{i}(τ) or S_{i}(τ) to be well-formed, the level of τ must be less than i. This mechanism is somewhat awkward, and is used to allow the calculus to be embedded in a predicative type theory. Section 5 contains some discussion of alternatives.

The static semantics of core λ^{K} is given by four judgements (inference rules appear in Appendix A). The subkinding judgement Γ ⊢_{K} κ_{1} ⊑ κ_{2} indicates that (in context Γ) every type constructor in κ_{1} is in κ_{2}. The constructor equality judgement Γ ⊢_{K} c_{1} = c_{2} : κ indicates that c_{1} and c_{2} are equal as members of kind κ. The typing judgement Γ ⊢_{K} e : c indicates that the term e has type c. Finally, the valuability judgement [29] Γ ⊢_{K} e ↓ c indicates that the term e has type c and evaluates without computational effects (in this setting this means just that it terminates).

The Module Calculus Lambda-K modules form their own syntactic class, and their types are called signatures, which also form their own syntactic class. A primitive module is either a single constructor ⟨c⟩ or a single term ⟨⟨e⟩⟩. If c has kind κ, then ⟨c⟩ has signature ⟨κ⟩. Likewise, if e has type τ, then ⟨⟨e⟩⟩ has signature ⟨⟨τ⟩⟩.

Modules are also formed using lambda-abstractions (for functors) and records (for structures). Such modules may be given dependent function signatures and dependent record signatures that are precisely analogous to the dependent function and dependent record kind mentioned above. A signature form for total functors (analogous to the total function type) would be straightforward to add, but is omitted for the sake of simplicity. Data abstraction is achieved by forgetting type information using the construct m : σ, which coerces the module m to have the signature σ (if that signature is valid for m); any type information about m not reflected in σ is forgotten. As with the

1Partial polymorphic functions could easily be added, but seem rarely to be useful in practice [53].

 sig
    tycon foo : type
    module S1 :
       sig
          tycon bar : type
          tycon baz = foo -> bar
          val gnurf : baz
       end
    val blap : S1.bar
 end

⟹

{ foo ▷ s_{foo} : ⟨Type⟩,
S1 ▷ s_{S1} :
{ bar ▷ s_{bar} : ⟨Type⟩,
baz ▷ s_{baz} : ⟨S(ext(s_{foo}) → ext(s_{bar}))⟩,
gnurf : ⟨⟨ext(s_{baz})⟩⟩ },
blap : ⟨⟨ext(πbar(s_{S1}))⟩⟩ }

 struct
    tycon foo = int -> int
    module S1 =
       struct
          tycon bar = int
          tycon baz =
             (int -> int) -> int
          val gnurf =
             fn f : int -> int => f 0
       end
    val blap = 12
 end

⟹ { foo = ⟨int → int⟩,

                                             S1 =

{ bar = ⟨int⟩, baz = ⟨(int → int) → int⟩, gnurf = ⟨⟨λf:(int → int). f 0⟩⟩ },

blap = ⟨⟨12⟩⟩ }

Figure 2: A Typical Module Encoding

subtyping and subkinding relations over the types and kinds, the signatures have a subsignature relation, which obeys rules similar to the rules governing subtyping and subkinding.

Modules are used within the core calculus by means of the extraction construct: ext(m) for module m. If m has signature ⟨κ⟩, then the constructor ext(m) has kind κ. Likewise, if m has signature ⟨⟨τ⟩⟩ then the term ext(m) has type τ.

With the above constructs, it is easy to encode source-level modules. A structure is constructed by building a record out of its contents with every constructor field encased in ⟨·⟩ and every term field encased in ⟨⟨·⟩⟩. Figure 2 shows the encoding of a typical module with a substructure into λ^{K}. Note the use of an internal and an external name in the encoding of the blap field of the signature. Functors and their signatures are encoded using λ and Π in the obvious manner.

The static semantics of the module calculus is given by three additional judgements (inference rules appear in Appendix A). The subsignature judgement Γ ⊢_{K} σ_{1} ⊑ σ_{2} indicates that (in context Γ) every module in σ_{1} is in σ_{2}. The module similarity judgement Γ ⊢_{K} m_{1} ≈ m_{2} : σ indicates that m_{1} and m_{2} are members of σ and the portions of m_{1} and m_{2} that relate to types are equal (as members of σ). When m_{1} and m_{2} are the same, this judgement serves as a signature assignment judgement. Finally, the module valuability judgement Γ ⊢_{K} m ↓ σ indicates that m has signature σ and evaluates without computational effects.

Type Formation Introduction  Elimination
universe i 𝕌_{i} type formation
(for i ≥ 1)  operators
disjoint union T_{1} + T_{2} inj_{1}(e) case(e, x_{1}.e_{1}, x_{2}.e_{2})
inj_{2}(e)
function space Πx:T_{1}.T_{2}  λx.e  e_{1}e_{2}
product space Σx:T_{1}.T_{2}  ⟨e_{1}, e_{2}⟩  π_{1}(e)

π_{2}(e)

integers  ℤ  …, −1, 0, 1, 2, … assorted operations
booleans  𝔹  true, false  if-then-else
atoms  Atom  string literals  equality test (=_{A})
top  Top

Figure 3: Type Theory Syntax

3 The Language of Type Theory

The type theory I use in this paper is the Martin-Löf-style type theory of Nuprl. A thorough discussion of Nuprl is beyond the scope of this paper, so the intent of this section is to give an overview of the programming features of type theory. It is primarily those programming features that I will use in the embedding. The logic of types is obtained through the propositions-as-types isomorphism [31], but this will not be critical to our purposes. Detailed discussions of type theory, including the logic of types, appear in Martin-Löf [38, 39] and Constable [7, 8], and Nuprl specifically is discussed in Constable et al. [5]. As in the previous section, the discussion here assumes knowledge of several well-known programming constructs.

As base types, the theory contains integers (denoted by ℤ), booleans (denoted by 𝔹), strings (denoted by Atom), and the trivial type Top (which contains every well-formed term, and in which all well-formed terms are equal). Complex types are built from the base types using various type constructors such as disjoint unions (denoted by T_{1}+T_{2}), dependent products (denoted by Σx:T_{1}.T_{2}) and dependent function spaces (denoted by Πx:T_{1}.T_{2}). When x does not appear free in T_{2}, we write T_{1} × T_{2} for Σx:T_{1}.T_{2} and T_{1} → T_{2} for Πx:T_{1}.T_{2}.

This gives an account of most of the familiar programming constructs other than polymorphism. To handle polymorphism we want to have functions that can take types as arguments. These can be typed with the dependent types discussed above if one adds a type of all types. Unfortunately, a single type of all types is known to make the theory inconsistent [20, 12, 41, 32], so instead the type theory includes a predicative hierarchy of universes, 𝕌_{1}, 𝕌_{2}, 𝕌_{3}, etc. The universe 𝕌_{1} contains all types built up from the base types only, and the universe 𝕌_{i+1} contains all types built up from the base types and the universes 𝕌_{1}, …, 𝕌_{i}. In particular, no universe is a member of itself.

Unlike λ^{K}, which has distinct syntactic classes for kinds, type constructors and terms, Nuprl has only one syntactic class for all expressions. As a result, types are first class citizens and may be computed just as any other term. For example, the expression if b then ℤ else Top (where b is a boolean expression) is a valid type. Evaluation is call-by-name, but the constructions in this paper may also be used in a call-by-value type theory with little modification.

To state the soundness of the embedding, we will require two assertions from the logic of types. These are equality, denoted by t_{1} = t_{2} in T, which states that the terms t_{1} and t_{2} are equal as members of type T, and subtyping, denoted by T_{1} ⊑ T_{2}, which states that every member of type T_{1} is in type T_{2} (and that terms equal in T_{1} are equal in T_{2}). A membership assertion, denoted by t ∈ T, is defined as t = t in T. The basic judgement in Nuprl is H ⊢_{ν} P, which states that in context H (which contains hypotheses and declarations of variables) the proposition P is true. Often the proposition P will be an assertion of equality or membership in a type.

The basic operators discussed above are summarized in Figure 3. The reader is referred to Crary [17] for the inference rules for the ⊢_{ν} judgement. Note that the lambda abstractions of Nuprl are untyped, unlike those of λ^{K}. In addition to the operators discussed here, the type theory contains some other less familiar type constructors: the partial type, set type and very dependent function type. In order to better motivate these type constructors, we defer discussion of them until their point of relevance. The dynamic semantics of all type theoretic operators appearing in this paper are given in Appendix B.

4 A Type-Theoretic Semantics

I present the embedding of λ^{K} into type theory in three parts. In the first part I begin by giving embeddings for most of the basic type and term operators. These embeddings are uniformly straightforward. Second, I examine what happens when the embedding is expanded to include fix. There we will find it necessary to modify some of the original embeddings of the basic operators. In the third part I complete the semantics by giving embeddings for the kind-level constructs of λ^{K}. The complete embedding is summarized in Figures 5 through 9.

The embedding itself could be formulated in type theory, leaving to metatheory only the trivial task of encoding the abstract syntax of the programming language. Were this done, the theorems of Section 4.5 could be proven within the framework of type theory. For simplicity, however, I will state the embedding and theorems in metatheory.

4.1 Basic Embedding

The embedding is defined as a syntax-directed mapping (denoted by [[ · ]]) of λ^{K} expressions to terms of type theory. Recall that in Nuprl all expressions are terms; in particular, types are terms and may be computed just as any other term. Many λ^{K} expressions are translated directly into type theory:

[[x]] =^{def} x
[[α]] =^{def} α
[[λx:c.e]] =^{def} λx.[[e]]
[[e_{1}e_{2}]] =^{def} [[e_{1}]][[e_{2}]]
[[c_{1} → c_{2}]] =^{def} [[c_{1}]] → [[c_{2}]]

Nothing happens here except that the types are stripped out of lambda abstractions to match the syntax of Nuprl. Functions at the type constructor level are equally easy to embed, but I defer discussion of them until Section 4.3.

Since the type theory does not distinguish between functions taking term arguments and functions taking type arguments, polymorphic functions may be embedded just as easily, although a dependent type is required to express the dependency of c on α in the polymorphic type ∀α:κ.c:

[[Λα:κ.e]] =^{def} λα.[[e]]
[[e[c]]] =^{def} [[e]][[c]]
[[∀α:κ.c]] =^{def} Πα:[[κ]].[[c]]

Just as the type was stripped out of the lambda abstraction above, the kind is stripped out of the polymorphic abstraction. The translation of the polymorphic function type above makes use of the embedding of kinds, but except for the elementary kind Type I defer discussion of the embedding of kinds until Section 4.3. The kind Type_{i}, which contains level-i types, is embedded as the universe containing level-i types:

[[Type_{i}]] =^{def} 𝕌_{i}

Records A bit more delicate than the above, but still fairly simple, is the embedding of records. Field labels are taken to be members of type Atom, and then records are viewed as functions that map field labels to the contents of the corresponding fields. For example, the record {x = 1, f = λx:int.x}, which has type {x : int, f : int → int}, is embedded as

λa. if a =_{A} x then 1 else if a =_{A} f then λx.x else ⋆

where a =_{A} a′ is the equality test on atoms, which returns a boolean when a and a′ are atoms, and ⋆ is an arbitrary member of Top.

Since the type of this function’s result depends upon its argument, this function must be typed using a dependent type:

Πa:Atom. if a =_{A} x then ℤ else if a =_{A} f then ℤ → ℤ else Top

In general, records and record types are embedded as follows:

[[{ℓ_{1} = e_{1}, …, ℓ_{n} = e_{n}}]] =^{def} λa. if a =_{A} ℓ_{1} then [[e_{1}]]
⋮
else if a =_{A} ℓ_{n} then [[e_{n}]]
else ⋆
[[π_{ℓ}(e)]] =^{def} [[e]] ℓ
[[{ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}}]] =^{def} Πa:Atom. if a =_{A} ℓ_{1} then [[c_{1}]]
⋮
else if a =_{A} ℓ_{n} then [[c_{n}]]
else Top

Note that this embedding validates the desired subtyping relationship on records. Since {x : int, f : int → int} ⊑ {x : int}, we would like the embedding to respect the subtyping relationship: [[{x : int, f : int → int}]] ⊑ [[{x : int}]]. Fortunately this is the case, since every type is a subtype of Top, and in particular the part of the type relating to the omitted field, if a = f then ℤ→ℤ else Top, is a subtype of Top.

4.2 Embedding Recursion

The usual approach to typing recursion, and the one used in λ^{K}, is to add a fix construct with the typing rule:

{H ⊢_{ν} e ∈ T → T \atop H ⊢_{ν} fix(e) ∈ T}  (wrong)

In effect, this adds recursively defined (and possibly divergent) terms to existing types. Unfortunately, such a broad fixpoint rule makes Martin-Löf type theories inconsistent because of the presence of induction principles. An induction principle on a type specifies the membership of that type; for example, the standard induction principle on the natural numbers specifies that every natural number is either zero or some finite iteration of successor on zero. The ability to add divergent elements to a type would violate the specification implied by that type’s induction rule.

One simple way to derive an inconsistency from the above typing rule uses the simplest induction principle, induction on the empty type Void. The induction principle for Void indirectly specifies that it has no members:

{H ⊢_{ν} e ∈ Void \atop H ⊢_{ν} e ∈ T}

However, it would be easy, using fix, to derive a member of Void: the identity function can be given type Void → Void, so fix(λx.x) would have type Void. Invoking the induction principle, fix(λx.x) would be a member of every type and, by the propositions-as-types isomorphism, would be a proof of every proposition. It is also worth noting that this inconsistency does not stem from the fact that Void is an empty type; similar inconsistencies may be derived (with a bit more work) for almost every type, including function types (to which the fix rule of λ^{K} is restricted).

It is clear, then, that fix cannot be used to define new members of the basic types. How then can recursive functions be typed? The solution is to add a new type constructor for partial types [10, 11, 51, 9, 17]. For any type T, the partial type \overline{T} is a supertype of T that contains all the elements of T and also all divergent terms. (A total type is one that contains only convergent terms.) The induction principles on \overline{T} [51, 9] are different than those on T, so we can safely type fix with the rule:^{2}

H ⊢_{ν} e ∈ \overline{T} → \overline{T} H ⊢_{ν} T admissible
H ⊢_{ν} fix(e) ∈ \overline{T}

We use partial types to interpret the possibly non-terminating computations of λ^{K}. When (in λ^{K}) a term e has type τ, the embedded term [[e]] will have type \overline{[[τ]]}. Moreover, if e is valuable, then [[e]] can still be given the stronger type [[τ]]. Before we can embed fix we must re-examine the embedding of function types. In Nuprl, partial functions are viewed as functions with partial result types:^{3}

[[c_{1} → c_{2}]] =^{def} [[c_{1}]] → \overline{[[c_{2}]]}
[[c_{1} ⇒ c_{2}]] =^{def} [[c_{1}]] → [[c_{2}]]
[[∀α:κ.c]] =^{def} (α:[[κ]]) → [[c]]

2The second subgoal, that the type T be admissible, is a technical condition related to the notion of admissibility in LCF. This condition is required because fixpoint induction can be derived from the recursive typing rule [51].

However, all the types used in the embedding in this paper are admissible, so I ignore the admissibility condition in this paper. Additional details appear in Smith [51] and Crary [16, 17].

3This terminology can be somewhat confusing. A total type is one that contains only convergent expressions.

The partial function type T_{1} → \overline{T}_{2} contains functions that return possibly divergent elements, but those functions themselves converge, so a partial function type is a total type.

Note that, as desired, [[τ_{1} ⇒ τ_{2}]] ⊑ [[τ_{1} → τ_{2}]], since [[τ_{2}]] ⊑ \overline{[[τ_{2}]]}. If partial polymorphic functions were included in λ^{K}, they would be embedded as Πα:[[κ]].\overline{[[c]]}.

Now suppose we wish to fix the function f which (in λ^{K}) has type (τ_{1} → τ_{2}) → (τ_{1} → τ_{2}), and suppose, for simplicity only, that f is valuable. Then [[f]] has type ([[τ_{1}]] → \overline{[[τ_{2}]]}) → \overline{[[τ_{1}]] → \overline{[[τ_{2}]]}}. This type does not quite fit the fix typing rule, which requires the domain type to be partial, so we must coerce [[f]] to a fixable type. We do this by eta-expanding [[f]] to gain access to its argument and then eta-expanding that argument:

λg.[[f]](λx.g x) ∈ \overline{[[τ_{1}]] → \overline{[[τ_{2}]]}} → \overline{[[τ_{1}]] → \overline{[[τ_{2}]]}}

Eta-expanding g ensures that it terminates, changing its type from \overline{[[τ_{1}]] → \overline{[[τ_{2}]]}} to [[τ_{1}]] → \overline{[[τ_{2}]]}. The former type is required by the fix rule, but the latter type is expected by [[f]]. Since the coerced [[f]] fits the fix typing rule, we get that fix(λg.[[f]](λx.g x)) has type \overline{[[τ_{1}]] → \overline{[[τ_{2}]]}}, as desired. Thus we may embed the fix construct as:

[[ fix_{c}(e)]] =^{def} fix(λg.[[e]](λx.g x))

Strictness In λ^{K}, a function may be applied to a possibly divergent argument, but in my semantics functions expect their arguments to be convergent. Therefore we must change the embedding of application to compute function arguments to canonical form before applying the function. (Polymorphic functions are unaffected because all type expressions converge (Corollary 4).) This is done using the sequencing construct let x = e_{1} in e_{2} which evaluates e_{1} to canonical form e′_{1} and then reduces to e_{2}[e′_{1}/x]. The sequence term diverges if e_{1} or e_{2} does and allows x be given a total type:

\begin{matrix}H ⊢_{ν} e_{1} ∈ \overline{T}_{2} & H[x : T_{2}] ⊢_{ν} e_{2} ∈ \overline{T_{1}} \\ H ⊢_{ν} let x = e_{1} in e_{2} ∈ \overline{T_{1}} \end{matrix}

Application is then embedded in the expected way:

[[e_{1}e_{2}]] =^{def} let x = [[e_{2}]] in [[e_{1}]] x

A final issue arises in regard to records. In the embedding of Section 4.1, the record {ℓ = e} would terminate even if e diverges. This would be unusual in a call-by-value programming language, so we need to ensure that each member of a record is evaluated:

[[{ℓ_{1} = e_{1}, …, ℓ_{n} = e_{n}}]] =^{def} let x_{1} = [[e_{1}]] in

⋮

let x_{n} = [[e_{n}]] in

λa. if a =_{A} ℓ_{1} then x_{1}

⋮
else if a =_{A} ℓ_{n} then x_{n}
else ⋆

4.3 Embedding Kinds

The kind structure of λ^{K} contains three first-order kind constructors. We have already seen the embedding of the kind Type; remaining are the power and singleton kinds. Each of these kinds represents a collection of types, so each will be embedded as something similar to a universe, but unlike the kind Type_{i}, which includes all types of the indicated level, the power and singleton kinds wish to exclude certain undesirable types. The power kind P_{i}(τ) contains only subtypes of τ and the singleton kind S_{i}(τ) contains only types that are equal to τ; other types must be left out.

The mechanism for achieving this exclusion is the set type [6]. If S is a type and P [·] is a predicate over S, then the set type {z : S | P [z]} contains all elements z of S such that P [z] is true. With this type, we can embed the power and singleton kinds as:^{4}

[[P_{i}(c)]] =^{def} {T : 𝕌_{i} | T ⊑ [[c]] ∧ [[c]] in 𝕌_{i}}
[[S_{i}(c)]] =^{def} {T : 𝕌_{i} | T = [[c]] in 𝕌_{i}}

Among the higher-order type constructors, functions at the type constructor level and their kinds are handled just as at the term level, except that function kinds are permitted to have dependencies but need not deal with partiality or strictness:

[[λα:κ.c]] =^{def} λα.[[c]]
[[c_{1}[c_{2}]]] =^{def} [[c_{1}]][[c_{2}]]
[[Πα:κ_{1}.κ_{2}]] =^{def} Πα:[[κ_{1}]].[[κ_{2}]]

Dependent Record Kinds For records at the type constructor level, the embedding of the records themselves is analogous to those at the term level (except that there is no issue of strictness):

[[{ℓ_{1} = c_{1}, …, ℓ_{n} = c_{n}}]] =^{def} λa. if a =_{A} ℓ_{1} then [[c_{1}]]
⋮
else if a =_{A} ℓ_{n} then [[c_{n}]]
else ⋆
[[π_{ℓ}(c)]] =^{def} [[c]] ℓ

However, the embedding of this expression’s kind is more complicated. This is because of the need to express dependencies among the fields of the dependent record kind. Recall that the embedding of a non-dependent record type already required a dependent type; to embed a dependent record type will require expressing even more dependency. Consider the dependent record kind {ℓ ▷ α : Type_{1}, ℓ′ ▷ α′ : P_{1}(α)}. We might naively attempt to encode this like the non-dependent record type as

Πa:Atom. if a =_{A} ℓ then 𝕌_{1} else
if a =_{A} ℓ′ then {T : 𝕌_{1} | T ⊑ α ∧ α in 𝕌_{1}} else Top

(wrong)

but this encoding is not correct; the variable α is now unbound. We want α to refer to the contents of field ℓ. In the encoding, this means we want α to refer to the value returned by the function

4The second clause in the embedding of the power kind ([[c]] in 𝕌_{i}) is used for technical reasons that require that well-formedness of P_{i}(τ) imply that τ : Type_{i}.

[figure: {f | x:T_{1} → T_{2}}; Πx:T_{1}.T_{2}; Σx:T_{1}.T_{2}; T_{1} → T_{2}; T_{1} × T_{2}; T_{1} + T_{2}]

Figure 4: The Type Triangle

when applied to label ℓ. So we want a type of functions whose return type can depend not only upon their arguments but upon their own return values!

The type I will use for this embedding is Hickey’s very dependent function type [30]. This type is a generalization of the dependent function type (itself a generalization of the ordinary function type) and like it, the very dependent function type’s members are just lambda abstractions. The difference is in the specification of a function’s return type. The type is denoted by {f | x:T_{1} → T_{2}} where f and x are binding occurrences that may appear free in T_{2} (but not in T_{1}).

As with the dependent function type, x stands for the function’s argument, but the additional variable f refers to the function itself. A function g belongs to the type {f | x:T_{1} → T_{2}} if g takes an argument from T_{1} (call it t) and returns a member of T_{2}[t, g/x, f].^{5}

For example, the kind {ℓ▷α : Type_{1}, ℓ′ ▷α′ : P_{1}(α)} discussed above is encoded as a very dependent function type as:

{f | a:Atom → if a =_{A} ℓ then 𝕌_{1} else
if a =_{A} ℓ′ then {T : 𝕌_{1} | T ⊑ f ℓ ∧ f ℓ in 𝕌_{1}} else Top}

To understand where this type constructor fits in with the more familiar type constructors, consider the “type triangle” shown in Figure 4. On the right are the non-dependent type constructors and in the middle are the dependent type constructors. Arrows are drawn from type constructors to weaker ones that may be implemented with them. Horizontal arrows indicate when a weaker constructor may be obtained by dropping a possible dependency from a stronger one; for example, the function type T_{1} → T_{2} is a degenerate form of the dependent function type Πx:T_{1}.T_{2} where the dependent variable x is not used in T_{2}. Diagonal arrows indicate when a weaker constructor may be implemented with a stronger one by performing case analysis on a boolean; for example, the disjoint union type T_{1} + T_{2} is equivalent to the type Σb:𝔹. if b then T_{1} else T_{2}.^{6} If we ignore the very dependent function type, the type triangle illustrates how the basic type constructors may be implemented by the dependent function and dependent product types. The very dependent function type completes this picture: the dependent function is a degenerate form where the f dependency is not used, and the dependent product may be implemented by switching on a boolean. Thus, the very dependent function type is a single unified type constructor from which all the basic type constructors may be constructed.

5To avoid the apparent circularity, in order for {f | x:T_{1} → T_{2}} to be well-formed we require that T_{2} may only use the result of f when applied to elements of T_{1} that are less than x with regard to some well-founded order. This restriction will not be a problem for this embedding because the order in which field labels appear in a dependent record kind is a perfectly good well-founded order.

6By switching on a label, instead of a boolean, record types and tagged variant types could be implemented and placed along the diagonals as well.

In general, dependent record kinds are encoded using a very dependent function type as follows:

[[{ℓ_{1} ▷ α_{1} : κ_{1}, …, ℓ_{n} ▷ α_{n} : κ_{n}}]]
=^{def}
{f | a:Atom → if a =_{A} ℓ_{1} then [[κ_{1}]]
else if a =_{A} ℓ_{2} then [[κ_{2}]][f ℓ_{1}/α_{1}]
⋮
else if a =_{A} ℓ_{n} then
[[κ_{n}]][f ℓ_{1} ⋯ f ℓ_{n−1}/α_{1} ⋯ α_{n−1}]
else Top}

4.4 Embedding Modules

The interpretation of modules in λ^{K} is by phase-splitting, where modules (including higher-order modules) are considered to consist of two components: a compile-time component and a run-time component. This is reflected in the type-theoretic semantics by an embedding that explicitly phasesplits modules into two parts. The technique used is derived from Harper, et al. [27].

The embeddings for modules and signatures are given by two syntax-directed mappings, [[ · ]]_{c} and [[ · ]]_{r}, one for the compile-time component of the given expression and one for the run time component. Given these, the embedding of a module is a pair of the compile-time and run-time components:

[[m]] =^{def} ⟨[[m]]_{c}, [[m]]_{r}⟩

In signatures, the types of run-time fields may depend upon a compile-time member, as in the signature {foo ▷ s_{foo} : ⟨Type⟩, bar : ⟨⟨ext(s_{foo})⟩⟩} (corresponding to the KML module sig tycon foo : type val bar : foo end). Consequently, the embedding of a signature is the dependent product of the compile-time component and the run-time component. The run-time component’s embedding is a function that takes as an argument the compile-time member on which it depends. In the embedding of the full signature, that function is applied to the variable standing for the compile-time member:

[[σ]] =^{def} Σv:[[σ]]_{c}.[[σ]]_{r}v

The embeddings of basic modules and signatures are simple. The run-time component is trivial for ⟨κ⟩ signatures and ⟨c⟩ modules, and the compile-time component is trivial for ⟨⟨c⟩⟩ signatures and ⟨⟨e⟩⟩. Module variables s are split into separate variables s_{c} and s_{r} for each component.

[[⟨c⟩]]_{c} =^{def} [[c]]  (module compile-time component)
[[⟨c⟩]]_{r} =^{def} ⋆  (module run-time component—trivial)
[[⟨κ⟩]]_{c} =^{def} [[κ]]  (signature compile-time component)
[[⟨κ⟩]]_{r} =^{def} λv.Top (signature run-time component—trivial)
[[⟨⟨e⟩⟩]]_{c} =^{def} ⋆  (module compile-time component—trivial)
[[⟨⟨e⟩⟩]]_{r} =^{def} [[e]]  (module run-time component)
[[⟨⟨c⟩⟩]]_{c} =^{def} Top  (signature compile-time component—trivial)
[[⟨⟨c⟩⟩]]_{r} =^{def} λv.[[c]] (signature run-time component)
[[s]]_{c} =^{def} s_{c}  (module compile-time component)
[[s]]_{r} =^{def} s_{r}  (module run-time component)

For each of the signatures above it is impossible for there to be any dependency of the run-time component on the compile-time component, since for ⟨κ⟩ there is no nontrivial run-time to depend on anything, and for ⟨⟨c⟩⟩ there is no nontrivial compile-time for anything to depend on. As a result, the variable v is ignored in each case.

Functors For function modules and signatures, everything looks familiar in the compile-time component, where the run-time material is ignored:

[[λs:σ.m]]_{c} =^{def} λs_{c}.[[m]]_{c}
[[m_{1}m_{2}]]_{c} =^{def} [[m_{1}]]_{c}[[m_{2}]]_{c}
[[Πs:σ_{1}.σ_{2}]]_{c} =^{def} Πs_{c}:[[σ_{1}]]_{c}.[[σ_{2}]]_{c}

However, the run-time component may not similarly ignore the compile-time component, because of possible dependencies. Therefore, the run-time component abstracts over both the compile-time and run-time components of its argument:

[[λs:σ.m]]_{r} =^{def} λs_{c}. λs_{r}. [[m]]_{r}
[[m_{1}m_{2}]]_{r} =^{def} [[m_{1}]]_{r}[[m_{2}]]_{c}[[m_{2}]]_{r}

The signature’s run-time component, then, takes an argument v representing the compile-time component and returns a curried function type. The result type is the run-time component of the result signature and that depends on the compile-time component. Fortunately, the result’s compile-time component is available (as v s_{c}), since v maps the compile-time component of the argument to the compile-time component of the result.

[[Πs:σ_{1}.σ_{2}]]_{r} =^{def} λv. Πs_{c}:[[σ_{1}]]_{c}. [[σ_{1}]]_{r}s_{c} → [[σ_{2}]]_{r}(v s_{c})

Structures For dependent record modules and signatures, the compile-time component looks like dependent record kinds and the type constructor records that belong to them:

[[{ℓ_{1} = m_{1}, …, ℓ_{n} = m_{n}}]]_{c} =^{def} λa. if a =_{A} ℓ_{1} then [[m_{1}]]_{c} ⋮ else if a =_{A} ℓ_{n} then [[m_{n}]]_{c} else ⋆

[[π_{ℓ}(m)]]_{c} =^{def} [[m]]_{c}ℓ
[[{ℓ_{1} ▷ s_{1} : σ_{1}, …, ℓ_{n} ▷ s_{n} : σ_{n}}]]_{c} =^{def} {f | a:Atom → if a =_{A} ℓ_{1} then [[σ_{1}]]_{c} else if a =_{A} ℓ_{2} then [[σ_{2}]]_{c}[f ℓ_{1}/s_{1c}] ⋮ else if a =_{A} ℓ_{n} then [[σ_{n}]]_{c}[f ℓ_{1} ⋯ f ℓ_{n−1}/s_{1c} ⋯ s_{(n−1)c}] else Top}

The run-time component of modules looks much like the embedding of record terms (as with those, a series of opening lets is necessary to ensure strictness):

[[{ℓ_{1} = m_{1}, …, ℓ_{n} = m_{n}}]]_{r} =^{def} let x_{1} = [[m_{1}]]_{r} in

⋮

let x_{n} = [[m_{n}]]_{r} in

λa. if a =_{A} ℓ_{1} then x_{1} ⋮ else if a =_{A} ℓ_{n} then x_{n} else ⋆

(where x_{i} does not appear free in m_{i})

[[π_{ℓ}(m)]]_{r} =^{def} [[m]]_{r}ℓ

The run-time component of signatures is also familiar, except that it must deal with dependencies on the compile-time component. Again, the run-time component takes an argument v representing the compile-time component. The run-time component [[σ_{i}]]_{r} of each field is applied to the compile-time component of that field, which is v ℓ_{i}. Also, each field may have dependencies on the compile-time components of earlier fields. These dependencies will have been expressed by free occurrences of the variables s_{ic}, into which we substitute the corresponding compile-time components v ℓ_{i}. It is worthwhile to note that these substitutions for s_{ic} are the only places where dependencies on the argument v are introduced.

[[{ℓ_{1} ▷ s_{1} : σ_{1}, …, ℓ_{n} ▷ s_{n} : σ_{n}}]]_{r}
=^{def} λv. Πa:Atom. if a =_{A} ℓ_{1} then [[σ_{1}]]_{r}(v ℓ_{1}) if a =_{A} ℓ_{2} then [[σ_{2}]]_{r}(v ℓ_{2})[v ℓ_{1}/s_{1c}] ⋮ else if a =_{A} ℓ_{n} then [[σ_{n}]]_{r}(v ℓ_{n})[v ℓ_{1} ⋯ v ℓ_{n−1}/s_{1c} ⋯ s_{(n−1)c}] else Top

[[α]] =^{def} α
[[λα:κ.c]] =^{def} λα.[[c]]
[[c_{1}[c_{2}]]] =^{def} [[c_{1}]][[c_{2}]]
[[{ℓ_{1} = c_{1}, …, ℓ_{n} = c_{n}}]] =^{def} λa. if a =_{A} ℓ_{1} then [[c_{1}]]

⋮

else if a =_{A} ℓ_{n} then [[c_{n}]] else ⋆

(where a does not appear free in c_{i})

[[π_{ℓ}(c)]] =^{def} [[c]] ℓ
[[c_{1} → c_{2}]] =^{def} [[c_{1}]] → \overline{[[c_{2}]]}
[[c_{1} ⇒ c_{2}]] =^{def} [[c_{1}]] → [[c_{2}]]
[[∀α:κ.c]] =^{def} Πα:[[κ]].[[c]]
[[{ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}}]] =^{def} Πa:Atom. if a =_{A} ℓ_{1} then [[c_{1}]]
⋮

else if a =_{A} ℓ_{n} then [[c_{n}]]

else Top

(where a does not appear free in c_{i})

Figure 5: Embedding Types

[[x]] =^{def} x
[[λx:c.e]] =^{def} λx.[[e]]
[[e_{1}e_{2}]] =^{def} let x = [[e_{2}]] in [[e_{1}]] x

(where x does not appear free in e_{1})

[[Λα:κ.e]] =^{def} λα.[[e]]
[[e[c]]] =^{def} [[e]][[c]]
[[{ℓ_{1} = e_{1}, …, ℓ_{n} = e_{n}}]] =^{def} let x_{1} = [[e_{1}]] in

⋮ let x_{n} = [[e_{n}]] in λa. if a =_{A} ℓ_{1} then x_{1}

⋮

else if a =_{A} ℓ_{n} then x_{n} else ⋆

(where x_{i} does not appear free in e_{j})

[[π_{ℓ}(e)]] =^{def} [[e]] ℓ
[[ fix_{c}(e)]] =^{def} fix(λg.[[e]](λx.g x))

(where g does not appear free in e)

Figure 6: Embedding Terms

[[Type_{i}]] =^{def} {T : 𝕌_{i} | T admissible}
[[P_{i}(c)]] =^{def} {T : 𝕌_{i} | T ⊑ [[c]] ∧ [[c]] in 𝕌_{i} ∧ T admissible}

(where T does not appear free in c)

[[S_{i}(c)]] =^{def} {T : 𝕌_{i} | T = [[c]] in 𝕌_{i} ∧ T admissible}

(where T does not appear free in c)

[[Πα:κ_{1}.κ_{2}]] =^{def} Πα:[[κ_{1}]].[[κ_{2}]]

[[{ℓ_{1} ▷ α_{1} : κ_{1}, …, ℓ_{n} ▷ α_{n} : κ_{n}}]] =^{def} {f | a:Atom → if a =_{A} ℓ_{1} then [[κ_{1}]]

else if a =_{A} ℓ_{2} then [[κ_{2}]][f ℓ_{1}/α_{1}]
⋮
else if a =_{A} ℓ_{n} then
[[κ_{n}]][f ℓ_{1} ⋯ f ℓ_{n−1}/α_{1} ⋯ α_{n−1}]
else Top}

(where f, a do not appear free in κ_{i})

Figure 7: Embedding Kinds

4.5 Properties of the Embedding

I conclude my presentation of the type-theoretic semantics of λ^{K} by examining some of the important properties of the semantics. We want the embedding to validate the intuitive meaning of the judgements of λ^{K}’s static semantics. If κ_{1} is a subkind of κ_{2} then we want the embedded kind [[κ_{1}]] to be a subtype of [[κ_{2}]]; if c_{1} and c_{2} are equal in kind κ, we want the embedded constructors [[c_{1}]] and [[c_{2}]] to be equal (in [[κ]]); and if e has type τ we want [[e]] to have type \overline{[[τ]]} (and [[τ]] if e is valuable). Similar properties are desired for the module judgements. This is stated in Theorem 1:

Theorem 1 (Semantic Soundness) For every λ^{K} context Γ, let [[Γ]] be defined as follows:

[[ •]] =^{def} ϵ
[[Γ[α : κ]]] =^{def} [[Γ]], α:[[κ]]
[[Γ[x : c]]] =^{def} [[Γ]], x:[[c]]
[[Γ[s : σ]]] =^{def} [[Γ]], s_{c}:[[σ]]_{c}, s_{r}:[[σ]]_{r}s_{c}

Suppose [[Γ]] = v_{1}:T_{1}, …, v_{n}:T_{n}; then the following implications hold:

1. If Γ ⊢_{K} κ ⊑ κ′ then v_{1}:T_{1}, …, v_{n}:T_{n} ⊢_{ν} ([[κ]] in 𝕌_{level(κ)+1} ∧ [[κ′]] in 𝕌_{level(κ′)+1} ∧ [[κ]] ⊑ [[κ′]]).

2. If Γ ⊢_{K} c = c′ : κ then v_{1}:T_{1}, …, v_{n}:T_{n} ⊢_{ν} [[c]] = [[c′]] in [[κ]].

3. If Γ ⊢_{K} e : c then v_{1}:T_{1}, …, v_{n}:T_{n} ⊢_{ν} [[e]] in \overline{[[c]]}.

4. If Γ ⊢_{K} e ↓ c then v_{1}:T_{1}, …, v_{n}:T_{n} ⊢_{ν} [[e]] in [[c]].

5. If Γ ⊢_{K} σ ⊑ σ′ then v_{1}:T_{1}, …, v_{n}:T_{n} ⊢_{ν} ([[σ]] in 𝕌_{level(σ)+1} ∧ [[σ′]] in 𝕌_{level(σ′)+1} ∧ [[σ]] ⊑ [[σ′]]).

6. If Γ ⊢_{K} m ≈ m′ : σ then v_{1}:T_{1}, …, v_{n}:T_{n} ⊢_{ν} ([[m]] in \overline{[[σ]]}∧[[m′]] in \overline{[[σ]]}∧[[m]]_{c} = [[m′]]_{c} in [[σ]]_{c}).

7. If Γ ⊢_{K} m ↓ σ then v_{1}:T_{1}, …, v_{n}:T_{n} ⊢_{ν} [[m]] in [[σ]].

[[σ]] =^{def} Σv:[[σ]]_{c}.[[σ]]_{r}v

(where v does not appear free in σ)

[[⟨κ⟩]]_{c} =^{def} [[κ]]
[[⟨κ⟩]]_{r} =^{def} λv.Top
[[⟨⟨c⟩⟩]]_{c} =^{def} Top
[[⟨⟨c⟩⟩]]_{r} =^{def} λv.[[c]]

(where v does not appear free in c)

[[Πs:σ_{1}.σ_{2}]]_{c} =^{def} Πs_{c}:[[σ_{1}]]_{c}.[[σ_{2}]]_{c}
[[Πs:σ_{1}.σ_{2}]]_{r} =^{def} λv. Πs_{c}:[[σ_{1}]]_{c}. [[σ_{1}]]_{r}s_{c} → [[σ_{2}]]_{r}(v s_{c})

(where v, s do not appear free in σ_{i})

[[{ℓ_{1} ▷ s_{1} : σ_{1}, …, ℓ_{n} ▷ s_{n} : σ_{n}}]]_{c} =^{def} {f | a:Atom → if a =_{A} ℓ_{1} then [[σ_{1}]]_{c} else if a =_{A} ℓ_{2} then [[σ_{2}]]_{c}[f ℓ_{1}/s_{1c}] ⋮ else if a =_{A} ℓ_{n} then [[σ_{n}]]_{c}[f ℓ_{1} ⋯ f ℓ_{n−1}/s_{1c} ⋯ s_{n−1c}] else Top}

(where f, a do not appear free in σ_{i})

[[{ℓ_{1} ▷ s_{1} : σ_{1}, …, ℓ_{n} ▷ s_{n} : σ_{n}}]]_{r} =^{def} λv. Πa:Atom. if a =_{A} ℓ_{1} then [[σ_{1}]]_{r}(v ℓ_{1}) if a =_{A} ℓ_{2} then [[σ_{2}]]_{r}(v ℓ_{2})[v ℓ_{1}/s_{1c}] ⋮ else if a =_{A} ℓ_{n} then [[σ_{n}]]_{r}(v ℓ_{n}) [v ℓ_{1} ⋯ v ℓ_{n−1}/s_{1c} ⋯ s_{n−1c}] else Top}

(where v, a do not appear free in σ_{i})

Figure 8: Embedding Signatures

[[m]] =^{def} ⟨[[m]]_{c}, [[m]]_{r}⟩
[[s]]_{c} =^{def} s_{c}
[[s]]_{r} =^{def} s_{r}
[[⟨c⟩]]_{c} =^{def} [[c]]
[[⟨c⟩]]_{r} =^{def} ⋆
[[⟨⟨e⟩⟩]]_{c} =^{def} ⋆
[[⟨⟨e⟩⟩]]_{r} =^{def} [[e]]
[[λs:σ.m]]_{c} =^{def} λs_{c}.[[m]]_{c}
[[λs:σ.m]]_{r} =^{def} λs_{c}. λs_{r}. [[m]]_{r}
[[m_{1}m_{2}]]_{c} =^{def} [[m_{1}]]_{c}[[m_{2}]]_{c}
[[m_{1}m_{2}]]_{r} =^{def} [[m_{1}]]_{r}[[m_{2}]]_{c}[[m_{2}]]_{r}
[[{ℓ_{1} = m_{1}, …, ℓ_{n} = m_{n}}]]_{c} =^{def} λa. if a =_{A} ℓ_{1} then [[m_{1}]]_{c} ⋮ else if a =_{A} ℓ_{n} then [[m_{n}]]_{c} else ⋆

(where a does not appear free in m_{i})

[[{ℓ_{1} = m_{1}, …, ℓ_{n} = m_{n}}]]_{r} =^{def} let x_{1} = [[m_{1}]]_{r} in

⋮ let x_{n} = [[m_{n}]]_{r} in λa. if a =_{A} ℓ_{1} then x_{1} ⋮ else if a =_{A} ℓ_{n} then x_{n} else ⋆

(where x_{i} does not appear free in m_{i})

[[π_{ℓ}(m)]]_{c} =^{def} [[m]]_{c}ℓ
[[π_{ℓ}(m)]]_{r} =^{def} [[m]]_{r}ℓ
[[m : σ]]_{c} =^{def} [[m]]_{c}
[[m : σ]]_{r} =^{def} [[m]]_{r}

Figure 9: Embedding Modules Proof

By induction on the derivations of the λ^{K} judgements.

We may observe two immediate consequences of the soundness theorem. One is the desirable property of type preservation: evaluation does not change the type of a program. Appendix B gives a small-step evaluation relation for the Nuprl type theory (denoted by t ↦ t′ when t evaluates in one step to t′). Type preservation of λ^{K} (Corollary 3) follows directly from soundness and type preservation of Nuprl (Proposition 2).

Proposition 2 If ⊢_{ν} t ∈ T and t ↦^{∗} t′ then t′ ∈ T.

Proof

Not difficult, but outside the scope of this paper (see Crary [17]).

Corollary 3 (Type Preservation) If ⊢_{K} e : τ and [[e]] ↦^{∗} t then t ∈ [[τ]].

Another consequence of the soundness theorem is that the phase distinction [4, 27] is respected in λ^{K}: all type expressions converge and therefore types may be computed in a compile-time phase. This is expressed by Corollary 4:

Corollary 4 (Phase Distinction) If ⊢_{K} c : κ then there exists canonical t such that [[c]] ↦^{∗} t.

Proof

For any well-formed λ^{K} kind κ, the embedded kind [[κ]] can easily be shown to be a total type. (Intuitively, every type is total unless it is constructed using the partial type constructor, which is not used in the embedding of kinds.) The conclusion follows directly.

5 Directions for Future Investigation

One important avenue for future work is to extend the semantics in this paper to explain stateful computation. One promising device for doing this is to encode stateful computations as monads [47, 35], but this raises two difficulties. In order to encode references in monads, all expressions that may side-effect the store must take the store as an argument. The problem is how to assign a type to the store. Since side-effecting functions may be in the store themselves, the store must be typed using a recursive type, and since side-effecting expressions take the store as an argument, that recursive type will include negative occurrences of the variable of recursion. Type theory may express recursive types with only positive occurrences, but to allow negative occurrences is an open problem.^{7} The other main problem arising with a monadic interpretation of state has to do with predicativity. If polymorphic functions may be placed into the store, every function type, when monadized to take the store as an argument, will have a level as high as the highest level appearing in the store. Consequently, those monadized function types will not be valid arguments to some type abstractions when they should be. The obvious solution to this problem is to restrict references to be built with level-1 (non-polymorphic) types only. A more general solution would be to use a type theory with impredicative features. In addition to solving this problem, this would also eliminate the need for level annotations in the source calculus. The type theory of Mendler [40] provides such impredicative features and is quite similar to Nuprl; I have not used that framework in this paper out of desire to use a simpler and more standard theory. The Calculus of Constructions [14, 13] also supplies impredicative features and could likely also support the semantics in this paper.

7See Birkedal and Harper [3] for a promising approach that may lead to a solution of this problem.

6 Conclusion

I have shown how to give a type-theoretic semantics to an expressive programming calculus. This semantics makes it possible to use formal type-theoretic reasoning about programs and programming languages without informal embeddings and without sacrificing core expressiveness of the programming language.

Formal reasoning aside, embedding programming languages into type theory allows a researcher to bring the full power of type theory to bear on a programming problem. For example, Crary [15] used a type-theoretic interpretation to expose the relation of power kinds to a nonconstructive set type. Adjusting this interpretation to make the power kind constructive resulted in a proof-passing technique used to implement higher-order coercive subtyping in KML.

Furthermore, the simplicity of the semantics makes it attractive to use as a mathematical model similar in spirit, if not in detail, to the Scott-Strachey program [50]. This semantics works out so neatly because type theory provides built-in structure well-suited for analysis of programming. Most importantly, type theory provides structured data and an intrinsic notion of computation. Non-type-theoretic models of type theory can expose the “scaffolding” when one desires the details of how that structure may be implemented [1, 23, 17].

As a theory of structured data and computation, type theory is itself a very expressive programming language. Practical programming languages are less expressive, but offer properties that foundational type theory does not, such as decidable type checking. I suggest that it is profitable to take type theory as a foundation for programming, and to view practical programming languages as tractable approximations of type theory. This paper illustrates how to formalize these approximations. This view not only helps to explain programming languages and their features, as I have done in this paper, but also provides a greater insight into how we can bring more of the expressiveness of type theory into programming languages.

Acknowledgements

I am grateful to Robert Harper and Robert Constable for their many substantially helpful comments and suggestions.

References

[1] Stuart Allen. A non-type-theoretic definition of Martin-Löf’s types. In Second IEEE Symposium on Logic in Computer Science, pages 215–221, Ithaca, New York, June 1987.

[2] Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, César Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saïbi, and Benjamin Werner. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, CNRS and ENS Lyon, 1996.

[3] Lars Birkedal and Robert Harper. Relational interpretations of recursive types in an operational setting. In Theoretical Aspects of Computer Software, 1997.

[4] Luca Cardelli. Phase distinctions in type theory. Manuscript, January 1988.

[5] R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki, and S.F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.

[6] Robert L. Constable. Constructive mathematics as a programming logic I: Some principles of theory. In Topics in the Theory of Computation, volume 24 of Annals of Discrete Mathematics, pages 21–37. Elsevier, 1985. Selected papers of the International Conference on Foundations of Computation Theory 1983.

[7] Robert L. Constable. Type theory as a foundation for computer science. In Theoretical Aspects of Computer Software 1991, volume 526 of Lecture Notes in Computer Science, pages 226–243, Sendai, Japan, 1991. Springer-Verlag.

[8] Robert L. Constable. Types in logic, mathematics and programming. In Sam Buss, editor, Handbook of Proof Theory, chapter 10. Elsevier Science, 1998.

[9] Robert L. Constable and Karl Crary. Computational complexity and induction for partial computable functions in type theory. Technical report, Department of Computer Science, Cornell University, 1997.

[10] Robert L. Constable and Scott Fraser Smith. Partial objects in constructive type theory. In Second IEEE Symposium on Logic in Computer Science, pages 183–193, Ithaca, New York, June 1987.

[11] Robert L. Constable and Scott Fraser Smith. Computational foundations of basic recursive function theory. In Third IEEE Symposium on Logic in Computer Science, pages 360–371, Edinburgh, Scotland, July 1988.

[12] Thierry Coquand. An analysis of Girard’s paradox. In First IEEE Symposium on Logic in Computer Science, pages 227–236, Cambridge, Massachusetts, June 1986.

[13] Thierry Coquand. Metamathematical investigations of a calculus of constructions. In P. Odifreddi, editor, Logic and Computer Science, volume 31 of The APIC Series, pages 91–122. Academic Press, 1990.

[14] Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.

[15] Karl Crary. Foundations for the implementation of higher-order subtyping. In 1997 ACM SIGPLAN International Conference on Functional Programming, pages 125–135, Amsterdam, June 1997.

[16] Karl Crary. Admissibility of fixpoint induction over partial types. Technical report, Department of Computer Science, Cornell University, 1998.

[17] Karl Crary. Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1998. Forthcoming.

[18] N. G. de Bruijn. A survey of the project Automath. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 579–606. Academic Press, 1980.

[19] Jean-Yves 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.

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

[21] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1988.

[22] Michael J. C. Gordon and Tom F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.

[23] Robert Harper. Constructing type systems over an operational semantics. Journal of Symbolic Computation, 14:71–84, 1992.

[24] Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Twentieth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 206–219, January 1993.

[25] Robert Harper and Mark 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, January 1994.

[26] Robert Harper and John C. Mitchell. On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15(2):211–252, April 1993.

[27] Robert Harper, John C. Mitchell, and Eugenio Moggi. Higher-order modules and the phase distinction. In Seventeenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 341–354, San Francisco, January 1990.

[28] Robert Harper and Chris Stone. An interpretation of Standard ML in type theory. Technical Report CMU-CS-97-147, Carnegie Mellon University, School of Computer Science, June 1997.

[29] Robert Harper and Chris Stone. A type-theoretic interpretation of Standard ML. In Proof, Language and Interaction: Essays in Honour of Robin Milner. The MIT Press, 1998. To appear.

[30] Jason J. Hickey. Formal objects in type theory using very dependent types. In Foundations of Object Oriented Languages 3, 1996.

[31] W. Howard. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 479–490. Academic Press, 1980.

[32] Douglas J. Howe. The computational behaviour of Girard’s paradox. In Second IEEE Symposium on Logic in Computer Science, pages 205–214, Ithaca, New York, June 1987.

[33] Douglas J. Howe. Semantic foundations for embedding HOL in Nuprl. Technical report, Bell Labs, 1996.

[34] Christoph Kreitz. Formal reasoning about communications systems I. Technical report, Department of Computer Science, Cornell University, 1997.

[35] John Launchbury and Simon L. Peyton Jones. State in Haskell. Lisp and Symbolic Computation, 8(4):293–341, December 1995.

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

[37] Xavier Leroy. The Objective Caml System, Release 1.00. Institut National de Recherche en Informatique et Automatique (INRIA), 1996. Available at http://pauillac.inria.fr/ocaml.

[38] Per Martin-Löf. An intuitionistic theory of types: Predicative part. In Proceedings of the Logic Colloquium, 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73–118. North-Holland, 1975.

[39] Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress of Logic, Methodology and Philosophy of Science, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153–175. North-Holland, 1982.

[40] Paul Francis Mendler. Inductive Definition in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, September 1987.

[41] Albert R. Meyer and Mark B. Reinhold. ‘Type’ is not a type. In Thirteenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 287–295, St. Petersburg Beach, Florida, January 1986.

[42] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). The MIT Press, Cambridge, Massachusetts, 1997.

[43] Greg Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania, December 1995.

[44] Greg Morrisett, David Walker, Karl Crary, and Neal 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, January 1998. Extended version published as Cornell University technical report TR97-1651.

[45] Erik Palmgren. An information system interpretation of Martin-Löf’s partial type theory with universes. Information and Computation, 106:26–60, 1993.

[46] Erik Palmgren and Viggo Stoltenberg-Hansen. Domain interpretations of intuitionistic type theory. U.U.D.M. Report 1989:1, Uppsala University, Department of Mathematics, January 1989.

[47] Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Twentieth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993.

[48] John C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Proceedings of the International Symposium on Algorithmic Languages, pages 345–372, Amsterdam, October 1981. North-Holland.

[49] Adrian Rezus. Semantics of constructive type theory. Technical Report 70, Informatics Department, Faculty of Science, Nijmegen, University, The Netherlands, September 1985.

[50] Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages. In Proceedings of the Symposium on Computers and Automata, volume 21 of Microwave Research Institute Symposia Series. Polytechnic Institute of Brooklyn, 1971.

[51] Scott Fraser Smith. Partial Objects in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, January 1989.

[52] 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.

[53] Andrew K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343–356, December 1995.

A Static Semantics of Lambda-K

Γ ⊢ κ_{1} ⊑ κ_{2}  κ_{1}, κ_{2} are valid kinds and κ_{1} is a

subkind of κ_{2}

Γ ⊢_{K} c_{1} = c_{2} : κ  c_{1} and c_{2} are equal in kind κ
Γ ⊢_{K} e : c  e has type c
Γ ⊢_{K} e ↓ c  e is valuable and has type c
Γ ⊢_{K} σ_{1} ⊑ σ_{2}  σ_{1}, σ_{2} are valid signatures and σ_{1}

is a subsignature of σ_{2}

Γ ⊢_{K} m_{1} ≈ m_{2} : σ  m_{1} and m_{2} are similar in

signature σ

Γ ⊢_{K} m ↓ σ  m is valuable and has signature σ
Γ ⊢_{K} κ kind  =^{def} Δ ⊢_{K} κ ⊑ κ
Γ ⊢_{K} c : κ  =^{def} Δ ⊢_{K} c = c : κ
Γ ⊢_{K} c_{1} ⊑_{i} c_{2}  =^{def} Δ ⊢_{K} c_{1} : P_{i}(c_{2})
Γ ⊢_{K} σ sig  =^{def} Γ ⊢_{K} σ ⊑ σ
Γ ⊢_{K} m : σ  =^{def} Γ ⊢_{K} m ≈ m : σ
level(Type_{i}) =^{def} i
level(Πα:κ_{1}.κ_{2}) =^{def} max(level(κ_{1}), level(κ_{2}))
level({ℓ_{i} ▷ α_{i} : κ_{i}^{[i=1...n]}}) =^{def} max_{i=1}^{n} level(κ_{i})
level(P_{i}(c)) =^{def} i
level(S_{i}(c)) =^{def} i

A.1 Kind Formation and Subkinding

\begin{matrix}Γ ⊢_{K} κ_{1} ⊑ κ_{2} & Γ ⊢_{K} κ_{2} ⊑ κ_{3} \\ Γ ⊢_{K} κ_{1} ⊑ κ_{3} \end{matrix}  (SubkindTrans)
Γ ⊢_{K} Type_{i} ⊑ Type_{j} i ≤ j  (Type)

\begin{matrix}Γ ⊢_{K} κ′_{1} ⊑ κ_{1} \\ Γ[α : κ′_{1}] ⊢_{K} κ_{2} ⊑ κ′_{2} Γ[α : κ_{1}] ⊢_{K} κ_{2} kind \end{matrix}

Γ ⊢_{K} Πα:κ_{1}.κ_{2} ⊑ Πα:κ′_{1}.κ′_{2} α ∉ Γ

(Pi)

Γ[α_{j} : κ_{j}]^{[j=1...i−1]} ⊢_{K} κ_{i} ⊑ κ′_{i} for 1 ≤ i ≤ m Γ[α_{j} : κ_{j}]^{[j=1...i−1]} ⊢_{K} κ_{i} kind for m < i ≤ n Γ[α_{j} : κ′_{j}]^{[j=1...i−1]} ⊢_{K} κ′_{i} kind for 1 ≤ i ≤ m

\begin{matrix}Γ ⊢_{K} \{ℓ_{i} ▷ α_{i} : κ_{i}^{[i=1...n]}\} ⊑ \{ℓ_{i} ▷ α_{i} : κ′_{i}^{[i=1...m]}\} \\ α_{i}^{[i=1...m−1]} ∉ Γ, n ≥ m \end{matrix}

(DepRecord)

{Γ ⊢_{K} c_{1} ⊑_{i} c_{2} \atop Γ ⊢_{K} P_{i}(c_{1}) ⊑ P_{j}(c_{2})} i ≤ j  (Pow)
Γ ⊢_{K} c : Type_{i}
Γ ⊢_{K} P_{i}(c) ⊑ Type_{i}

(PowType)

{Γ ⊢_{K} c_{1} = c_{2} : Type_{i} \atop Γ ⊢_{K} S_{i}(c_{1}) ⊑ S_{j}(c_{2})} i ≤ j  (Sing)
{Γ ⊢_{K} c : Type_{i} \atop Γ ⊢_{K} S_{i}(c) ⊑ P_{i}(c)}  (SingPow)

A.2 Kinding and Constructor Equality

{Γ ⊢_{K} c_{2} = c_{1} : κ \atop Γ ⊢_{K} c_{1} = c_{2} : κ}  (Symm)
\begin{matrix}Γ ⊢_{K} c_{1} = c_{2} : κ & Γ ⊢_{K} c_{2} = c_{3} : κ \\ Γ ⊢_{K} c_{1} = c_{3} : κ \end{matrix}  (Trans)
Γ ⊢_{K} α = α : κ α : κ ∈ Γ  (TypeVar)

Γ ⊢_{K} κ_{1} kind Γ[α : κ_{1}] ⊢_{K} c = c′ : κ_{2} Γ ⊢_{K} λα:κ_{1}.c = λα:κ_{1}.c′ : Πα:κ_{1}.κ_{2} α ∉ Γ (PiIntro)

\begin{matrix}Γ ⊢_{K} c_{1} = c′_{1} : Πα:κ_{1}.κ_{2} & Γ ⊢_{K} c_{2} = c′_{2} : κ_{1} \\ Γ ⊢_{K} c_{1}[c_{2}] = c′_{1}[c′_{2}] : κ_{2}[c_{2}/α] \end{matrix}  (PiElim)

Γ ⊢_{K} c_{i} = c′_{i} : κ_{i}[c_{j}^{[j=1...i−1]}/α_{j}^{[j=1...i−1]}] for 1 ≤ i ≤ n

Γ ⊢_{K} {ℓ_{i} ▷ α_{i} : κ_{i}^{[i=1...n]}} kind

\begin{matrix}Γ ⊢_{K} \{ℓ_{i} = c_{i}^{[i=1...n]}\} = \{ℓ_{i} = c′_{i}^{[i=1...n]}\} : \\ \{ℓ_{i} ▷ α_{i} : κ_{i}^{[i=1...n]}\} \end{matrix}

(DepRecordIntro)

Γ ⊢_{K} c = c′ : \{ℓ_{j} ▷ α_{j} : κ_{j}^{[i=1...n]}\} ; \begin{matrix}Γ ⊢_{K} π_{ℓ_{i}}(c) = π_{ℓ_{i}}(c′) : κ_{i}[π_{ℓ_{j}} (c)^{[j=1...i−1]}/α_{j}^{[j=1...i−1]}] \\ 1 ≤ i ≤ n \end{matrix}

(DepRecordElim)

Γ ⊢_{K} c_{1} = c′_{1} : Type_{i} Γ ⊢_{K} c_{2} = c′_{2} : Type_{i}

Γ ⊢_{K} c_{1} → c_{2} = c′_{1} → c′_{2} : Type_{i} (Arrow)

Γ ⊢_{K} c_{1} = c′_{1} : Type_{i} Γ ⊢_{K} c_{2} = c′_{2} : Type_{i}

Γ ⊢_{K} c_{1} ⇒ c_{2} = c′_{1} ⇒ c′_{2} : Type_{i} (TArrow)

\begin{matrix}Γ ⊢_{K} κ_{1} ⊑ κ_{2} \\ Γ ⊢_{K} κ_{2} ⊑ κ_{1} Γ[α : κ_{1}] ⊢_{K} c = c′ : Type_{i} \end{matrix}

Γ ⊢_{K} ∀α:κ_{1}.c_{1} = ∀α:κ_{2}.c_{2} : Type_{i} α ∉ Γ, level(κ_{1}) < i, level(κ_{2}) < i

(Quant)

Γ ⊢_{K} c_{i} = c′_{i} : Type_{j} for 1 ≤ i ≤ n

Γ ⊢_{K} {ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}} = {ℓ_{1} : c′_{1}, …, ℓ_{n} : c′_{n}} : Type_{j}

(Record)

\begin{matrix}Γ ⊢_{K} c = c′ : κ_{1} & Γ ⊢_{K} κ_{1} ⊑ κ_{2} \\ Γ ⊢_{K} c = c′ : κ_{2} \end{matrix}  (Subkind)
{Γ ⊢_{K} (λα:κ′.c_{1})[c_{2}] : κ \atop Γ ⊢_{K} (λα:κ′.c_{1})[c_{2}] = c_{1}[c_{2}/α] : κ}  (PiBeta)
{Γ ⊢_{K} λα:κ′_{1}.c[α] : Πα:κ_{1}.κ_{2} \atop Γ ⊢_{K} λα:κ′_{1}.c[α] = c : Πα:κ_{1}.κ_{2}} α ∉ c  (PiEta)
{Γ ⊢_{K} π_{ℓ_{j}} (\{ℓ_{i} = c_{i}^{[i=1...n]}\}) : κ \atop Γ ⊢_{K} π_{ℓ_{j}} (\{ℓ_{i} = c_{i}^{[i=1...n]}\}) = c_{j} : κ} 1 ≤ j ≤ n

(DepRecordBeta)

{Γ ⊢_{K} \{ℓ_{i} = π_{ℓ_{i}}(c)^{[i=1...n]}\} : \{ℓ_{i} ▷ α_{i} : κ_{i}^{[i=1...n]}\} \atop Γ ⊢_{K} \{ℓ_{i} = π_{ℓ_{i}}(c)^{[i=1...n]}\} = c : \{ℓ_{i} ▷ α_{i} : κ_{i}^{[i=1...n]}\}}

(DepRecordEta)

{Γ ⊢_{K} c_{1} = c_{2} : Type_{i} \atop Γ ⊢_{K} c_{1} : S_{i}(c_{2})}  (SingIntro)
{Γ ⊢_{K} c_{1} : S_{i}(c_{2}) \atop Γ ⊢_{K} c_{1} = c_{2} : Type_{i}}  (SingElim)
\begin{matrix}Γ ⊢_{K} c_{1} = c_{2} : Type_{i} & Γ ⊢_{K} c_{1} : P_{i}(c_{3}) \\ Γ ⊢_{K} c_{1} = c_{2} : P_{i}(c_{3}) \end{matrix}  (PowFun)
\begin{matrix}Γ ⊢_{K} c_{1} = c_{2} : Type_{i} & Γ ⊢_{K} c_{1} : S_{i}(c_{3}) \\ Γ ⊢_{K} c_{1} = c_{2} : S_{i}(c_{3}) \end{matrix}  (SingFun)

Γ ⊢_{K} m_{1} ≈ m_{2} : ⟨κ⟩ Γ ⊢_{K} ext(m_{1}) = ext(m_{2}) : κ (TypeModElim)

A.3 Subtyping

\begin{matrix}Γ ⊢_{K} c_{1} ⊑_{i} c_{2} & Γ ⊢_{K} c_{2} ⊑_{i} c_{3} \\ Γ ⊢_{K} c_{1} ⊑_{i} c_{3} \end{matrix}  (SubtypeTrans)
\begin{matrix}Γ ⊢_{K} c′_{1} ⊑_{i} c_{1} & Γ ⊢_{K} c_{2} ⊑_{i} c′_{2} \\ Γ ⊢_{K} c_{1} → c_{2} ⊑_{i} c′_{1} → c′_{2} \end{matrix}  (ArrowSub)
\begin{matrix}Γ ⊢_{K} c′_{1} ⊑_{i} c_{1} & Γ ⊢_{K} c_{2} ⊑_{i} c′_{2} \\ Γ ⊢_{K} c_{1} ⇒ c_{2} ⊑_{i} c′_{1} ⇒ c′_{2} \end{matrix}  (TArrowSub)
Γ ⊢_{K} c_{1} : Type_{i} Γ ⊢_{K} c_{2} : Type_{i}

Γ ⊢_{K} c_{1} ⇒ c_{2} ⊑_{i} c_{1} → c_{2} (TotalSub)

\begin{matrix}Γ ⊢_{K} κ_{1} ⊑ κ_{2} & Γ ⊢_{K} κ_{2} ⊑ κ_{1} & Γ[α : κ_{1}] ⊢_{K} c_{1} ⊑_{i} c_{2} \\ Γ ⊢_{K} ∀α:κ_{1}.c_{1} ⊑_{i} ∀α:κ_{2}.c_{2} \end{matrix}

α ∉ Γ, level(κ_{1}) < i, level(κ_{2}) < i

(QuantSub)

{Γ ⊢_{K} c_{i} ⊑_{j} c′_{i} for 1 ≤ i ≤ n \atop Γ ⊢_{K} \{ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}\} ⊑_{j} \{ℓ_{1} : c′_{1}, …, ℓ_{n} : c′_{n}\}}

(RecordSub)

Γ ⊢_{K} {ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}} : Type_{i} Γ ⊢_{K} c : Type_{i}
Γ ⊢_{K} {ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}, ℓ : c} ⊑_{i} {ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}}

(RecordFieldSub)

A.4 Typing

Γ ⊢_{K} x : c x : c ∈ Γ  (Var)
\begin{matrix}Γ ⊢_{K} c_{1} : Type_{i} & Γ[x : c_{1}] ⊢_{K} e : c_{2} \\ Γ ⊢_{K} λx:c_{1}.e : c_{1} → c_{2} \end{matrix} x ∉ Γ (ArrowIntro)
\begin{matrix}Γ ⊢_{K} e_{1} : c_{1} → c_{2} & Γ ⊢_{K} e_{2} : c_{1} \\ Γ ⊢_{K} e_{1}e_{2} : c_{2} \end{matrix}  (ArrowElim)
\begin{matrix}Γ ⊢_{K} c_{1} : Type_{i} & Γ[x : c_{1}] ⊢_{K} e ↓ c_{2} \\ Γ ⊢_{K} λx:c_{1}.e : c_{1} ⇒ c_{2} \end{matrix} x ∉ Γ (TArrowIntro)
\begin{matrix}Γ ⊢_{K} e_{1} : c_{1} ⇒ c_{2} & Γ ⊢_{K} e_{2} : c_{1} \\ Γ ⊢_{K} e_{1}e_{2} : c_{2} \end{matrix}  (TArrowElim)

Γ ⊢_{K} κ kind Γ[α : κ] ⊢_{K} e ↓ c Γ ⊢_{K} Λα:κ.e : ∀α:κ.c α ∉ Γ  (QuantIntro)

\begin{matrix}Γ ⊢_{K} e : ∀α:κ.c_{2} & Γ ⊢_{K} c_{1} : κ \\ Γ ⊢_{K} e[c_{1}] : c_{2}[c_{1}/α] \end{matrix}  (QuantElim)

{Γ ⊢_{K} e_{i} : c_{i} for 1 ≤ i ≤ n \atop Γ ⊢_{K} \{ℓ_{1} = e_{1}, …, ℓ_{n} = e_{n}\} : \{ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}\}}

(RecordIntro)

{Γ ⊢_{K} e : \{ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}\} \atop Γ ⊢_{K} π_{ℓ_{i}}(e) : c_{i}}  (RecordElim)

{Γ ⊢_{K} e : (c_{1} → c_{2}) → (c_{1} → c_{2}) \atop Γ ⊢_{K} fix(e) : c_{1} → c_{2}}  (Fix)

{Γ ⊢_{K} m : ⟨⟨c⟩⟩ \atop Γ ⊢_{K} ext(m) : c}  (TermModElim)

\begin{matrix}Γ ⊢_{K} e : c_{1} & Γ ⊢_{K} c_{1} ⊑_{i} c_{2} \\ Γ ⊢_{K} e : c_{2} \end{matrix}  (Subtype)

A.5 Valuability

Γ ⊢_{K} x ↓ c x : c ∈ Γ  (VarHalt)

\begin{matrix}Γ ⊢_{K} c_{1} : Type_{i} & Γ[x : c_{1}] ⊢_{K} e : c_{2} \\ Γ ⊢_{K} λx:c_{1}.e ↓ c_{1} → c_{2} \end{matrix} x ∉ Γ

(ArrowIntroHalt)

\begin{matrix}Γ ⊢_{K} c_{1} : Type_{i} & Γ[x : c_{1}] ⊢_{K} e ↓ c_{2} \\ Γ ⊢_{K} λx:c_{1}.e ↓ c_{1} ⇒ c_{2} \end{matrix} x ∉ Γ

(TArrowIntroHalt)

\begin{matrix}Γ ⊢_{K} e_{1} ↓ c_{1} ⇒ c_{2} & Γ ⊢_{K} e_{2} ↓ c_{1} \\ Γ ⊢_{K} e_{1}e_{2} ↓ c_{2} \end{matrix}  (TArrowElimHalt)

Γ ⊢_{K} κ kind Γ[α : κ] ⊢_{K} e ↓ c Γ ⊢_{K} Λα:κ.e ↓ ∀α:κ.c α ∉ Γ (QuantIntroHalt)

\begin{matrix}Γ ⊢_{K} e ↓ ∀α:κ.c_{2} & Γ ⊢_{K} c_{1} : κ \\ Γ ⊢_{K} e[c_{1}] ↓ c_{2}[c_{1}/α] \end{matrix}  (QuantElimHalt)

{Γ ⊢_{K} e_{i} ↓ c_{i} for 1 ≤ i ≤ n \atop Γ ⊢_{K} \{ℓ_{1} = e_{1}, …, ℓ_{n} = e_{n}\} ↓ \{ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}\}}

(RecordIntroHalt)

{Γ ⊢_{K} e ↓ \{ℓ_{1} : c_{1}, …, ℓ_{n} : c_{n}\} \atop Γ ⊢_{K} π_{ℓ_{i}}(e) ↓ c_{i}}  (RecordElimHalt)

{Γ ⊢_{K} e ↓ (c_{1} → c_{2}) ⇒ (c_{1} → c_{2}) \atop Γ ⊢_{K} fix(e) ↓ c_{1} → c_{2}}  (FixHalt)

{Γ ⊢_{K} m ↓ ⟨⟨c⟩⟩ \atop Γ ⊢_{K} ext(m) ↓ c}  (TermModElimHalt)

\begin{matrix}Γ ⊢_{K} e ↓ c_{1} & Γ ⊢_{K} c_{1} ⊑_{i} c_{2} \\ Γ ⊢_{K} e ↓ c_{2} \end{matrix}  (SubtypeHalt)

A.6 Signature Formation and Subsignatures

\begin{matrix}Γ ⊢_{K} σ_{1} ⊑ σ_{2} & Γ ⊢_{K} σ_{2} ⊑ σ_{3} \\ Γ ⊢_{K} σ_{1} ⊑ σ_{3} \end{matrix}  (SubsigTrans)

{Γ ⊢_{K} κ_{1} ⊑ κ_{2} \atop Γ ⊢_{K} ⟨κ_{1}⟩ ⊑ ⟨κ_{2}⟩}  (KindSig)

{Γ ⊢_{K} c_{1} ⊑_{i} c_{2} \atop Γ ⊢_{K} ⟨⟨c_{1}⟩⟩ ⊑ ⟨⟨c_{2}⟩⟩}  (TypeSig)

\begin{matrix}Γ ⊢_{K} σ′_{1} ⊑ σ_{1} & Γ[s : σ′_{1}] ⊢_{K} σ_{2} ⊑ σ′_{2} \\ Γ ⊢_{K} Πs:σ_{1}.σ_{2} ⊑ Πs:σ′_{1}.σ′_{2} \end{matrix}  (PiSig)

Γ[s_{j} : σ_{j}]^{[j=1...i−1]} ⊢_{K} σ_{i} ⊑ σ′_{i} for 1 ≤ i ≤ m Γ[s_{j} : σ_{j}]^{[j=1...i−1]} ⊢_{K} σ_{i} sig for m < i ≤ n Γ[s_{j} : σ′_{j}]^{[j=1...i−1]} ⊢_{K} σ′_{i} sig for 1 ≤ i ≤ m

\begin{matrix}Γ ⊢_{K} \{ℓ_{i} ▷ s_{i} : σ_{i}^{[i=1...n]}\} ⊑ \{ℓ_{i} ▷ s_{i} : σ′_{i}^{[i=1...m]}\} \\ s_{i}^{[i=1...m−1]} ∉ Γ, n ≥ m \end{matrix}

(RecordSig)

A.7 Signature Assignment and Module Similarity

{Γ ⊢_{K} m_{2} ≈ m_{1} : σ \atop Γ ⊢_{K} m_{1} ≈ m_{2} : σ}  (SymmMod)

\begin{matrix}Γ ⊢_{K} m_{1} ≈ m_{2} : σ & Γ ⊢_{K} m_{2} ≈ m_{3} : σ \\ Γ ⊢_{K} m_{1} ≈ m_{3} : σ \end{matrix}  (TransMod)

Γ ⊢_{K} s : σ s : σ ∈ Γ  (ModVar)

{Γ ⊢_{K} c_{1} = c_{2} : κ \atop Γ ⊢_{K} ⟨c_{1}⟩ ≈ ⟨c_{2}⟩ : ⟨κ⟩}  (TypeModIntro)
\begin{matrix}Γ ⊢_{K} e_{1} : c & Γ ⊢_{K} e_{2} : c \\ Γ ⊢_{K} ⟨⟨e_{1}⟩⟩ ≈ ⟨⟨e_{2}⟩⟩ : ⟨⟨c⟩⟩ \end{matrix}  (TermModIntro)
\begin{matrix}Γ ⊢_{K} σ_{1} sig & Γ[s : σ_{1}] ⊢_{K} m ≈ m′ : σ_{2} \\ Γ ⊢_{K} λs:σ_{1}.m ≈ λs:σ_{1}.m′ : Πs:σ_{1}.σ_{2} \end{matrix}  (PiModIntro)

\begin{matrix}Γ ⊢_{K} m_{1} ≈ m′_{1} : Πs:σ_{1}.σ_{2} & Γ ⊢_{K} m_{2} ≈ m′_{2} : σ_{1} \\ Γ ⊢_{K} m_{1}m_{2} ≈ m′_{1}m′_{2} : σ_{2}[m_{2}/s] \end{matrix}

(PiModElim)

Γ ⊢_{K} m_{i} ≈ m′_{i} : σ_{i}[m_{j}^{[j=1...i−1]}/s_{j}^{[j=1...i−1]}] for 1 ≤ i ≤ n

Γ ⊢_{K} {ℓ_{i} ▷ s_{i} : σ_{i}^{[i=1...n]}} sig

\begin{matrix}Γ ⊢_{K} \{ℓ_{i} = m_{i}^{[i=1...n]}\} ≈ \{ℓ_{i} = m′_{i}^{[i=1...n]}\} : \\ \{ℓ_{i} ▷ s_{i} : σ_{i}^{[i=1...n]}\} \end{matrix}

(RecordModIntro)

Γ ⊢_{K} m = m′ : \{ℓ_{j} ▷ s_{j} : σ_{j}^{[i=1...n]}\} ; \begin{matrix}Γ ⊢_{K} π_{ℓ_{i}}(m) = π_{ℓ_{i}}(m′) : σ_{i}[π_{ℓ_{j}} (m)^{[j=1...i−1]}/s_{j}^{[j=1...i−1]}] \\ 1 ≤ i ≤ n \end{matrix}

(RecordModElim)

{Γ ⊢_{K} m : σ \atop Γ ⊢_{K} (m : σ) : σ}  (CoerceMod)

A.8 Module Valuability

Γ ⊢_{K} s ↓ σ s : σ ∈ Γ  (ModVarHalt)
{Γ ⊢_{K} c : κ \atop Γ ⊢_{K} ⟨c⟩ ↓ ⟨κ⟩}  (TypeModIntroHalt)
{Γ ⊢_{K} e ↓ c \atop Γ ⊢_{K} ⟨⟨e⟩⟩ ↓ ⟨⟨c⟩⟩}  (TermModIntroHalt)
\begin{matrix}Γ ⊢_{K} σ_{1} sig & Γ[s : σ_{1}] ⊢_{K} m : σ_{2} \\ Γ ⊢_{K} λs:σ_{1}.m ↓ Πs:σ_{1}.σ_{2} \end{matrix}  (PiModIntro)

Γ ⊢_{K} m_{i} ↓ σ_{i}[m_{j}^{[j=1...i−1]}/s_{j}^{[j=1...i−1]}] for 1 ≤ i ≤ n

Γ ⊢_{K} {ℓ_{i} ▷ s_{i} : σ_{i}^{[i=1...n]}} sig Γ ⊢_{K} {ℓ_{i} = m_{i}^{[i=1...n]}} ↓ {ℓ_{i} ▷ s_{i} : σ_{i}^{[i=1...n]}}

(RecordModIntro)

Γ ⊢_{K} m ↓ \{ℓ_{j} ▷ s_{j} : σ_{j}^{[i=1...n]}\} ; \begin{matrix}Γ ⊢_{K} π_{ℓ_{i}}(m) ↓ σ_{i}[π_{ℓ_{j}} (m)^{[j=1...i−1]}/s_{j}^{[j=1...i−1]}] \\ 1 ≤ i ≤ n \end{matrix}

(RecordModElim)

{Γ ⊢_{K} m ↓ σ \atop Γ ⊢_{K} (m : σ) ↓ σ}  (CoerceMod)

B Dynamic Semantics of Nuprl

A term is canonical if its top level form is any of the type constructors or introduction forms from Figure 3.

e ↦ e′

case(e, x_{1}.e_{1}, x_{2}.e_{2}) ↦ case(e′, x_{1}.e_{1}, x_{2}.e_{2})
case(inj_{1}(e), x_{1}.e_{1}, x_{2}.e_{2}) ↦ e_{1}[e/x_{1}]
case(inj_{2}(e), x_{1}.e_{1}, x_{2}.e_{2}) ↦ e_{2}[e/x_{2}]

{e_{1} ↦ e′_{1} \atop e_{1}e_{2} ↦ e′_{1}e_{2}}

(λx.e_{1})e_{2} ↦ e_{1}[e_{2}/x]

{e ↦ e′ \atop π_{1}(e) ↦ π_{1}(e′)}

π_{1}(⟨e_{1}, e_{2}⟩) ↦ e_{1}

{e ↦ e′ \atop π_{2}(e) ↦ π_{2}(e′)}

π_{2}(⟨e_{1}, e_{2}⟩) ↦ e_{2}

e ↦ e′
if e then e_{1} else e_{2} ↦ if e′ then e_{1} else e_{2}
if true then e_{1} else e_{2} ↦ e_{1}
if false then e_{1} else e_{2} ↦ e_{2}

{e_{1} ↦ e′_{1} \atop e_{1} =_{A} e_{2} ↦ e′_{1} =_{A} e_{2}}

e1 is a string literal e_{2} ↦ e′_{2}

e_{1} =_{A} e_{2} ↦ e_{1} =_{A} e′_{2}

e1 and e2 are identical string literals e_{1} =_{A} e_{2} ↦ true

e1 and e2 are different string literals e_{1} =_{A} e_{2} ↦ false

e_{1} ↦ e′_{1}

let x = e_{1} in e_{2} ↦let x = e′_{1} in e_{2}

e_{1} is canonical let x = e_{1} in e_{2} ↦ e_{2}[e_{1}/x]

fix(e) ↦ e fix(e)