Julien Cretin

Didier Rémy

System F with Coercion Constraints

Keywords: Type, System F, F-eta, Polymorphism, Coercion, Conversion, Retyping functions, Type containment, Subtyping, Bounded Polymorphism. Type-indexed Recursive types Types, Système F, Polymorphisme, Coercion, Conversion, Fonction de retypage, Type containment, Sous-typage, Bounded Polymorphism

] by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions and equi-recursive types. This allows to present in a uniform way several type system features that had previously been studied separately: type containment, bounded and instance-bounded polymorphism, which are already encodable with parametric coercion abstraction, and ML-style subtyping constraints. Our framework allows for a clear separation of language constructs with and without computational content. We also distinguish coherent coercions that are fully erasable from potentially incoherent coercions that suspend the evaluation-and enable the encoding of GADTs. Technically, type coercions that witness subtyping relations between types are replaced by a more expressive notion of typing coercions that witness subsumption relations between typings, e.g. pairs composed of a typing environment and a type. Our calculus is equipped with a strong notion of reduction that allows reduction under abstractions-but we also introduce a form of weak reduction as reduction cannot proceed under incoherent type abstractions. Type soundness is proved by adapting the step-indexed semantics technique to strong reduction strategies, moving indices inside terms so as to control the reduction steps internally.

Introduction

Type systems are syntactical languages to express properties and invariants of programs. Their objects are usually types, typing contexts, and typing derivations. These can be interpreted as mathematical objects or proofs. Typically, a typing judgment Γ ⊢ a : τ can be interpreted as a proof that the term a is well-behaved and that its computational behavior is approximated by the type τ when the approximations of the behaviors of its free variables are given by the typing context Γ. The simply-typed λ-calculus extended with constants such as pairs or integers to model the core of a real programming language is the simplest of all type systems. It is also somewhat canonical: it just contains one type construct for each related construct of the language: arrow types τ → σ to classify functions, τ × σ to classify pairs, etc. and nothing else. Each type construct has a counter-part in terms and we may call them computational types.

Simply-typed λ-calculus is however too restrictive and type systems are usually extended with some form of polymorphism that allows an expression to have several types, or rather a type that stands for a whole collection of other types. Parametric polymorphism, whose System F is the reference introduces polymorphic types ∀α τ . A typing judgment Γ ⊢ a : ∀α τ means that the program a has also type τ [α ← σ] (i.e. τ where α has been replaced by σ) for all types σ.

This operation, called type instantiation is in fact independent of the program a and can be captured as an auxiliary instantiation judgment ∀α τ ≤ τ [α ← σ]. This means that any term that has type ∀α τ also has type τ [α ← σ]. Type instantiation is only a very specific form of some more general concept called type containment introduced by Mitchell [Mitchell(1988)]. Mitchell showed that adding type containment to System F is equivalent to closing System F by η-expansion (hence the name F η for the resulting system). Type containment allows instantiation to be performed deeper inside terms (by contrast with System F where it remains superficial), following the structure of types covariantly, or contravariantly on the left of arrow types. Type containment contains the germs of subtyping, which usually refers to a restriction of type containment that does not include type instantiation as part of the subtyping relation, but instead injects primitive subtyping relations between constants such as int ≤ float or a primitive bottom and top types. F <: [START_REF] Cardelli | An extension of system f with subtyping[END_REF] Cardelli, Martini, Mitchell, and Scedrov] is the system of reference for combining subtyping with polymorphism. Surprisingly, the languages F η and F <: share the same underlying concepts but have in fact quite different flavors and are incomparable (no one is strictly more general then the other). For example, F <: has bounded quantification ∀(α ≤ τ ) σ that allows to abstract over all type α that are a subtype of τ , a concept not present in F η . Although quite powerful, bounded quantification seems bridled and somewhat ad hoc as it allows for a unique and upper bound.

The language ML F [Le Botlan and Rémy(2009)] is another variant of System F that has been introduced for performing partial type inference while retaining principal types. It has similarities with both F <: and F η , but introduces yet another notion, instance bounded quantification-or unique lower bounds.

In [START_REF] Cretin | [END_REF]], we introduced F p ι , a language of type coercions with the ability to abstract over coercions, that can express F η type containment, F <: upper bounded polymorphism, and ML F instance-bounded polymorphism, uniformly. Following a general and systematic approach to coercions lead to an expressive and modular design. However, F p ι still comes with a severe restriction: abstract coercions must be parametric in either their domain or their codomain, so that abstract coercions are coherent, i.e. their types are always inhabited by concrete coercions. This limitation is disappointing from both theoretical and practical view points. In practice, F p ι fails to give an account of subtyping constraints that are used for type inference with subtyping in ML. While in theory, subtyping constraints and second-order polymorphism

RR n°8456

are orthogonal concepts that should be easy to combine.

Summary of our contributions

In this work, we solve this problem and present a language F cc that generalizes F p ι (and thus subsumes F η , F <: , and ML F ) to also model subtyping constraints. Besides, F cc includes a general form of recursive coercions, from which we can recover powerful subtyping rules between equi-recursive types. As in our previous work, the language is equipped with a strong reduction strategy, which also models reduction on open terms and provides stronger properties. We still permit a form of weak reduction on demand to model incoherent abstractions when needed, e.g. to encode GADTs.

We also generalize type coercions to typing coercions which enables a much clearer separation between computational types and erasable types that are all treated as coercions. In particular, type abstraction becomes a coercion and distributivity rules become derivable. Another side contribution of our work is an adaption of step-indexed semantics to strong reduction strategies, moving indices inside terms.

Plan The rest of the paper is organized as follows. We discuss a few important issues underlying the design of F cc in §2. We present F cc formally in §3. We introduce our variant of step-indexed denotational semantics in §4 and apply it to prove the soundness of our calculus in Section §5. We discuss the expressivity of F cc in §6 and differences with our previous work and other related works as well as future works in §7.

The language F cc and its soundness and normalization proofs have been formalized and mechanically verified in Coq.1

The design of F cc

The language F cc is designed around the notion of erasable coercions. Strictly speaking erasable coercions should leave no trace in terms and not change the semantics of the underlying untyped λ-term. When coercions are explicit and kept during reduction, as in F p ι , one should show a bisimulation property between the calculus with explicit coercions and terms of λ-calculus after erasure of all coercions. However, since coercions do not have computational content, they may also be left implicit, as is the case in F cc .

Some languages also use coercions with computational content. These are necessarily explicit and cannot be erased at runtime. They are of quite a different nature, so we restrict our study to erasable coercions.

Still, erasability is subtle in the presence of coercion abstraction, because one could easily abstract over nonsensical coercions, e.g. that could coerce any type into any other type. By default, these situations should be detected and rejected of course. We say that coercion abstraction is coherent when the coercion type is inhabited and incoherent when it may be uninhabited. Notice that type abstraction in System F, bounded polymorphism in F <: , and instance bounded polymorphism in ML F are all coherent.

Coherent abstraction ensures that the body of the abstraction is meaningful-whenever welltyped. Hence, it makes sense to reduce the body of the abstraction before having a concrete value for the coercion-or equivalently to reduce open terms that contain coherent abstract coercions.

Conversely, incoherent abstraction must freeze the evaluation of the body until it is specialized with a concrete coercion that provides inhabitation evidence. Therefore, abstraction over incoherent coercions cannot be erased, even though coercions themselves carry no information and can be represented as the unit type value, as in FC-the internal language of Haskell whose coercion abstractions are (potentially) incoherent.

Choosing a weak evaluation strategy as is eventually done in all programming languages does not solve the problem, but just sweeps it under the carpet: while type-soundness will hold, static type errors will be delayed until applications and library functions that will never be applicable may still be written.

Conversely, a strong reduction strategy better exercises the typing rules: that is, type soundness for a strong reduction strategy provides stronger guarantees. In our view, type systems should be designed to be sound for strong reduction strategies even if their reduction is eventually restricted to weak strategies for efficiency reasons. This is how programming languages based on System F or F <: have been conceived, indeed.

Therefore, F cc is equipped with strong reduction as the default and this is a key aspect of our design which could otherwise have been much simpler but also less useful.

However, we also permit abstraction over (potentially) incoherent coercions on demand, as this is needed to encode some form of dynamic typing, as can be found in programming languages with GADTs, for example. Indeed, GADTs allow to define parametric functions that are partial and whose body may only make sense for some but not all type instances. When accepting a value of a GADT as argument, the function may gain evidence that some type equality holds and that the value is indeed in the domain of the function. We claim that incoherent abstraction should be used exactly when needed and no more. In particular, one should not make all abstractions incoherent just because some of them must be.

From explicit to implicit coercions Coherence is ensured in F p ι by the parametricity restriction that limits abstraction to have a unique upper or lower bound. This also prevents abstract coercions from appearing in between the destructor and the constructor of a redex, a pattern of the form (c λ(x : τ ′ ) M N ) (where c • is the application of a coercion) called a wedge, which could typically block the reduction of explicitly typed terms-therefore loosing the bisimulation with reduction of untyped terms. While the coherence of the abstract coercion c should make it safe to break it apart into two pieces, one attached to the argument N , the other one attached to the body M , this would require new forms of coercions, new reduction rules and quite sophisticated typing rules to keep track of the relation between the residual of wedges after they have been split apart. Even though it should be feasible in principle, this approach seemed far too complicated in the general case to be of any practical use.

Therefore our solution is to give up explicit coercions and leave them implicit. While this removes the problem of wedges at once, it also prevents us from doing a syntactic proof of type soundness. Instead, type soundness in F cc is proved semantically by interpreting types as sets of terms and coercions as proofs of inclusion between types.

Simultaneous coercion abstractions

In order to relax the parametricity restriction of F p ι and allow coercions whose domain and range are simultaneously structured types, while preserving coherence, we permit multiple type abstractions to be introduced simultaneously with all coercion abstractions that constraint them. Since coherence does not come by construction anymore, coherence proofs must be provided explicitly for each block of abstraction as witnesses that the types of coercions are inhabited, i.e. that they can be at least instantiated once in the current environment.

Grouping related abstractions allows to provide coherence proofs independently for every group of abstractions, and simultaneously for every coercion in the same group.

Recursive coercions Recursive types are another interesting new feature of F cc . They are essential in practice and also very useful in theory, as they model several advanced features of programming languages, such as objects or closures. Recursive types are technically challenging however. Thus, they are often presented with some restrictions, for instance, restricting to positive recursion or to the folding-unfolding rules, which are easier to formalize. However, general recursive types are already needed in OCaml or in ML with subtyping constraints. We therefore follow a general approach to recursive types to cover these useful cases. The introduction of recursive coercions is then natural to operate on expressions with recursive types. Quite interestingly, this brings an induction principle for reasoning on recursive types from which the most general subtyping rules for recursive types [Amadio and Cardelli(1993)] are admissible ( §3.3).

From type coercions to typing coercions A type coercion τ ⊲ σ is a proof that all programs of type τ have also type σ in some environment Γ. Pushing the idea of coercions further, typings (the pair of an environment and a type, written Γ ⊢ τ ) are themselves approximations of program behaviors, which are also naturally ordered. Thus, we may consider syntactical objects, which we call typing coercions, to be interpreted as proofs of inclusions between the interpretation of typings. By analogy with type coercions that witness a subtyping relation between types, typing coercions witness a relation between typings. This idea, which was already translucent in our previous work [START_REF] Cretin | [END_REF]], is now internalized.

Interestingly, type generalization can be expressed as a typing coercion-but not as a type coercion: it turns a typing Γ, α ⊢ τ into the typing Γ ⊢ ∀α τ . This allows to replace what is usually a term typing rule by a coercion typing rule, with two benefits: superficially, it allows for a clearer separation of term constructs that are about computation from coercion constructs that do not have computational content (type abstraction and instantiation, subtyping, etc.); more importantly, it makes type generalization automatically available anywhere a coercion can be used and, in particular, as parts of bigger coercions. An illustration of this benefit is that the distributivity rules (e.g. as found in F η ) are now derivable by composing type generalization, type instantiation, and η-expansion (generalization of the subtyping rule for computational types).

The advantage of using typing coercions is particularly striking in the fact that all erasable type system features studied in this paper can be expressed as coercions, so that computation and typing features are perfectly separated.

Language definition

The syntax and semantics of terms

The syntax of the language is given in Figure 2. Because our calculus is implicitly typed, its syntax is in essence that of the λ-calculus extended with pairs. Terms contain variables x, abstractions λx a, applications (a b), pairs a, b , and projections π i a for i in {1, 2}.

Terms also contain two new constructs ∂ a and a ♦ called incoherent abstraction and incoherent application, respectively. The incoherent abstraction ∂ a can be seen as a marker on the term a that freezes its evaluation, while the incoherent application a ♦ allows evaluation of the frozen term a to be resumed. These two constructs enforce a form of weak reduction in a calculus with strong reduction by default. They are required to model GADTs, but removing them consistently everywhere preserves all the properties of F cc . Hence, one can always ignore them in a first reading of the paper.

The reduction rules are given on Figure 4. We write a[x ← b] for the capture avoiding substitution of the term b for the variable x in the term a, defined as usual. Head reduction The terms we are interested in are the sound ones, i.e. whose evaluation never produces an error. We write Ω for the set of errors, which is the subset of syntactically well-formed terms that "we don't want to see" neither in source programs nor during their evaluation: an error is either immediate or occurring in an arbitrary context E (Figure 3); immediate errors are potential redexes D[h] (the application of a destructor D to a constructor h) that are not valid redexes (the left-hand side of a head-reduction rule). Conversely, values are the irreducible terms that we expect as results of evaluation: they are either constructors applied to values or prevalues which are themselves either variables or destructors applied to prevalues. Notice that the definition of errors is independent of the reduction strategy while the definition of values is not. This is

RR n°8456 Γ Θ Γ P Γ Θ, P †
= x | λx a | (a a) | a, a | π i a | ∂ a | a ♦ Terms κ ::= ⋆ | 1 | κ × κ | {α : κ | P} Kinds τ, σ ::= α | τ → τ | τ × τ | ∀(α : κ) τ Types | Π(α : κ) τ | µα τ | ⊥ | ⊤ | | τ, τ | π i τ P ::= ⊤ | P ∧ P | (Σ ⊢ τ ) ⊲ τ Propositions | ∃ κ | ∀(α : κ) P Θ ::= ∅ | Θ, P | Θ, P † Coinduction environments Γ ::= ∅ | Γ, (α : κ) | Γ,
Σ ::= ∅ | Σ, (α : κ) Erasable environments p ::= x | (p v) | π i p | p ♦ Prevalues v ::= p | λx v | v, v | ∂ a Values h ::= λx a | a, a | ∂ a Constructors D ::= ([] a) | π i [] | [] ♦ Destructors E ::= λx [] | ([] a) | (a []) | ✚ ✚ ∂ [] | [] ♦ Contexts | [], a | a, [] | π i [] Figure 3: Notations RedCtx a ❀ b E [a] ❀ E [b] RedApp ((λx a) b) ❀ a[x ← b] RedProj π i a 1 , a 2 ❀ a i RedIApp (∂ a) ♦ ❀ a

Types, kinds, propositions, and coercions

We use types to approximate the behavior of terms, but types are themselves classified by kinds. So let us present kinds first. Although we do not have type functions, we need to manipulate tuples of types because several type variables and coercion constraints sometimes need to be introduced altogether. For sake of simplicity and a slight increase in flexibility, we mix types, type sequences, and constrained types into the same syntactical class of types which are then classified by kinds. Kinds are written κ. The star kind ⋆ classifies sets of terms, as usual. The unit kind 1 and the product kind κ × κ are used to classify the unit object and pairs of types, which combined together, may encode type sequences: for example, a type variable of kind κ 1 × κ 2 may stand for a pair of variables of kinds κ 1 and κ 2 . The constrained kind {α : κ | P} restricts the set κ to the elements α satisfying the proposition P. For instance, {α : ⋆ | α ⊲ τ } is the set of types σ that can be coerced to (e.g. are a subtype of) τ -assuming that α is not free in τ .

Instead of having only proofs of inclusion between sets of terms, which we call coercions, we define a general notion of propositions, written P. Propositions contain the true proposition ⊤, conjunctions P ∧ P, coercions (Σ ⊢ τ ) ⊲ τ , coherence propositions ∃ κ, and polymorphic propositions ∀(α : κ) P. The proposition (Σ ⊢ τ ) ⊲ σ in a context Γ means the existence of a coercion from the typing Γ, Σ ⊢ τ to the typing Γ ⊢ σ. When Σ is ∅, we write τ ⊲ σ for (∅ ⊢ τ ) ⊲ σ and recover the usual notation for type coercions. For example, α ⊲ τ means that α can be coerced to τ (e.g. α is a subtype of τ ). The coherence proposition of the constrained kind {α : κ | P}, namely ∃ {α : κ | P}, gives the usual existential proposition, because coherence corresponds to inhabitation and a type τ is in the constrained kind {α : κ | P} if it is in κ and satisfies P.

Types are described on Figure 2. They are written τ or σ. They contain type variables α, arrow types τ → σ, product types τ × σ, coherent polymorphic types ∀(α : κ) τ , incoherent polymorphic types Π(α : κ) τ , recursive types µα τ , the top type ⊤, and the bottom type ⊥.

Types also contain the unit object , pairs of types τ, τ , and projections π i τ to construct and project type sequences. We define the projections of pairs π i τ 1 , τ 2 to be equal to the

RR n°8456 TermVar (x : τ ) ∈ Γ Γ ⊢ x : τ TermLam Γ ⊢ τ : ⋆ Γ, (x : τ ) ⊢ a : σ Γ ⊢ λx a : τ → σ TermApp Γ ⊢ a : τ → σ Γ ⊢ b : τ Γ ⊢ (a b) : σ TermPair (Γ ⊢ a i : τ i ) i∈{1,2} Γ ⊢ a 1 , a 2 : τ 1 × τ 2 TermProj Γ ⊢ a : τ 1 × τ 2 Γ ⊢ π i a : τ i TermCoer Γ, Σ ⊢ a : τ Γ ⊢ (Σ ⊢ τ ) ⊲ σ Γ ⊢ a : σ TermBlock Γ κ Γ, (α : κ) ⊢ a : τ Γ ⊢ ∂ a : Π(α : κ) τ TermUnblock Γ ⊢ σ : κ Γ ⊢ a : Π(α : κ) τ Γ ⊢ a ♦ : τ [α ← σ]
Figure 5: Term typing rules corresponding components τ i . Type equality is then closed by reflexivity, symmetry, transitivity, and congruence for all syntactical constructs. This defines equality judgments on types (τ 1 = τ 2 ), kinds (κ 1 = κ 2 ), and propositions (P 1 = P 2 ), which are used in typing rules below. Notice that equality is never applied implicitly.

We use environments to approximate the behavior of variables. The syntax of environments, written Γ, is described on Figure 2. Environments are lists of type binders (α : κ) and term binders (x : τ ). We write Σ for environments that do not contain term bindings. We also use lists of propositions, written Θ, called coinduction environments, to keep track of which propositions can be used coinductively.

Let t be a type, a kind, a proposition, a typing environment, a sequence, or a set of such objects. We write fv(t) the set of free variables of t, defined in the obvious way, and t[α ← τ ] for the capture avoiding substitution of τ for the variable α in t. All objects t are taken up to α-conversion of their bound variables.

We assume that environments are well-scoped. That is, Γ, (x : τ ) can only be formed when x / Γ ⊢ κ kind coherence Γ ⊢ Γ environment coherence and well-formedness Γ κ kind well-formedness Γ P prop. well-formedness

We assume that judgments are always well-scoped: free variables of objects appearing on the right of the turnstile must be bound in the typing environment Γ.

Auxiliary judgments

The main two judgments are for terms and coercions. Others are auxiliary judgments and we describe them first.

The kind judgment Γ ⊢ κ states that the kind κ is coherent relative to the environment κ. This judgment is actually equivalent to the proposition judgment Γ ⊢ ∃ κ that will be explained below. The environment coherence and well-formedness judgment Γ ⊢ Γ ′ checks that every kind appearing in Γ ′ is coherent in the environment that precedes it and that every type has kind

Typeeq Γ ⊢ τ : κ κ = κ ′ Γ κ ′ Γ ⊢ τ : κ ′ TypeVar (α : κ) ∈ Γ Γ ⊢ α : κ TypeArr Γ ⊢ τ : ⋆ Γ ⊢ σ : ⋆ Γ ⊢ τ → σ : ⋆ TypeProd Γ ⊢ τ : ⋆ Γ ⊢ σ : ⋆ Γ ⊢ τ × σ : ⋆ TypeFor Γ κ Γ, (α : κ) ⊢ τ : ⋆ Γ ⊢ ∀(α : κ) τ : ⋆ TypePi Γ κ Γ, (α : κ) ⊢ τ : ⋆ Γ ⊢ Π(α : κ) τ : ⋆ TypeBot Γ ⊢ ⊥ : ⋆ TypeTop Γ ⊢ ⊤ : ⋆ TypeUnit Γ ⊢ : 1 TypePair Γ ⊢ τ 1 : κ 1 Γ ⊢ τ 2 : κ 2 Γ ⊢ τ 1 , τ 2 : κ 1 × κ 2 TypeProj Γ ⊢ τ : κ 1 × κ 2 Γ ⊢ π i τ : κ i Γ ⊢ Σ Γ, Σ ⊢ τ : ⋆ Γ ⊢ σ : ⋆ Γ (Σ ⊢ τ ) ⊲ σ
Well-formedness rules are defined in Figure 1.

The type judgment Γ ⊢ τ : κ is defined in Figure 6. Rule TypePack is used to turn a type τ of kind κ satisfying a proposition P into a type of the constrained kind {α : κ | P}. Conversely, TypeUnpack turns back a type of the constrained kind {α : κ | P} into one of kind κ, unconditionally. TypeMu allows to build the recursive type µα τ , which can be formed whenever τ is productive as stated by the judgment α → τ : wf . Other rules are straightforward.

Term typing rules Following the tradition, we write Γ ⊢ a : τ to mean that in environment Γ the term a has type τ . However, we would also like to write this a : Γ ⊢ τ too and say that the term a has the typing Γ ⊢ τ , that is, a is approximated by the type τ whenever its free variables are in the approximations described by Γ. We will keep the standard notation to avoid confusion, but we will read the judgment as above when helpful. The judgment Γ ⊢ a : τ implies that τ has kind ⋆ under Γ whenever Γ is well-formed, as stated below by the extraction lemma (Lemma 21).

Term typing rules are given on Figure 5. Observe that the first five rules are exactly the typing rules of the simply-typed λ-calculus.

The last two rules are for incoherent abstraction and application (they could be skip at first): Rule TermBlock says that the program ∂ a whose evaluation is frozen may be typed with the

Propeq Γ; Θ ⊢ P P = P ′ Γ P ′ Γ; Θ ⊢ P ′ PropVar P † ∈ Θ Γ; Θ ⊢ P PropTrue Γ; Θ ⊢ ⊤ PropAndPair (Γ; Θ ⊢ P i ) i∈{1,2} Γ; Θ ⊢ P 1 ∧ P 2 PropAndProj Γ; Θ ⊢ P 1 ∧ P 2 Γ; Θ ⊢ P i PropForIntro Γ κ Γ, (α : κ); Θ ⊢ P Γ; Θ ⊢ ∀(α : κ) P PropForElim Γ ⊢ τ : κ Γ; Θ ⊢ ∀(α : κ) P Γ; Θ ⊢ P[α ← τ ] PropRes Γ ⊢ τ : {α : κ | P} Γ; Θ ⊢ P[α ← τ ] PropExi Γ ⊢ τ : κ Γ; Θ ⊢ ∃ κ PropFix Γ P Γ; Θ, P ⊢ P Γ; Θ ⊢ P Figure 7: Proposition judgment relation
incoherent polymorphic type Π(α : κ) τ if a can be typed with τ in an extended context that assigns a well-formed kind κ to α. Notice that Γ κ, as opposed to Γ ⊢ κ, does not imply that the kind is coherent, but well-formed. Rule TermUnblck is the counterpart of TermBlock. If we have a term a of an incoherent polymorphic type Π(α : κ) τ , i.e. whose evaluation has been frozen and a type σ of kind κ, we know that the kind κ is inhabited by σ. Therefore, we may safely unfreeze a and give it the type τ

[α ← σ].
Rule TermCoer is at the heart of our approach which delegates most of the logic of typing to the existence of appropriate typing coercions. The rule reads as follows: if a term a admits the typing Γ, Σ ⊢ τ and there exists a coercion from τ to σ introducing Σ under Γ, which we write Γ ⊢ (Σ ⊢ τ ) ⊲ σ, then the term a also admits the typing Γ ⊢ σ. The presence of Σ allows the coercion to manipulate the typing context as well as the type, which is the reason for our generalization from type coercions to typing coercions. When Σ is ∅, the rule looks more familiar and resembles the usual subtyping rule: if a term a has type τ under Γ and there exists a coercion from the type τ to the type σ under Γ (which is written Γ ⊢ τ ⊲ σ), then the term a has also type σ under Γ.

This factorization of all rules but those of the simply-typed λ-calculus under one unique rule, namely TermCoer, emphasizes that coercions are only decorations for terms. Rule TermCoer annotates the term a to change its typing without changing its computational content, as the resulting term is a itself. This is only made possible by using typing coercions instead of type coercions.

Propositions typing judgment

The judgment Γ ⊢ (Σ ⊢ τ ) ⊲ σ is in fact an abbreviation for Γ; ∅ ⊢ (Σ ⊢ τ ) ⊲ σ, which is itself a special case of the more general judgment Γ; Θ ⊢ P when Θ is ∅ and P is (Σ ⊢ τ ) ⊲ σ. Indeed, (Σ ⊢ τ ) ⊲ σ a particular proposition P stating the existence of a typing coercion from τ to σ introducing Σ. The proposition environment Θ contains additional hypotheses that can be used coinductively when proving that a coercion holds.

The proposition judgment is split into two figures, with rules for general propositions in Figure 7 and rules specific to coercion propositions in Figure 8. We first explain typing rules for general propositions.

Rule Propeq allows the use of type equality. Rule PropVar allows the use of a coinductive hypothesis P in Θ. This is written P † ∈ Θ because propositions that are guarded are marked † in Θ and only those are safe to use coinductively.

In particular, rule PropFix which we do not usually find in type systems allows to prove a proposition by coinduction: if P is true assuming P in the unguarded coinduction environment,

RR n°8456

then P is true without this additional hypothesis. Coinductive propositions are introduced as unguarded so that they cannot be used directly, which would be ill-founded. Only some of the coercion rules (described below) allow coinduction to be guarded. The usual rules about recursive types that can be found in other type systems are derivable from this general rule (see Section 3.3).

Rules PropTrue, PropAndPair, and PropAndProj are uninteresting. Rule PropForIntro and PropForElim are unsurprising. Rule PropExi allows to embed the coherence of a kind κ, i.e. the existence of a type inhabitant of kind κ as the proposition ∃ κ. Rule PropRes allows to extract a proposition from a type τ of a constrained kind {α : κ | P}, replacing the variable α of kind κ by the witness τ of kind κ.

Coercions We now explain typing rules for coercion propositions. We may ignore the environment Θ in most cases, as it is just unused or transferred to the premises unchanged, except for the three η-expansion rules that mark the environment as guarded Θ † in their premises, therefore allowing coinductive uses of propositions Θ via Rule PropFix. These are the rules that decompose computational types that have a counterpart in terms, namely CoerArr, CoerProd, and CoerPi.

We now explain coercion rules ignoring Θ. Intuitively, the judgment Γ ⊢ (Σ ⊢ τ ) ⊲ σ implies that any term that admits the typing Γ, Σ ⊢ τ also admits the typing Γ ⊢ σ. (The converse is not true: the fact that any term that admits the typing Γ, Σ ⊢ τ also admits the typing Γ ⊢ σ does not imply that the judgment Γ ⊢ (Σ ⊢ τ ) ⊲ σ is derivable; therefore, the coercion typing judgment is semantically incomplete.) One could expect this judgment to be of the form

(Γ, Σ ⊢ τ ) ⊲ (Γ ⊢ σ), or even (Γ 1 ⊢ τ 1 ) ⊲ (Γ 2 ⊢ τ 2 ).
However, in our notation, Σ describes environment actions under Γ in a compositional manner and eventually permits to go from Γ 1 to Γ 2 .

The coercion typing rules can be understood under the light of Rule TermCoer. The first two rules, CoerRefl and CoerTrans, close the coercion relation by reflexivity and transitivity. To understand CoerTrans let's take a term a with typing Γ, Σ 2 , Σ 1 ⊢ τ 1 . Applying Rule TermCoer with the second premise of Rule TermTrans ensures that the term a admits the typing Γ, Σ 2 ⊢ τ 2 . Applying Rule TermCoer again with the first premise of Rule TermTrans, ensures that a admits the typing Γ ⊢ τ 3 as if we have applied Rule TermCoer to the original typing of a with the conclusion of Rule CoerTrans.

The Rule CoerWeak implements a form of weakening. It tells that if any term of typing Γ, Σ ⊢ τ can be seen as Γ ⊢ σ, then any term of typing Γ ⊢ τ can also be seen as Γ ⊢ σ. Since weakening holds for term judgments, we can do the following reasoning to justify this rule. Assume that the premise Γ, Σ ⊢ τ holds; we argue that the conclusion should also hold. Indeed, a term that admits the typing Γ ⊢ τ also have typing Γ, Σ ⊢ τ by weakening; therefore, by the premise of Rule CoerWeak, it must also have typing Γ ⊢ σ. However, this reasoning is mathematical and based on our interpretation of coercions: Rule CoerWeak is required as it is would not be derivable from other rules-not even admissible-if we removed it from the definition. Notice that this is the only rule that removes binders.

The rules CoerBot and CoerTop close the coercion relation with extrema. For any typing Γ ⊢ τ , there is a smaller typing, namely Γ ⊢ ⊥, and a bigger typing, namely Γ ⊢ ⊤.

The rules CoerProd, CoerArr, and CoerPi close the coercion relation by η-expansion, which is the main feature of subtyping. Here, η-expansion is generalized to typing coercions instead of type coercions. The η-expansion rules describe how the coercion relation goes under computational type constructors, i.e. those of the simply-typed λ-calculus. Interestingly, the ηexpansion rules for erasable type constructors can be derived as their introduction and elimination rules are already coercions.

Intuitively, η-expansion rules can be understood by decorating the η-expansion context with coercions at their respective type constructor. These coercions are erasable because the ηexpansion of a term has the same computational behavior as the term itself.

For example, consider the η-expansion context for the arrow type λx (([] x)). Placing a term with typing Γ, Σ ⊢ τ ′ → σ ′ in the hole, we may give λx (([] x)) the typing Γ ⊢ τ → σ provided a coercion of type Γ, Σ ⊢ τ ⊲ τ ′ is applied around x. The result of the application has typing Γ, Σ ⊢ σ ′ which can in turn be coerced to Γ ⊢ σ if there exists a coercion of type Γ ⊢ (Σ ⊢ σ ′ ) ⊲ σ. Thus, the η-expansion has typing Γ ⊢ τ → σ. While the coercion applied to the result of the application may bind variables Σ for the hole (and the argument), the coercion applied to the variable x needs not bind variables, since the variable x could not use them anyway.

Rules CoerGen and CoerInst, implement the main feature of the language, namely simultaneous coherent coercion abstractions. Intuitively, Rule CoerGen combines several type and coercion abstractions. This is however transparent in rule CoerGen since the simultaneous abstractions are grouped in the kind κ. Hence, this rule looks like a standard generalization rule. The only key here is the left premise that requires the coercion to be coherent. Rule CoerInst is the counter part of CoerGen: it instantiates the abstraction by a type of the right kind. Notice that CoerGen is the only rule using typing coercions in a crucial way and that could not be presented as a coercion if we just had type coercions.

Rule CoerPi is an η-expansion rule and should be understood by typing the η-expansion of the incoherent polymorphic type ∂ ([] ♦), inserting a coercion around the incoherent application. Placing a term with typing Γ, Σ ⊢ Π(α ′ : κ ′ ) τ ′ in the hole, we may first apply weakening to get a typing of the form Γ, (α :

κ), Σ ⊢ Π(α ′ : κ ′ ) τ ′ . By instantiation (Rule TermInst), we get a typing Γ, (α : κ), Σ ⊢ τ ′ [α ′ ← σ ′ ] provided Γ, (α : κ), Σ ⊢ σ ′ : κ ′ . Applying a coercion (Σ ⊢ τ ′ [α ′ ← σ ′ ]) ⊲ τ (Rule TermCoer),
we obtain the typing Γ, (α : κ) ⊢ τ , which we may generalized (Rule TermGen) to obtain the typing Γ ⊢ Π(α : κ) τ of ∂ ([] ♦). Notice that, as Rule CoerGen, we do not require coherence for the kind κ, just its well-formedness. However, we require the coherence of the type environment extension Σ under Γ. This is a very important premise because we do not want the incoherence of κ to leak in Σ and thus under the coercion, because η-expansions are coercions and thus erasable.

Rules CoerFold and CoerUnfold are the usual folding and unfolding of recursive types, which give the equivalence between µα τ and τ [α ← µα τ ]. Interestingly, the usual rules for reasoning on recursive types [Amadio and Cardelli(1993)] are admissible using PropFix (we write

τ 1 ⊳⊲ τ 2 for τ 1 ⊲ τ 2 ∧ τ 2 ⊲ τ 1 ): CoerPeriod α → σ : wf Γ; Θ ⊢ (τ i ⊳⊲ σ[α ← τ i ]) i∈{1,2} Γ; Θ ⊢ τ 1 ⊲ τ 2 CoerEtaMu Γ, (α, β, α ⊲ β); Θ ⊢ τ ⊲ σ Γ; Θ ⊢ µα τ ⊲ µβ σ
Interestingly, the proof for CoerPeriod requires reinforcement of the coinduction hypothesis since we need τ 1 ⊳⊲ τ 2 and not just τ 1 ⊲ τ 2 in the coinduction hypothesis. Finally, the well-foundedness judgment, written α → τ : χ, means that α → τ is well-founded when χ is wf or non-expansive when χ is ne. The rules are unsurprising. The most interesting rules are RecArr, RecProd, and RecPi which ensure well-foundedness provided the components are themselves non-expansive. Conversely, rules RecFor and RecMu just transfer both wellfoundedness and non-expansiveness from their components. For polymorphic types the abstract variable should not appear in its bound to ensure well-foundedness or non-expansiveness. Of course, recursive types can only be well-formed if they are well founded (left premise of RecMu).

CoerRefl Γ ⊢ τ : ⋆ Γ; Θ ⊢ τ ⊲ τ CoerTrans Γ, Σ ′ ; Θ ⊢ (Σ ⊢ τ ) ⊲ τ ′ Γ; Θ ⊢ (Σ ′ ⊢ τ ′ ) ⊲ τ ′′ Γ; Θ ⊢ (Σ ′ , Σ ⊢ τ ) ⊲ τ ′′ CoerWeak Γ; Θ ⊢ (Σ ⊢ τ ) ⊲ σ Γ; Θ ⊢ τ ⊲ σ CoerTop Γ ⊢ τ : ⋆ Γ; Θ ⊢ τ ⊲ ⊤ CoerBot Γ ⊢ τ : ⋆ Γ; Θ ⊢ ⊥ ⊲ τ CoerArr Γ, Σ; Θ † ⊢ τ ⊲ τ ′ Γ; Θ † ⊢ (Σ ⊢ σ ′ ) ⊲ σ Γ; Θ ⊢ (Σ ⊢ τ ′ → σ ′ ) ⊲ τ → σ CoerProd (Γ; Θ † ⊢ (Σ ⊢ τ i ) ⊲ σ i ) i∈{1,2} Γ; Θ ⊢ (Σ ⊢ τ 1 × τ 2 ) ⊲ σ 1 × σ 2 CoerPi Γ κ Γ ⊢ Σ Γ, (α : κ), Σ ⊢ σ ′ : κ ′ Γ, (α : κ); Θ † ⊢ (Σ ⊢ τ ′ [α ′ ← σ ′ ]) ⊲ τ Γ; Θ ⊢ (Σ ⊢ Π(α ′ : κ ′ ) τ ′ ) ⊲ Π(α : κ) τ CoerGen Γ ⊢ κ Γ, (α : κ) ⊢ τ : ⋆ Γ; Θ ⊢ (α : κ ⊢ τ ) ⊲ ∀(α : κ) τ CoerInst Γ, (α : κ) ⊢ τ : ⋆ Γ ⊢ σ : κ Γ; Θ ⊢ ∀(α : κ) τ ⊲ τ [α ← σ] CoerUnfold α → τ : wf Γ, (α : ⋆) ⊢ τ : ⋆ Γ; Θ ⊢ µα τ ⊲ τ [α ← µα τ ] CoerFold α → τ : wf Γ, (α : ⋆) ⊢ τ : ⋆ Γ; Θ ⊢ τ [α ← µα τ ] ⊲ µα τ Figure 8: Coercion judgment relation RecVar α → α : ne RecArr (α → τ i : ne) i∈{1,2} α → τ 1 → σ 2 : wf RecProd (α → τ i : ne) i∈{1,2} α → τ 1 × σ 2 : wf RecFor α / ∈ fv(κ) α → τ : χ α → ∀(β : κ) τ : χ RecPi α / ∈ fv(κ) α → τ : ne α → Π(β : κ) τ : wf RecMu β → τ : wf α → τ : χ α → µβ τ : χ Recwf α / ∈ fv(τ ) α → τ : wf Recne α → τ : wf α → τ : ne

Semantics

A term is sound if none of its reductions lead to an error. To avoid the negation, it is easier to reason with valid terms defined as the complement of Ω, i.e. terms that are not errors, which we write ✵. Hence, a term is sound if all its reduction paths lead to valid terms. Since this construction appears repeatedly, we define the expansion of a set of terms R, which we write (❀ ⋆ R), the set of terms a such that any reduction path starting with a leads to a term in R. The set S of sound terms is the expansion (❀ ⋆ ✵) of valid terms.

Head normal forms ∆ are terms whose root node is a constructor, i.e. abstractions, pairs, and incoherent abstractions, while neutral terms ∇ are variables, applications, projections, and incoherent application. Notice that ∆ and ∇ are complement of one another, i.e. terms are the disjoint union of ∆ and ∇.

Progress is a way to double-check the definition of the semantics, by defining values syntactically and checking that semantic values (irreducible valid terms) are syntactic values (and neutral values are prevalues): The converse is also true, i.e. values do not contain errors. However, this won't remain true when we restrict the strategy, e.g. to call-by-value. In this case, redefining the grammar of values, progress will still hold, but some grammatically well-formed values may contain "inaccessible" errors, such as errors occurring under an abstraction.

Lemma 1 (Progress). If a ∈ ✵ and a ❀ , then a is of the form v. RR n°8456 ⌊x k ⌋ j = x kj ⌊λ k x e⌋ j = λ kj x ⌊e⌋ j ⌊(e f ) k ⌋ j = (⌊e⌋ j ⌊f ⌋ j ) kj ⌊ e 1 , e 2 k ⌋ j = ⌊e 1 ⌋ j , ⌊e 2 ⌋ j kj ⌊π i k e⌋ j = π i kj ⌊e⌋ j ⌊∂ k e⌋ j = ∂ kj ⌊e⌋ j ⌊e ♦ k ⌋ j = ⌊e⌋ j ♦ kj
Type soundness states that well-typed terms are sound. We prove this by interpreting syntactic types as semantic types which are themselves sets of terms. However, since we allow general recursive types the evaluation of terms may not terminate. This is not a problem, since type soundness is not about termination, but ruling out unsound terms, which if they reach an error do so in a finite number of steps.

The idea of step-indexed techniques is to stop the reduction after a certain number of steps, as if some initially available fuel (the number of allowed reduction steps) has all been consumed. Since errors are necessarily reached after a finite number of steps, we may always detect errors with some finite but arbitrary large number of reduction steps.

However, there is a difficulty applying this technique with strong reduction strategies, which we solve by including the fuel inside terms, called indexed terms, and block the reduction internally when terms do not have enough fuel, rather than control the number of reduction steps externally.

The indexed calculus

Terms of the indexed calculus are terms of the λ-calculus where each node is annotated with a natural number called the index (or fuel) of this node. They are written with letter f or e and formally defined on Figure 11: indexed terms are variables x k , abstractions λ k x e, applications (e f ) k , pairs e, f k , projections π i k e, incoherent abstractions ∂ k e, and incoherent applications e ♦ k . We consistently label one hole contexts and errors. We write E k for one-hole context with index k.

Intuitively, indices indicate the maximum number of reduction steps allowed under the given node. Since redexes usually involve several nodes, we must take the minimum of indices of the redex nodes. We use an auxiliary lowering function on indexed terms to keep track of such constraints by lowering the indices in a subterm. It is written ⌊e⌋ j and defined on Figure 10. We use concatenation of indices to denote the minimum of their values. This is not ambiguous since we never use multiplication of indices. Lowering simply changes all indices in the term e with their minimum with j.

The capture avoiding substitution e[x ← f ] of term f for variable x in the term e replaces in e all free occurrences x j of x by ⌊f ⌋ j . The definition is generalized in the obvious way to simultaneous substitutions. We use letter γ to range over substitutions. The lowering of substituted occurrences is necessary to make substitution commute with the lowering function:

Lemma 2. ⌊e[x ← f ]⌋ k = ⌊e⌋ k [x ← f ] = ⌊e⌋ k [x ← ⌊f ⌋ k ]
In particular, renaming commutes with the lowering function.

RR n°8456

e, f :: The reduction rules of the indexed calculus mimic those of the λ-calculus, but with some index manipulation, as described on Figure 12. Reduction can only proceed when the index on the nodes involved in the reduction are strictly positive; the indices are lowered after reduction by the minimum of the involved indices decremented by one. As a corollary, reduction cannot occur at or under a node with a null index. This applies both to head reduction rules (FRedApp, FRedProj, and FRedIApp) and to reduction in an evaluation context (Rule FRedCtx). That is, a head reduction can only be applied along a path of the form

= x k | λ k x e | (e e) k | e, e k | π i k e | ∂ k e | e ♦ k E k ::= λ k x [] | ([] e) k | (e []) k | [], e k | e, [] k | π i k [] | ✚ ✚ ✚ ∂ k [] | [] ♦ k Figure 11: Syntax of indexed terms FRedCtx e ❀ f E k+1 [e] ❀ E k [f ] FRedApp ((λ j+1 x e) f ) k+1 ❀ ⌊e[x ← f ]⌋ kj FRedProj π i k+1 e 1 , e 2 j+1 ❀ ⌊e i ⌋ kj FRedIApp (∂ j+1 e) ♦ k+1 ❀ ⌊e⌋ kj
E k1 1 [. . . E kp p [e]
] when indices k i 's are all strictly positive; they are all decremented after the reduction.

For example, here is a decorated reduction of apply (the λ-term λx λy (x y)) applied to two terms a and b:

(((λ k3+1 x λ j1 y (x j3 y j4 ) j2 ) a) k2+1 b) k1+1 ❀ ((λ j1k2k3 y (⌊a⌋ j3k2k3 y j4k2k3 ) j2k2k3 ) b) k1
Since the reduction happens under the external application, it must have some fuel k 1 + 1, which is decreased by one in the result. Then, for the redex to fire, the application must have some fuel k 2 + 1 as well as the abstraction k 3 + 1, which are both decreased by 1 and combined as k 2 k 3 to lower the result of the reduction. Before that, the term a, which has been substituted for x j3 has been lowered to j 3 in the result. The important feature is that b has not been lowered, which is an important difference with what would happen with the traditional step-indexed approach when indices are outside terms.

Strong normalization By design, the indexed calculus is strongly normalizing, i.e. all reduction paths of all terms are finite. In particular, they are bounded by the index of their root node.

Bisimulation

To show that reduction between undecorated terms and decorated terms coincides, we define ⌊e⌋ the erasure of an indexed term e obtained by dropping all indices. We lift this function to sets of terms: ⌊R⌋ is the set {⌊e⌋ | e ∈ R}. By construction, dropping is stronger than lowering, i.e. dropping after lowering is the same as dropping, or in math, ⌊⌊e⌋ j ⌋ = ⌊e⌋. As for lowering, dropping commutes with substitution: ⌊e

[x ← f ]⌋ = ⌊e⌋[x ← ⌊f ⌋].
We overload the notations Ω and ∇ for the sets of errors and neutral terms for indexed terms. This overloading is not a problem since it is always clear from context which version of terms we mean. Moreover, the definitions coincide with ⌊Ω⌋, and ⌊∇⌋, so it could also be seen as leaving the dropping implicit. We also overload the notation S for the set of sound indexed terms. Although it is defined as for λ-terms as (❀ ⋆ ✵), the meaning is different since the reduction is now bridled by indices.

x j ⋆ x k = j ⋆ k λ j x e ⋆ λ k x f = π i j e ⋆ π i k f = j ⋆ k ∧ e ⋆ f ∂ j e ⋆ ∂ k f = e ♦ j ⋆ f ♦ k = j ⋆ k ∧ e ⋆ f (e 1 e 2 ) j ⋆ (f 1 f 2 ) k e 1 , e 2 j ⋆ f 1 , f 2 k = j ⋆ k ∧ e 1 ⋆ f 1 ∧ e 2 ⋆ f 2
The calculus on indexed terms is just an instrumentation of the λ-calculus that behaves the same up to the consumption of all the fuel. Formally, we show that they can simulate one another, up to some condition on the indices.

Indexed terms can be simulated by λ-terms. That is, if an indexed term can reduce, then the same reduction step can be performed after dropping indices.

Lemma 3 (forward simulation). If e ❀ f , then ⌊e⌋ ❀ ⌊f ⌋.

In order to make the other direction concise, we lift predicates on integers to predicates on indexed terms by requiring the predicate to hold for all indices occurring in the term. For instance, e ≤ k means that the indices in e are smaller or equal to k. This is formally defined on Figure 13.

Indexed terms can simulate λ-terms, provided they have enough fuel. This means that if an indexed term has strictly positive indices and can be reduced after dropping its indices, then the same reduction step can be performed on the indexed term.

Lemma 4 (backward simulation). If e > 0 and ⌊e⌋ ❀ a ′ , then there exists e ′ such that e ❀ e ′ and ⌊e ′ ⌋ = a ′ .

Semantic types

To define semantic types concisely, it is convenient to have a few helper operations on sets of indexed terms. We first lift binary properties on indices to indexed terms. This is done by asking the two terms to share the same skeleton (they drop to the same λ-term) and the indices of corresponding nodes to be related by the property on indices. A formal definition is given in Figure 14.

The interior of a set R is the set R↓ containing all terms smaller than a term in R, i.e. {f | ∃e ∈ R, f ≤ e}. The contraction of a set R is the set (R❀) of all terms obtained by one-step reduction of a term in R, i.e. {f | ∃e ∈ R, e ❀ f }.

A pretype is a set of sound terms that contains both its interior and its contraction. We write P the set of pretypes.

Definition 5 (Pretypes).

P def = {R ⊆ S | R↓ ∪ (R❀) ⊆ R} RR n°8456
Notice that the empty set and S are pretypes. Pretypes only contain sound terms since types will be pretypes and types will be sets of sound terms. The closure of pretypes by interior is just technical. The main property of pretypes is to be closed by reduction. Types are pretypes that are also closed by a form of expansion. As a first approximation, sound terms that reduce to a term in a type R should also be in R. However, a type R should still not contain unsound terms even if these reduce to some term in R. Moreover, the meaning of a set of terms R is in essence determined by its set of head normal forms, which we call the kernel of R. We use concatenation for intersection of sets of terms. Hence, the kernel of R is ∆R. A type R need not contain every head normal form that reduces to some term in R. Consider for example the term e 0 equal to λx x and one of its expansion is the term e 1 equal to λx ((λy x) (x x)). The sets {e 0 } and {e 0 , e 1 } have quite different meanings. Notice that by definition, the kernel is an idempotent operation:

∆(∆R) = ∆R.
The expansion-closure of a set of terms R, written ♦ R, is the set (❀ ⋆ (∇✵ ⊎ ∆R)), which contains terms of which every reduction path leads to either a valid neutral term or a head normal form of R. By definition, the expansion closure is monotonic:

if R ⊆ S, then ♦ R ⊆ ♦ S; it is also idempotent: ♦ (♦ R) = ♦ R.
Finally, semantic types are pretypes that are stable by expansion closure:

Definition 6 (Semantic types). ❚ def = {R ∈ P | ♦ R ⊆ R}.
The kernel of a type is a pretype-but not a type. Conversely, the expansion-closure of a pretype is a type. Actually expansion-closure and kernel are almost inverses of one another: if R is a type, then ♦ (∆R) = R.

The smallest type, called the bottom type and written ⊥, is equal to ♦ {}, that is (❀ ⋆ (∇✵)). The largest type, ⊤, called the top type is the set S of sound terms.

Simple types

We can now define the semantics of functions and products as semantic type operators.

Definition 7 (Arrow, product, and incoherent operators).

R → S def = ♦ {λ k x e ∈ S | k > 0 ⇒ ∀f, ⌊f ⌋ k-1 ∈ R ⇒ ⌊e[x ← f ]⌋ k-1 ∈ S} R × S def = ♦ { e, e ′ k ∈ S | k > 0 ⇒ ⌊e⌋ k-1 ∈ R ∧ ⌊e ′ ⌋ k-1 ∈ S} ΠI F def = ♦ {∂ k e | k > 0 ⇒ ∀i ∈ I ⌊e⌋ k-1 ∈ F i }
The arrow, product, and incoherent operators preserve types.

Lemma 8. If R and S are types, then so are R → S and R × S. Lemma 9. If F i is type for all i ∈ I, then so is ΠI F.

The proof uses the following easy properties on indices:

• ⌊⌊e⌋ j ⌋ k = ⌊e⌋ kj • If k ′ ≤ k and e ′ ≤ e, then ⌊e ′ ⌋ k ′ ≤ ⌊e⌋ k . • If e ′ ≤ e and f ′ ≤ f , then e ′ [x ← f ′ ] ≤ e[x ← f ].
And this less easy one: Lemma 10. If e ❀ f holds, then ⌊e⌋ k+1 ❀ f ′ and ⌊f ⌋ k ≤ f ′ for some f ′ .

RR n°8456

Proof. We only detail the proof for the arrow operator, which uses indexed terms in a crucial way. The proof for the product operator is similar, but easier. Since the arrow operator is defined by expansion-closure, it is a type if its kernel is a pretype. Its kernel contains only sound terms by definition. So it remains to show that the definition contains its interior and contraction.

Let λ j x e ′ ≤ λ k x e (1), λ k x e ∈ S (2), and

k > 0 ⇒ ∀f, ⌊f ⌋ k-1 ∈ R ⇒ ⌊e[x ← f ]⌋ k-1 ∈ S (
3), and show that λ j x e ′ ∈ S (4) and j > 0 ⇒ ∀f, ⌊f ⌋ j-1 ∈ R ⇒ ⌊e ′ [x ← f ]⌋ j-1 ∈ S (5). The first assertion (4) comes easily with (1) and (2) since S contains its interior. To show (5), let j > 0 and ⌊f ⌋ j-1 ∈ R (6) and show ⌊e ′ [x ← f ]⌋ j-1 ∈ S (7). By (1) we have j ≤ k, so k > 0. We also have ⌊⌊f ⌋ j-1 ⌋ k-1 = ⌊f ⌋ j-1 which is in R by ( 6). So from (3) we have ⌊e

[x ← ⌊f ⌋ j-1 ]⌋ k-1 ∈ S.
Since S is a type, it contains its interior so ⌊e ′ [x ← ⌊f ⌋ j-1 ]⌋ j-1 ∈ S. Since the substitution and the lowering function commute, we conclude (7).

Let λ k x e ❀ e 1 (8), λ k x e ∈ S (9), and

k > 0 ⇒ ∀f, ⌊f ⌋ k-1 ∈ R ⇒ ⌊e[x ← f ]⌋ k-1 ∈ S (10)
. By inversion of the reduction relation we have k = k ′ + 1 and e 1 = λ k ′ x e ′ for some k ′ and e ′ such that e ❀ e ′ (11). We now have to show that λ k ′ x e ′ ∈ S (12) and 13). We show ( 12) with ( 8) and ( 9) since S contains its contraction. To show (13), let k ′ > 0 and ⌊f ⌋

k ′ > 0 ⇒ ∀f, ⌊f ⌋ k ′ -1 ∈ R ⇒ ⌊e ′ [x ← f ]⌋ k ′ -1 ∈ S (
k ′ -1 ∈ R (14) and show ⌊e ′ [x ← f ]⌋ k ′ -1 ∈ S (15). We have ⌊⌊f ⌋ k ′ -1 ⌋ k-1 = ⌊f ⌋ k ′ -1 which is in R by (14). So from (10) we have ⌊e[x ← ⌊f ⌋ k ′ -1 ]⌋ k-1 ∈ S.
Since S is a type, it contains its contraction and interior so ⌊e ′ [x ← ⌊f ⌋ k ′ -1 ]⌋ k ′ -1 ∈ S by Lemma 10. Since the substitution and the lowering function commute, we conclude (15).

Intersection types

The intersection i∈I R i of a nonempty family of types (R i ) i∈I is a type. (As a particular case, the bottom type ⊥ is also the intersection of all types.)

Recursive types

This section follows the usual description of recursive types using approximations as done in [Appel and McAllester(200 This addition of recursive types is the main reason for using a step-indexed semantics. However, while they require the need for step-indexed semantics, they do not raise any difficulty once the semantics has been correctly set up.

The k-approximation of a set R, written R k is the subset {e ∈ R | e < k} of element of R that are smaller than k

The following properties of approximations immediately follow from the definition. R 0 is the empty set; a sequence of approximations is the approximation by the minimum of the sequence: R j k = R jk ; Two sets of terms that are equal at all approximations are equal: If R k = S k holds for all k, then R = S.

Definition 11 (Well-foundness). A function F on sets of terms is well-founded (resp. nonexpansive) if for any set of terms R, the approximations of

F R and F R k are equal at rank k + 1 (resp. k), i.e. F R k+1 = F R k k+1 (resp. F R k = F R k k )
Intuitively, well-foundedness (resp. non-expansiveness) ensures that F builds terms smaller than k + 1 (resp. k) by only looking at terms smaller than k in its argument.

The iteration of a well-founded function F does not look at its argument for terms of small indices:

F k R k is independent of R; in particular, it is equal to F k ⊥ k . Therefore, F j R kj and F k R kj are equal.
Definition 12 (Recursive operator). Given a well-founded function F on sets of terms, we define μ F as the set of terms k≥0 F k ⊥ k .

The recursive operator preserves semantic types: Lemma 13. If F is well-founded and maps semantic types to semantic types, then μ F is a semantic type.

Moreover, recursive types can be unfolded or folded as expected: if F is well-founded, then μ F = F (μ F). This is proved by showing that μ F k is equal to both F k ⊥ k and F (μ F) k for every k.

The following Lemma, which although in a different settings, is stated exactly as with traditional step-indexed semantics [Appel and McAllester(2001)]:

Lemma 14. We have the following properties:

• Every well-founded function is non-expansive. • X → X is non-expansive. • X → R where X is unused in R (R is constant) is well-founded.
• The composition of non-expansive functors is non-expansive.

• The composition of a non-expansive functor with a well-founded functor (in either order) is well-founded.

• If F and G are non-expansive, then X → F X → G X and X → F X × G X are well-founded. • If (F i ) i∈I is a family of non-expansive functors, then X → Πi∈I (F i X) is well-founded. • If (F i ) i∈I is a family of non-expansive (resp. well-founded) functors, then X → i∈I (F i X)
is non-expansive (resp. well-founded).

• If X → F X Y is non-expansive (resp. well-founded) for every Y and F X is well founded for every X, then X → μ (F X) is non-expansive (resp. well-founded).

Just for illustration X → X → S is well-founded since X → X is non-expansive and X → S is constant, thus well-founded, and therefore non-expansive.

Semantic judgment

A binding is a pair (x : R) of a variable and a semantic type. A context is a set of bindings (x : R), defining a finite mapping from term variables to types. We say that a substitution γ is compatible with a context G and we write γ : G if dom(γ) and dom(G) coincide and for all (x : R) in G, the term γ x is in R.

We define the semantic judgment G |= S as the set of terms e such that γ e is in S for any substitution γ "compatible" with G.

Definition 15 (Semantic judgment).

γ :

G def = ∀(x : R) ∈ G, γ x ∈ R G |= S def = {e | ∀γ : G, γ e ∈ S}
We may now present the semantic typing rules for the simply-typed λ-calculus.

Lemma 16 (Variable). If R is a type and (x : R) is in G, then x k is in G |= R.

RR n°8456

Proof. Let γ be compatible with G (1). We show that γ x k is in R. Since (x : R) is in G, we have γ x in R by ( 1), Being a type, R is closed by lowering. Hence, ⌊γ x⌋ k is also in R. By definition of substitution, this is equal to γ x k , which is thus also in R.

Lemma 17 (Abstraction). If R and S are types and e is in G, (x : R) |= S, then

λ k x e is in G |= R → S.
Proof. Let γ be compatible with G (1). We show that γ (λ k x e) is in R → S (2). Assume γ (λ k x e) ❀ ⋆ e 1 . Then e 1 is necessarily of the form λ j x e ′ where γ e ❀ ⋆ e ′ .

We first show that λ j x e ′ ∈ S (3). Since γ is compatible with G, γ, x → x is compatible with G, (x : R) as variables are in all types. Since e is in (G, (x : R) |= S), we have (γ, x → x) e, i.e. γ e in S. Since S is closed by reduction, we have e ′ in S and a fortiori in S. This implies (3).

Assume j > 0 and ⌊f ⌋ j-1 ∈ R. Let γ ′ be γ, x → ⌊f ⌋ j-1 . By construction γ ′ : G, (x : R). Since e is in (G, (x : R) |= S), we have γ ′ e in S and, since S is closed by reduction, e ′ [x ← ⌊f ⌋ j-1 ] is also in S. By decreasing index we have ⌊e ′ [x ← ⌊f ⌋ j-1 ]⌋ j-1 ∈ S, from which by Lemma 2 becomes ⌊e ′ [x ← f ]⌋ j-1 ∈ S. This ends the proof of (2).

Lemma 18 (Application). If R and S are types, e is in G |= R → S, and f is in G |= R, then (e f ) k is in G |= S for any k.
Proof. Let γ be compatible with G. We show that γ (e f ) k ∈ S. By hypotheses we have γ e ∈ R → S and γ f ∈ R. We prove the more general result that for all k, e, and f , if e ∈ R → S and f ∈ R hold, then (e f ) k ∈ S also holds. This is proved is by induction over the strong normalization of e and f using the closure expansion of S.

The term (e f ) k is neutral. It is also valid since e and f are sound and, by construction of R →S, e is an abstraction when in normal form. If (e f ) k reduces by a context rule, we use our induction hypothesis. Otherwise, e must be of the form λ j+1 x e ′ for some j and e ′ and k be of the form k ′ + 1 and the reduction is

(e f ) k ❀ ⌊e ′ [x ← f ]⌋ jk ′ . It remains to show ⌊e ′ [x ← f ]⌋ jk ′ ∈ S (1).
We have ⌊f ⌋ j ∈ R by stability under decreasing index. So, we have ⌊e ′ [x ← f ]⌋ j ∈ S by definition of the arrow operator. Then (1) follows by stability under decreasing index.

Lemma 19 (Pairs). Let R 1 and R 2 be types.

If e i is in G |= R i , then e 1 , e 2 k is in G |= R 1 × R 2 . If e in G |= R 1 × R 2 , then π i k e is in G |= R i .
Lemma 20 (Incoherent). Let F i be types for all

i ∈ I. If e is in G |= F i for all i ∈ I, then ∂ k e is in G |= ΠI F. If e in G |= ΠI F, then e ♦ k is in G |= F i for all i ∈ I.
Note that when S is a type and R is a type for all (x : R) ∈ G, then G |= S is a pretype.

Soundness

In order to show the soundness property we need the extraction lemma (Lemma 21), which uses the usual weakening and substitution lemmas.

Lemma 21 (Extraction). If ∅ Γ holds, then the following properties hold:

• If Γ ⊢ κ holds, then Γ κ holds.

• If Γ ⊢ τ : κ holds then Γ κ holds.

• If Γ; Θ ⊢ P and Γ Θ hold then Γ P holds.

• If Γ ⊢ a : τ holds then Γ ⊢ τ : ⋆ holds.

RR n°8456

The soundness proof is not direct. We will translate the F cc type system from the λ-calculus to a temporary type system on the indexed calculus. We will prove soundness for the indexed calculus type system and migrate the result to the λ-calculus type system. The relation between both type systems will be that if a λ-term is well-typed then all indexed terms that drop to this λ-term are well-typed too. And reciprocally, if an indexed term is well-typed, then its dropped λ-term is well-typed too. Both directions preserve the typing (the pair of the environment and type). Notice that only the term judgment needs to be changed since it is the only one talking about terms.

Syntactically, the indexed term judgment e : Γ ⊢ τ contains the exact same rules as those of the λ-term judgment. However index annotations now appear on the term node we are typing. This annotation has no constraint, which gives us that if a term is typed with annotations it can be typed without and reciprocally if a term is typed without annotations it can be typed with any annotations.

Lemma 22. The following assertions hold:

• If e : Γ ⊢ τ holds, then ⌊e⌋ : Γ ⊢ τ holds.

• If a : Γ ⊢ τ holds, then e : Γ ⊢ τ holds for all e such that ⌊e⌋ = a.

To state and prove the soundness of the indexed type system we interpret (syntactic) kinds, types, propositions, and typing environments.

We interpret kinds as sets of mathematical objects, which are either sets of terms, the unit object, or pairs of objects. The kind star is interpreted as the set of sets of terms. The unit kind is interpreted as the singleton containing the unit object. The product kind is interpreted as the cartesian product of the interpretation of its components. The constrained kind is interpretated as the subset of the interpretation of its kind satisfying its proposition.

Definition 23 (Kind interpretation). The interpretation of a kind κ under η, written |κ| η is the mathematical object recursively defined as:

• |⋆| η = sets of terms

• |1| η = { } • |κ 1 × κ 2 | η = { x 1 , x 2 | x 1 ∈ |κ 1 | η ∧ x 2 ∈ |κ 2 | η } • |{α : κ | P}| η = {x ∈ |κ| η | ∀k |P| k η,α →x }
The interpretation of a syntactic type is a semantic type, but it is parametrized over a mapping from type variables to semantic types written η. The interpretation of a type variable is its value in the mapping. If it is not present in the mapping, the unit semantic type is returned. The interpretation of arrow, product, and incoherent polymorphic types simply use the arrow, product, and incoherent operators defined in §4.4. The interpretation of the coherent polymorphic type ∀(α : κ) τ under η is the intersection of all interpretations of τ under η, α → x where x ranges in the interpretation of κ under η. The interpretation of the recursive type µα τ under η is the infinite iteration of the functor mapping X to the interpretation of τ under the extension of η mapping α to X-which corresponds to the infinite unfolding of the recursive type. Top and bottom are mapped to their semantic equivalent. Finally, the unit type, pairs of types, and projections of types, are interpretated to their mathematical equivalent.

Definition 24 (Type interpretation). The interpretation of a type τ under η, written |τ | η is the set of terms recursively defined as:

• |α| η = η(α) • |τ → σ| η = |τ | η → |σ| η • |τ × σ| η = |τ | η × |σ| η • |Π(α : κ) τ | η = Π|κ| η (x → |τ | η,α →x ) • |∀(α : κ) τ | η = |κ| η (x → |τ | η,α →x ) • |µα τ | η = μ (X → |τ | η,α →X ) • |⊥| η = ⊥ • |⊤| η = ⊤ • | | η = • | τ, σ | η = |τ | η , |σ| η • |π i τ | η = π i |τ | η
We define the interpretation of environments, written |Γ| γη , as the pair of a term substitution (a mapping from term variables to indexed terms) and a semantic type mapping (from type variables to semantic types). The interpretation is parametrized by initial mappings γ and η. The empty environment is interpreted by the singleton set containing the initial mappings. The interpretation of an environment Γ extended with a term binding (x : τ ) extends the term mappings in the interpretation of Γ with x bound to a term in the interpretation of τ under the associated type mapping. The interpretation of an environment Γ extended with a type binding (α : κ) extends the type mapping with an element of the interpretation of κ.

We define the interpretation of proposition indexed by a type mapping η and an index k. The true and conjonction proposition are interpretated to their mathematical analogs. The coercion proposition is interpretated to the inclusion of ∀Σ τ in σ for terms smaller than k. The coherence proposition is interpretated as the inhabitation of the kind. And the polymorphic proposition is interpretated as quantified assertion.

Definition 25 (Proposition interpretation). The interpretation of a proposition P under η with k, written |P| k η is the mathematical assertion recursively defined as:

• |⊤| k η = True • |P 1 ∧ P 2 | k η = |P 1 | k η ∧ |P 2 | k η • |(Σ ⊢ τ ) ⊲ σ| k η = ∀e < k (∀η ′ ∈ |Σ| η e ∈ |τ | η ′ ) ⇒ e ∈ |τ | η • |∃ κ| k η = ∃x ∈ |κ| η • |∀(α : κ) P| k η = ∀x ∈ |κ| η |P| k η,α →x
The coinduction environment interpretation |Θ| k η is a conjonction of mathematical assertions for each proposition: when the proposition is not guarded, it holds for all indices smaller than k; when it is guarded, it also holds for k and is thus accessible.

RR n°8456

Definition 26 (Coinduction environment semantics). We define |Θ| k η as follows:

• |∅| k η = True • |Θ, P| k η = |Θ| k η ∧ ∀j < k |P| j η • Θ, P † k η = |Θ| k η ∧ ∀j ≤ k |P| j η
We write |Γ| to stand for |Γ| ∅∅ . And we write |Γ| η the second projection of |Γ| Gη , which does not depend on G, since the type mapping does not depend on the term mapping.

Definition 27 (Environment semantics). We define |Γ| Gη as follows:

• |∅| Gη = {Gη} • |Γ, (x : τ )| Gη = {(G ′ , (x : |τ | η ′ )η ′ | G ′ η ′ ∈ |Γ| Gη } • |Γ, (α : κ)| Gη = {G ′ (η ′ , α → x) | G ′ η ′ ∈ |Γ| Gη ∧ x ∈ |κ| η ′ )}
We have the following lemmas. If τ is non-expansive (resp. well-founded) with respect to α, then its interpretation as a functor is also non-expansive (resp. well-founded). If a concatenated environment is well-formed then the interpretation of the second one under the first is nonempty. If a kind is coherent, then it is inhabited. If a type is well-kinded, then its interpretations under all type mappings in the interpretation of its environment is in the interpretation of its kind. If a proposition P is proved under Θ, then for all mappings and indices the interpretation of P holds if the interpretation of Θ does too. The interpretation of a coherent type environment is not empty and only contains semantic types. Finally, a well-typed term is in the semantic judgment of the interpretation of its typing.

Lemma 28. The following assertions hold.

• If α → τ : ne holds, then (X → |τ | η,α →X ) is non-expansive. • If α → τ : wf holds, then (X → |τ | η,α →X ) is well-founded. • If Γ ⊢ κ holds, then ∀η ∈ |Γ| |κ| η = ∅ holds. • If Γ ⊢ τ : κ holds, then ∀η ∈ |Γ| |τ | η ∈ |κ| η holds. • If Γ; Θ ⊢ P holds, then ∀η ∈ |Γ| ∀k |Θ| k η ⇒ |P| k η holds. • If Γ ⊢ Γ ′ holds, then ∀η ∈ |Γ| |Γ ′ | η = ∅ holds. • If Γ ⊢ Γ ′ holds, then ∀η ∈ |Γ| ∀(x : R) ∈ |Γ ′ | ∅η R ∈ ❚ holds. • If Γ ⊢ e : τ holds, then ∀Gη ∈ |Γ| e ∈ G |= |τ | η holds.
The filling of λ-term a at rank k is the indexed-term obtained by annotating each node of a with index k (Figure 15). By construction, we have ⌊⌈a⌉ k ⌋ = a.

Theorem 29 (Soundness). If ∅ ⊢ Γ and Γ ⊢ a : τ hold, then a is sound. Termination in the absence of recursive types Although evaluation may not terminate because of the presence of recursive types, it remains interesting to show that recursive types are the only source of non-termination. We already know this in System F. We show that coercions do not themselves introduce non-termination, as long as all types remain non-recursive. The proof is based on reducibility candidates as for System F and does not raise any difficulties. We thus omit the details.

RR n°8456 ⌈x⌉ k = x k ⌈λx a⌉ k = λ k x ⌈a⌉ k ⌈(a b)⌉ k = (⌈a⌉ k ⌈b⌉ k ) k ⌈ a 1 , a 2 ⌉ k = ⌈a 1 ⌉ k , ⌈a 2 ⌉ k k ⌈π i a⌉ k = π i k ⌈a⌉ k ⌈∂ a⌉ k = ∂ k ⌈a⌉ k ⌈a ♦⌉ k = ⌈a⌉ k ♦ k
Theorem 30 (Termination). If ∅ ⊢ Γ and Γ ⊢ a : τ hold in the sublanguage without recursive types and coinduction, then a strongly normalizes.

Subject reduction While by definition, there is subject reduction on semantic types (as they are closed by reduction), we do not have subject reduction syntactically. This just means that the type system is too rough an approximation to still capture the invariant of programs after they have been reduced.

Confluence Because we have mixed strong and block reduction, we have lost confluence. This is a known problem with a known fix. One solution is to extend the language with a restricted form of explicit subsitutions so that substitution may be held at the frontier of block terms until these terms would be unblock. We have not done the instrumentation to avoid complicating the language. Besides, if we remove incoherent abstraction and application, then the language is the λ-calculus and confluence holds again.

Coq development

We have a Coq development of the soundness proof for F cc . This Coq development also contains a proof of equivalence between 2 versions of the typing rules: a version with minimum redundancy, and a more redundant version used to prove soundness. This version is necessary for the induction hypothesis to hold even for extracted judgments and not only the direct premises.

The development differs from the paper by using de-Bruijn indices and using two homogeneous environments (one for types and one for terms) instead of a heterogeneous dependent one. The development can be found online.2

Expressivity

The language F cc is more expressive than F p ι : apart from the change of presentation, moving from type coercions to typing coercions and from explicit coercions to implicit coercions, the only significant change is for type and coercion abstraction: the new construct of F cc which by design generalizes the two forms of coercion abstraction in F p ι . Indeed, we can choose ⊥ (resp. ⊤) to witness coercions that are parametric in their domain (resp. range). Therefore the languages F <: , ML F , and F η which are subsumed by F p ι can also be seen as sublanguages of F cc .

Encoding subtyping constraints

We claim that languages with ML-like subtyping constraints [START_REF] Odersky | Type inference with constrained types[END_REF]Odersky, Sulzmann, and Wehr] can be simulated in F cc . With subtyping constrains, term judgments may be written A ⊢ e : τ | C where A is the environment, e the expression, τ its type, and C is a sequence of subtyping constraints, e.g. as in [Pottier(1996)].

To ease the embedding of subtyping constraints in F cc , we slightly abuse of notations. First, we see let-bindings as the usual syntactic sugar for redexes. We write α for a sequence of variables α 1 . . . α n where n is left implicit. Given a sequence of variables α, we see α i as α.i, the i'th projection of α. We write (α | P) as a shorthand for the type binding Type systems with subtyping constraints use two notions, solvability and consistency, that coincide in ML. Solvability means that one can find a ground instance for type variables that solves the constraints. Consistency means that transitive and congruence closure of the set of constraints does not contain inconsistencies.

We claim that solvability of a set of constraints C implies the consistency of the translation of C, since it amounts to exhibit type witnesses such that the constraints hold. These witnesses lie in a syntax with simple types and recursive types. Moreover, since solvability is equivalent to consistency, we conclude that consistency is equivalent to coherence.

The two interesting typing judgments for subtyping constraints are for let-binding and subsumption. These are as follows and are derivable in F cc :

α ⊢ σ α ⊢ C ′ [β ← σ] (α | C), Γ, (x : ∀(β , C ′ )τ ) ⊢ b : ρ (α, β | C ′ ), Γ ⊢ a : τ (α | C), Γ ⊢ ((λx b) a) : ρ (α | C), Γ ⊢ a : τ (α | C ′ ) ⊢ C ∧ τ ⊲ σ (α | C ′ ), Γ ⊢ a : σ
However, there remain two differences with the way subtyping constraints are usually handled. A judgment A ⊢ e : τ | C is valid when C is consistent while our corresponding judgment (fv(A, C, τ ) | C), A ⊢ e : τ is valid when C is solvable, i.e. ⊢ (fv(C) | C), which must exhibit a substitution θ of domain fv(C) such that ∅ ⊢ Cθ. While consistency and solvability coincide in ML with subtyping constraints, this need not be the case. Consistency is a semantic property while solvability is a syntactic property. Using consistency instead of solvability, we only have to verify a property of the constraints without having to exhibit a concrete solution. Consistency is more flexible than solvability. In practice, it can also be checked more modularly.

We already have some flexibility to reason about coherence in F cc using propositions and assumptions in the typing context. However, constraint entailment differs in both systems. In particular, we cannot express the decomposition of typing constrains, e.g. deduce the consistency of σ ⊲ σ ′ from the consistency of τ → σ ⊲ τ → σ ′ , as is the case with subtyping constraints.

The reason is that subtyping constraints are syntactic and taken in a closed-world view: subtyping relations that cannot be expressed syntactically do not hold, which can be used to reinforce constraint entailment. Our approach in F cc is semantic and syntactic coercions must be interpreted in the semantics. Since our semantics has more types and coercions than the syntax allows to build, some reasoning principles that would be true from a purely syntactic point of view will not hold in our semantics and thus cannot be added in the syntax. We are bound to an open-world view. Still, it would be interesting to see how our approach could be extended to allow a form of closed world view and express some negative information.

Encoding GADTs

Incoherent polymorphism is necessary for features that contain some form of dynamic typing, such as GADTs. It may also be a simplification for the programmer that does not have to provide the witness type that proves the coherence-but at his own risk of delaying type errors.

In this subsection we show how GADTs can be encoded with incoherent polymorphism and also how coherence and incoherent polymorphism can be interestingly mixed.

Incoherent polymorphism permits type abstraction for any well-formed kind: inhabited kinds, potentially inhabited kinds, and empty kinds. In the polymorphic type Π(α : κ) τ , the coherence of kind κ may depend over some type variable β of the type environment. Depending on how β is instantiated, the kind κ may or may not be inhabited.

Before we give a concrete example, let us first introduce existential types by their CPS encoding. Because we have two notions of polymorphism, coherent and incoherent, we also have two notions of existential types: we write ∃(α : κ) τ for coherent existential types and Σ(α : κ) τ for incoherent existential types3 defined as follows.

coherent:

∃(α : κ) τ def = ∀β (∀(α : κ) (τ → β)) → β incoherent: Σ(α : κ) τ def = ∀β (Π(α : κ) (τ → β)) → β
We define the pack and unpack term syntactic sugar for the coherent existential, and ipack and iunpack for their incoherent version. Notice that the body of the iunpack sugar is hidden under an incoherent type abstraction, and as such is allowed to be unsound because it cannot be reduced. Let's assume we have type-level functions and sum types. We can now define the following GADT, named Term, and with kind ⋆ → ⋆ (where τ ⊳⊲ σ stands for τ ⊲ σ ∧ σ ⊲ τ as above):

Term α def = Σ(β : ⋆ × ⋆ | α ⊳⊲ (π 1 β → π 2 β)) α + ∃β Term (β → α) × Term β
This GADT is the sum of an incoherent existential type and a coherent one. The incoherent existential type requires α to be an arrow type and stores a term of such type; it also names π 1 β the argument type and π 2 β its return type. The coherent existential type adds no constraint on α but stores a pair such that its first component applied to its second component is of type α; it names β the intermediate type. The Term GADT contains two constructors: one for the left-hand side of the sum injecting functions and one for the right-hand side of the sum freezing function applications. We can define its two constructors in the following manner:

Lam x def = inl (ipack x) : ∀α ∀β (α → β) → Term (α → β) App y x def = inr (pack y, x ) : ∀α ∀β Term (α → β) → Term α → Term β
We can now define a recursive eval function taking a term of type Term α and returning a term of type α for all type variable α. Said otherwise, eval has type ∀α (Term α → α). When the argument is on the left-hand side of the sum, eval simply unpacks it and returns it. When the argument is on the right-hand side of the sum, eval fist unpacks it as a pair and applies the evaluation of the first component to the evaluation of the second component. We thus use the incoherent version of unpacking on the left-hand side and the coherent version on the right-hand side.

eval x = case x of { inl x 1 → iunpack x 1 as y in y | inr x 2 → unpack x 2 as y in (((eval ()π 1 y)) ((eval ()π 2 y)))}

Let's now suppose that we call eval with a term of type Term (τ × σ). This term is necessarily from the right-hand side of the sum because τ × σ cannot be equivalent to an arrow type by consistency. However, in the first branch, in the body of the inconsistent unpack, we have access to the proposition τ × σ ⊳⊲ π 1 β → π 2 β which is inconsistent. This sort of inconsistency in some branches of case expressions is frequent with GADTs. Notice however, that we can reduce the second branch because we used a coherent existential type since there is a witness for β for any instantiation of α.

Discussion

We first compare F cc with our prior work and other related works; we then discuss language extensions and future works.

Comparison with F p ι

The closest work is of course our previous work on F p ι of which F cc is an extension. The main improvement in F cc is the ability to abstract other arbitrary constrains, but as a serious drawback one has to provide coercion witnesses to ensure the coherence.

Coherence is sufficient for type soundness, but in an explicit language of coercions it does not suffice for subject reduction, which also requires that the language has a rich syntactic representation to keep track during the reduction of invariants expressed by coercions. Our approach in F cc is to avoid the need for decomposing abstract coercions into smaller ones by presenting an implicit version of the language. This also avoids introducing new coercion constructs in the language and their associated typing rules-which we failed to prove to be sound by syntactic means in an explicit language of coercions.

Therefore, moving from F p ι to F cc has a cost-the lost an explicit calculus of coercions with subject reduction. Of course, one can still introduce explicit syntax for coercion typing rules in the source so as to ease type checking, but terms with explicit coercions will not have reduction rules in F cc .

An interesting question is whether there are interesting languages between F p ι and F cc that would still have a (relatively simple) calculus of explicit coercions. If we restrict to certain forms of coercions, instead of general coercions, the question of coherence may be much simpler. For example, one could just consider equality coercions as in the language FC.

In F cc , we simultaneously abstract over a group of type variables and coercions that constrain those variables. The choice of grouping must be such that the group is coherence for all possible instantiation of variables in the context.

We have also explored a syntactically more atomic version of F cc where type and coercion abstraction are separate constructs as in F ι [START_REF] Cretin | [END_REF]]. Namely, the usual type abstraction ∀α τ and coercion abstraction (τ 1 ⊲ τ 2 ) ⇒ σ-a term of type σ under the hypothesis that τ 1 ⊲ τ 2 holds. For instance, this would permit to write a function of type ∀α (α → (τ 1 ⊲ τ 2 ) ⇒ σ) and apply it to a type parameter, then to a value of type α, and finally to a coercion. However, this additional flexibility is negligible, these are just η-expansion variants of terms in F cc . Moreover, related type abstractions and coercions should still be checked simultaneously. That is, even if the arguments are passed separately, the typing derivation must maintain a notion of grouping underneath so as to check for coherence. The solution in F cc seems a better compromise between simplicity and expressiveness.

Comparison with other works

To the best of our knowledge there is no previous work considering typing coercions. However, the use of type coercions to study features of type system is not at all new. Coercions have also been used in the context of subtyping, but without the notion of abstraction over coercions.

Subtyping have been popularized by object-oriented languages, even though inheritance is somehow better modeled by matching [START_REF] Bruce | Subtyping is not a good "match" for object-oriented languages[END_REF] or row polymorphism [START_REF] Rémy | [END_REF]]. In our view subtyping and polymorphism are both treated as coercions. Moreover, row polymorphism is just polymorphism with a richer structure of types and matching is a hidden form of row polymorphism.

The heavy use of coercions in FC, the core language of GHC, was one of our initial motivations for studying coercions in a general setting. In FC, only toplevel coercion axioms coming from type families and newtypes are checked for consistency. Local coercion abstractions are not. This is safe because all coercion abstractions in FC freeze the evaluation. This simplifies the meta-theory but at some significant cost, since the evaluation must be delayed to never reduce in a potentially inconsistent context. Our inconsistent coercions largely coincide to-and was inspired by coercions in FC. In return what F cc offers in addition is the ability to choose between coherent and incoherent coercion abstractions so that coherent coercions could be expressed as such and thus not freeze the evaluation and still bring more static guarantees to the user. While F cc treats coercions in the general case, FC considers only a very specific case of equality constraints-with additional restrictions-so that e.g. coherence of toplevel coercions axioms can be checked automatically.

All language features without computational content are treated as coercions in F cc . However, we have kept weakening implicit. Explicit weakening would exercise our general approach to typing inclusions which we have only used in a restricted form. Interestingly, explicit weakening has already been used in combination with explicit substitution [START_REF] David | [END_REF]]. Moreover, a new form of reduction is introduced to break wedges creating a particular substitution with the information about the weakening occurring in the wedge: ( k λt u) → [0/u, k]t. k is a constructor to lift a term by k de Bruijn indices and [j/u, k] is the explicit substitution constructor: the j de Bruijn index is substituted by j u, indices smaller than j are not modified, and those greater than j are incremented by k -1.

Coercions have also been used to eliminate function call overhead from datatype constructors in [START_REF] Vanderwaart | Typed compilation of recursive datatypes[END_REF]: the folding and unfolding of datatype definitions are done using erasable coercions, thus with no run-time effect or hidden cost while preserving the semantics.

Recursive coercions have also been used to provide coercion iterators over recursive structures [Crary(2000)]. However, the motivations are quite different and coercions are only used as a tool to compile bounded quantification away into intersection types.

RR n°8456

Extensions and variations

Higher-order types We introduced F cc as an extension of System F, thus restricting ourselves to second-order polymorphism. We have verified that our approach extends with higher-order types as in F ω . The changes are not significant because we already have kinds and a (very simple) form of reduction on types. However, the formalization in a proof assistant is significantly heavier. The internal language FC of GHC already has higher-order kinds, but not full β-reduction at the level of types.

Intersection types It should also be possible to add intersection types. (Our semantics already has them.). Following the work of Wells [START_REF] Wells | [END_REF]] on branching types, it would then be interesting to have intersection types as branching typings, which would be trees of typings where leaves are usual typings and nodes are chunks of typing environments.

Existential types We haven't included existential types in F cc and just used their standard CPS encoding into universal types. Adding primitive existential types would also be interesting but not immediate. This is not so surprising as the combination of existential types with strong reduction strategies is known to raise difficulties. The natural interpretation of existential types is the infinite union of the interpretations when the hidden part varies over all possible witnesses. The problem is already present and easier to explain with union types: the union of two semantic types is not obviously a type, and more precisely closed by expansion, as is the case for intersection. A term e in ♦ (R ∪ S) could a priori reduce to both e 1 in ∆R \ ∆S and e 2 in ∆S \ ∆R and not be in R ∪ S.

In the current setting, where the underlying language is the λ-calculus, it seems that e should be in R ∪ S by a complex standardization argument [Riba(2007)] in the absence of indices and may not be applicable in the case of indices-or force us to have a more involved definition of indexing compatible with standardization, namely so that semantic types are closed by a form of standardization. In any case, this argument cannot apply anymore if we add non-determinism such as random choice to the calculus. In this case, existential types must be reduced to a head normal form before unpacking, which is exactly what the CPS encoding of existential types enforces! A solution we have started to investigate is to use a reduction strategy equivalent to strong reduction but where only terms starting with a constructor are substituted. This relates to existing calculi with explicit substitutions and generalizes call-by-need calculi to strong reduction.

Alternate indexing Nevertheless, this raises the question of whether our definition of indexing is the right one. There is a lot of room for variations in the definition of indexing, since they are only a mean of abruptly stopping the reduction as long as other indexing of the same term will always allow to proceed further. However, in this process we have lost some interesting properties of the underlying λ-calculus such as confluence and standardization. Finding alternative-but probably more complex-indexing that would preserve those properties may still be worth exploring.

Side effects

We have studied a calculus of coercions in an ideal theoretical setting, but we do not foresee any problem in applying this to a real programming language with impure features such as side effects. We are not bound to a strong reduction strategy, but on the opposite have all the freedom to choose weak reduction strategies for term abstractions. In the presence of side-effects, we would have a form of value-restriction, allowing type and coercion abstractions only on value forms. We do not expect this to raise new problems with coercions-nor do we expect them to disappear! Other application of step-indexed semantics. Our semantics is a form of unary logical relation, and we expect no difficulties when considering binary relations. Step-indexing is also used in the presence of side effects to break the recursion in the store. Checking how indexed terms would work in the presence of a store remains to be done.

From implicit to explicit non-reducible coercions When coercions are left implicit they must be inferred-as well as coercion witnesses, which is obviously undecidable in the general case. (Typechecking in F η or in the most expressive variant of F <: are already undecidable.) In practice, the user should provide both of them explicitly-or at least provide sufficient information so that they can be inferred. Hence, a surface language would probably have explicit coercions-just for typing purposes-and coercions should be dropped after typechecking. Indeed, we do not describe how coercions and, in particular, wedges can be reduced. In this setting, our soundness result still applies-reduction will not introduce erroneous programs-but it does not imply subject reduction: it may happen that after reduction there is no way to redecorate the residual program with explicit coercions to make it well-typed. We believe that this is the price to pay for the generality offered by our approach.

Conclusion

Generalizing the notion of type coercions to typing coercions, we have proposed a type system where the distinction between the computation and the typing aspects of terms have been completely separated. It subsumes many features of existing type systems including subtyping, bounded quantification, instance bounded quantification, and subtyping constraints.

We have adapted the step-indexed semantics to work for calculi with strong reduction strategies and used it to prove the soundness of our language in a general setting. The step-indexed terms have been introduced just for our needs, but it would be worth exploring this approach further.

As for coercions, several research directions remain to be explored. Hopefully, new type system features such dependent types could still be added. A surface language with explicit coercions annotations is a prerequisite for decidable type checking. Variations on constraints allowing closed-world views as well as restrictions to recover subject reduction are worth further investigation.

Figure 1 :

 1 Figure 1: Well-formedness of kinds and propositions α, β Type variables x, y Term variables a, b ::= x | λx a | (a a) | a, a | π i a | ∂ a | a ♦ Terms κ ::= ⋆ | 1 | κ × κ | {α : κ | P} Kinds τ, σ ::= α | τ → τ | τ × τ | ∀(α : κ) τ Types | Π(α : κ) τ | µα τ | ⊥ | ⊤ | | τ, τ | π i τ P ::= ⊤ | P ∧ P | (Σ ⊢ τ ) ⊲ τ Propositions | ∃ κ | ∀(α :κ) P Θ ::= ∅ | Θ, P | Θ, P † Coinduction environments Γ ::= ∅ | Γ, (α : κ) | Γ, (x : τ ) Environments χ ::= ne | wf Recursive tokens

Figure 4 :

 4 Figure 4: Reduction relation

Figure 9 :

 9 Figure 9: Well-foundedness judgment relation

Figure 10 :

 10 Figure 10: Lower function

Figure 12 :

 12 Figure 12: Indexed calculus reduction relation

PFigure 13 :

 13 Figure 13: Lifting integer predicates to indexed terms

Figure 14 :

 14 Figure 14: Lifting of a binary predicate ⋆ on indices to terms

Figure 15 :

 15 Figure 15: Fill function

  (α : {α : ⋆ n | P}) where n is the size of α. Finally, we see constraint type schemes ∀α.C ⇒ τ as the coherent polymorphic type ∀(α | C) τ . A term judgment A ⊢ e : τ | C can then be seen as the F cc judgment (ᾱ | C), A ⊢ e : τ where α are free variables of A, C, and τ . Notice that the environment in the translation of judgments is always of the form (α | C), A composed of a single abstraction block (α | C) followed by term bindings A.

=

  λx (x ♦ a) iunpack a as x in b def = (a (∂ λx b))

RR n°8456

Scripts are available at http://gallium.inria.fr/~remy/coercions/.RR n°8456

WfKStarΓ ⋆ WfKOne Γ 1 WfKProd Γ κ 1 Γ κ 2 Γ κ 1 × κ 2 WfKRes Γ κ Γ, (α : κ) P Γ {α : κ | P} WfPTrue Γ ⊤ WfPAnd Γ P 1 Γ P 2 Γ P 1 ∧ P 2 WfPCoer Γ ⊢ Σ Γ, Σ ⊢ τ : ⋆ Γ ⊢ σ : ⋆ Γ (Σ ⊢ τ ) ⊲ σ WfPExi Γ κ Γ ∃ κ WfPFor Γ, (α : κ) P Γ ∀(α : κ) P WfGNil Γ ∅ WfGType Γ Γ ′ Γ, Γ ′ κ Γ Γ ′ , (α : κ) WfGTerm Γ Γ ′ Γ, Γ ′ ⊢ τ : ⋆ Γ Γ, (x : τ ) WfYNil Γ ∅ WfYConsA Γ Θ Γ P Γ Θ, P WfYConsB

∈ dom(Γ) and fv(τ ) ⊆ dom(Γ); and Γ, (α : κ) can only be formed when α / ∈ dom(Γ) and fv(κ) ⊆ dom(Γ). Similarly, Γ; Θ requires fv(Θ) ⊆ dom(Γ).3.3 Typing judgmentsTypes, kinds, and propositions are recursively defined and so are their typing judgments. We actually have the following judgments all recursively defined: Γ ⊢ a : τ term Γ; Θ ⊢ P prop. Γ ⊢ τ : κ type

TypeMuα → τ : wf Γ, (α :⋆) ⊢ τ : ⋆ Γ ⊢ µα τ : ⋆ TypePack Γ, (α : κ) P Γ ⊢ τ : κ Γ ⊢ P[α ← τ ] Γ ⊢ τ : {α : κ | P} TypeUnpack Γ ⊢ τ : {α : κ | P} Γ ⊢ τ : κFigure 6: Type judgment relation star. It is defined by the three rules:Γ ⊢ ∅ Γ ⊢ Γ ′ Γ, Γ ′ ⊢ κ Γ ⊢ Γ ′ , (α : κ) Γ ⊢ Γ ′ Γ, Γ ′ ⊢ τ : ⋆ Γ ⊢ Γ ′ , (x : τ )Kind and proposition well-formedness are recursively scanning their subexpressions for all occurrences of coercion propositions (Σ ⊢ τ ) ⊲ σ to ensure that Σ, τ , and σ are well-typed, as described by the following rule:

http://gallium.inria.fr/~remy/coercions/ RR n°8456

Σ here is a binder and has of course no connection with Σ used as typing environments.RR n°8456

RR n°8456RESEARCH CENTRE PARIS -ROCQUENCOURTDomaine de Voluceau, -Rocquencourt B.P. 105 -78153 Le Chesnay Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399