(Co-)Iteration for Higher-Order Nested Datatypes

Andreas Abel^{1}^{⋆} and Ralph Matthes^{2}^{⋆⋆}

1 Department of Computer Science, University of Munich

               abel@informatik.uni-muenchen.de

2 PPS,

CNRS, Université Paris VII (on leave from University of Munich)

              matthes@informatik.uni-muenchen.de

Abstract. The problem of defining iteration for higher-order nested datatypes of arbitrary (finite) rank is solved within the framework of System F^{ω} of higher-order parametric polymorphism. The proposed solution heavily relies on a general notion of monotonicity as opposed to a syntactic criterion on the shape of the type constructors such as positivity or even being polynomial. Its use is demonstrated for some rank-2 heterogeneous/nested datatypes such as powerlists and de Bruijn terms with explicit substitutions. An important feature is the availability of an iterative definition of the mapping operation (the functoriality) for those rank-1 type transformers (i. e., functions from types to types) arising as least fixed-points of monotone rank-2 type transformers. Strong normalization is shown by an embedding into F^{ω}. The results dualize to greatest fixed-points, hence to coinductive constructors with coiteration.

1 Introduction

What is iteration for nested datatypes? It is a disciplined use of least fixed-points of nested recursive definitions of types and type transformers which rewards the programmer with a guarantee of termination and can usually be expressed in terms of initial algebras. By “nested”, different concepts can be understood. The easiest would be to first introduce the type of natural numbers by the equation Nat = 1 + Nat and then the lists of naturals by NatList = 1 + Nat × NatList. Here, Nat is nested within NatList. In proof theory, the general principle behind it is called iterated inductive definitions [BFPS81]. More demanding would be nesting by help of parameters: Let List(A) = 1 + A × List(A) be the type of lists over A. Then FinTree = List(FinTree) is nested in the sense of an interleaving of the definitions of FinTree and List(FinTree). Certainly, this can be represented as a simultaneous definition. Nesting in the sense advocated in [BM98] is different:

⋆ The first author gratefully acknowledges the support by the PhD Programme Logic

in Computer Science (GKLI) of the Deutsche Forschungs-Gemeinschaft. ⋆⋆ The second author has benefitted from financial support by the EC ESPRIT project

21900 “TYPES” and the EU IST working group 29001 “TYPES”.

It is a definition of a family of types where the recursive calls may refer to other members of the family, e. g.,

Lam(A) = A + Lam(A) × Lam(A) + Lam(1 + A)

as a representation of untyped lambda terms [BP99b,AR99]. This is just a heterogeneous datatype because Lam itself is not used in determining to which family member recursive calls are made. True nesting, called non-linear [BP99a], occurs in the representation of untyped lambda terms with explicit substitution as follows:

L̂am(A) = A + L̂am(A) × L̂am(A) + L̂am(1 + A) + L̂am(L̂am(A)),

see example 4 below.

The aim of the present article is to shed more light on those nested inductive types in terms of type theory, i. e., by a formulation in System F^{ω} of higher-order parametric polymorphism [Gir72]. We propose a system GMIC of general monotone inductive and coinductive constructors of arbitrary kind of F^{ω} which hence also covers greatest fixed-points with associated coiteration. The system will be given in Curry-style, hence does not need any type information for the term rewrite rules. The well-known (at least, since [Wra89]) embeddings of inductive and coinductive datatypes into System F can be extended to an embedding of GMIC into F^{ω} by a syntactic analogue of Kan extensions (mentioned in the context of nested datatypes in [BP99a]).

A major effort has been made to ensure that there are iterative definitions of closed terms of types such as ∀A∀B. (A → B) → L̂am(A) → L̂am(B) which hence witness monotonicity or “functoriality” of L̂am and the other type transformers that are the solutions to these nested equations.

Unlike previous work of the second author [Mat01], we base our notion of monotonicity on a non-standard definition of inequality. In the case of F, G being definable functions from types to types, it is

F ≤ G := ∀A∀B. (A → B) → F A → GB,

kindly suggested by Peter Hancock during his visit in Munich in late 2000. The same notion has been used by Altenkirch/McBride [AM02] and Hinze [Hin02] to define map functions generically.

A rough categorical motivation can be given as follows: If F, G were functors, then ∀A. F A → GA would be the type of natural transformations α from F to G. Then, given some f : A → B, we would have Gf ∘ α_{A} and α_{B} ∘ F f as equal “morphisms” of type F A → GB. In our definition, we drop functoriality of F and G but directly require the “diagonal” in the associated naturality diagram from F A to GB (see Fig. 1).

The article is organized as follows: The present section is concluded by a short overview of System F^{ω} (with a more detailed account in appendix A and the Church version in appendix B). Section 2 contains the definition of GMIC

\xymatrix{A \ar[r]^{f} & B & F A \ar[r]^{F f} \ar@{.>}[ddr]^{ℓ_{f}} \ar[dd]^{α_{A}} & F B \ar[dd]^{α_{B}} \\ F \ar[r]^{α} & G \\ F \ar[r]^{ℓ}_{≤} & G & G A \ar[r]^{G f} & G B}

Fig. 1. “map”-like transformation ℓ : F ≤ G

and its specializations to (co-)inductive types and to (co-)inductive functors, including several examples for programming in GMIC. A short argument is given in 2.4 for subject reduction and confluence of GMIC. The syntactic analogue of Kan extensions forms Section 3. They are in close relation with our non-standard definition of ≤ for type constructors and are needed for our more advanced examples: substitution for de Bruijn terms and resolution of explicit substitutions (Section 3.1). Section 3.2 shows that, logically, the notion of monotonicity in [Mat01] is a special case of the one in GMIC. Section 4 gives the proof of strong normalization by an embedding into System F^{ω}. As mentioned before, appendices A and B give details of our version of System F^{ω}.

The Haskell implementation of (co)inductive types and functors plus most of the examples can be obtained from the Web site of the first author [Abe03].

Acknowledgements: Many thanks to Peter Hancock for his suggestion of the unusual notion of the definition of F ≤_{κ1} G, to Tarmo Uustalu for repeated advice on syntactic Kan extensions and the representation of substitution and to Thorsten Altenkirch for his valuable feedback on early versions of the present article. We also thank the anonymous referees who provided helpful comments.

1.1 System F^{ω}

Our development of higher-order datatypes takes place within a conservative extension of Curry-style System F^{ω} by finite sums and products and existential quantification. It contains three syntactic categories:

Kinds. We denote kinds by the letter κ. For the pure kind of rank n we introduce the special name κn.

\begin{aligned}κ & ::= & ∗ | κ → κ′ \\ κ0 & := & ∗ \\ κ(n + 1) & := & κn → κn \end{aligned}

Examples for pure kinds are κ0 = ∗, types, κ1 = ∗ → ∗, type transformers and κ2 = (∗ → ∗) → ∗ → ∗ transformers of type transformers. Note that each kind κ′ can be written as κ → ∗, where we write κ for κ_{1}, …, κ_{n}, set κ_{1}, …, κ_{n} → κ := κ_{1} → … → κ_{n} → κ and assume that → associates to the right. Also set |κ_{1}, …, κ_{n}| := n.

Constructors. Uppercase latin letters and the greek letters Φ and Ψ denote constructors, given by the following grammar.

\begin{aligned}A, B, F, G & ::= & X | λX.F | F G | ∀F^{κ}. A | ∃F^{κ}. A | A → B \\ & | & 0 | A + B | 1 | A × B \end{aligned}

We identify β-equivalent constructors. A constructor F has kind κ if there is a context Γ such that Γ ⊢ F : κ. The kinding rules for the constructors can be found in Appendix A. It also contains the typing rules for the terms and the reduction rules.

Preferably we will use letters A, B, C, D for constructors of rank 0 (types), F, G, H for constructors of rank 1 and Φ, Ψ for constructors of rank 2. If no kinds are given and cannot be guessed from the context, we assume A, B, C, D : ∗, F, G, H : κ1 and Φ, Ψ : κ2. We write F ∘ G for constructor composition λX.F (GX).

Objects (Curry terms). Lower case letters denote terms.

r, s, t ::= x | λx.t | r s | abort r | inl t | inr t | case (r, x. s, y. t)
| ⟨⟩ | ⟨t_{1}, t_{2}⟩ | r.0 | r.1 | pack t | open (r, x. s)

Most term constructors are standard; “pack” introduces and“open” eliminates existential quantification. As for kinds, there is a “vector notation” t for a list t_{1}, …, t_{n} of terms. The polymorphic identity λx.x : ∀A. A → A will be denoted by id. We write f ∘ g for function composition λx. f (g x). Application rs associates to the left, hence rs = (… (rs_{1}) … s_{n}) for s = s_{1}, …, s_{n}.

A term t has type A if Γ ⊢ t : A for some context Γ. The relation ⟶ denotes the usual one-step β-reduction which is confluent, type preserving and strongly normalizing. As mentioned above, the exact typing and reduction rules can be found in Appendix A.

Church terms. We consider Church-style terms (again, following the distinction between the styles à la Curry and à la Church proposed in [Bar92]) as a linear notation for typing derivations. For details see appendix B. Whenever we write a Church term, we mean the typing derivation of the corresponding Curry term.

In the following we will refer to the here defined system simply as “F^{ω}”.

2 Monotone Inductive and Coinductive Constructors

For constructors F and G of kind κ we define the types F ⊆_{κ} G and F ≤_{κ} G by recursion on κ as follows. Then general monotonicity mon_{κ} F for constructor F can be expressed in terms of ≤_{κ}, and will also be a type.

\begin{aligned}F ⊆_{∗} G & := & F → G \\ F ⊆_{κ→κ′} G & := & ∀X^{κ}. F X ⊆_{κ′} G X \\ F ≤_{∗} G & := & F → G \\ F ≤_{κ→κ′} G & := & ∀X^{κ}∀Y^{κ}. X ≤_{κ} Y → F X ≤_{κ′} G Y \\ mon_{κ} F & := & F ≤_{κ} F \end{aligned}

(When clear from the context, we will omit subscripts κ from ⊆, ≤ and mon. We assume that ⊆ and ≤ bind stronger than → or ×.) The proposed (co-)inductive constructors will not rely on some syntactic notion of positivity,^{1} but exclusively on the above defined notion of monotonicity, hence giving a logical flavour to the system. Monotonicity as an assertion/proposition is modelled as a type. The propositions-as-types paradigm of type theory, first introduced as the Curry-Howard-isomorphism [How80] for minimal propositional logic, has been an important guide in the development of the system.

Having monotonicity, we can enrich system F^{ω} with some constructor and term constants to obtain higher-order (co)inductive datatypes. Closed terms receiving a type of the form mon_{κ} F will be called monotonicity witnesses for F.

Inductive constructors.

Formation.  μ_{κ} : (κ → κ) → κ
Introduction. in_{κ} : ∀F^{κ→κ}. F (μ_{κ}F) ⊆ μ_{κ}F
Elimination.  It_{κ} : ∀F^{κ→κ}. mon F → ∀G^{κ}. F G ⊆ G → μ_{κ}F ≤ G
Reduction.  It_{κ→∗} m s f (in_{κ→∗} t) ⟶_{β} s (m (It_{κ→∗} m s) f t)

In the last line we require |f| = |κ|. As a first example, define

M_{κ}^{μ}(m)  := It_{κ} m in_{κ}
λm. M_{κ}^{μ}(m) : ∀F^{κ→κ}. mon F → mon (μ_{κ}F).

Hence, there is a completely uniform way of inferring monotonicity of μ_{κ}F from that of F. Moreover, the defined monotonicity witness has the desired reduction behavior: M_{κ}^{μ}(m) f (in_{κ}t) ⟶_{β} in_{κ} (m M_{κ}^{μ}(m) f t).

Coinductive constructors.

Formation.  ν_{κ} : (κ → κ) → κ
Introduction. Coit_{κ} : ∀F^{κ→κ}. mon F → ∀G^{κ}. G ⊆ F G → G ≤ ν_{κ}F
Elimination.  out_{κ} : ∀F^{κ→κ}. ν_{κ}F ⊆ F (ν_{κ}F)
Reduction.  out_{κ→∗} (Coit_{κ→∗} m s f t) ⟶_{β} m (Coit_{κ→∗} m s) f (s t)

1 Syntactic in the sense of being a criterion on the shape of the constructor. This criterion is used in most the articles on inductive types [Hag87,Men87,Lei90,Geu92].

Again, we require |f| = |κ|. Dually to the case of inductive constructors, define

M_{κ}^{ν}(m)  := Coit_{κ} m out_{κ}
λm. M_{κ}^{ν}(m) : ∀F^{κ→κ}. mon F → mon (ν_{κ}F).

Hence, also monotonicity of ν_{κ}F follows uniformly from monotonicity of F and has the desired computation rule: out_{κ} (M_{κ}^{ν}(m) f t) ⟶_{β} m M_{κ}^{ν}(m) f (out_{κ} t).

This completes the definition of the system GMIC of general monotone inductive and coinductive constructors. To give a feel for the meaning of these dense definitions we will specialize them to kinds κ0 and κ1 in the following sections.

2.1 (Co)Inductive Types

For kind κ0 we obtain monotone (co)inductive types as described in the second author’s thesis [Mat98]. These include all interleaved positive datatypes, especially all homogeneous datatypes like natural numbers, lists, trees etc. which are common in functional programming.

Inductive types (κ = ∗).

Formation.  μ_{∗} : (∗ → ∗) → ∗
Introduction. in_{∗} : ∀F^{∗→∗}. F (μ_{∗}F) → μ_{∗}F
Elimination.  It_{∗} : ∀F^{∗→∗}. mon F → ∀A^{∗}. (F A → A) → μ_{∗}F → A
Reduction.  It_{∗} m s (in_{∗} t) ⟶_{β} s (m (It_{∗} m s) t)

For the examples to follow, we will need some basic monotonicity witnesses:

pair : mon(λAλB.A × B) := λfλgλp. ⟨f (p.0), g (p.1)⟩
fork : mon(λA.A × A) := λf. pair ff
either : mon(λAλB.A + B) := λfλgλx. case (x, a. inl (f a), b. inr (g b))
maybe : mon(λA.1 + A) := either id

Example 1 (Binary trees). As a preparation for Example 6, we show how to encode a type BT of binary trees with constructors leaf : BT and span : BT → BT → BT and iterator ItBT : ∀A.(1 + A × A → A) → BT → A.

BTF  : ∗ → ∗  := λA. 1 + A × A
BT  : ∗  := μ_{∗}BTF
leaf  : BT  := in_{∗}(inl ⟨⟩)
span  : BT → BT → BT := λtλu. in_{∗}(inr ⟨t, u⟩)
mon BTF : ∗  = ∀A∀B. (A → B) → (1 + A × A) → (1 + B × B)
btf : mon BTF := maybe ∘ fork
ItBT  : ∀A.((1 + A × A) → A) → BT → A := It_{∗} btf

Coinductive types (κ = ∗).

Formation.  ν_{∗} : (∗ → ∗) → ∗
Introduction. Coit_{∗} : ∀F^{∗→∗}. mon F → ∀A^{∗}. (A → F A) → A → ν_{∗}F
Elimination.  out_{∗} : ∀F^{∗→∗}. ν_{∗}F → F (ν_{∗}F)
Reduction.  out_{∗} (Coit_{∗} m s t) ⟶_{β} m (Coit_{∗} m s) (s t)

As for inductive types, these are just the usual definitions, with arbitrary monotonicity witnesses (sometimes also called strength) instead of canonical ones for positive type transformers F. For the positive (covariant) case, their justification from the point of view of category theory has first been given in [Hag87], a very good presentation of the ideas is to be found in [Geu92].

2.2 (Co)Inductive Functors

If we specialize to kind κ1, we get heterogeneous (non-regular) and so-called (non-linear) nested datatypes. Prominent examples are powerlists [Hin00] and a monadic representation of de Bruijn λ-terms [AR99,BP99b].

Inductive functors (κ = κ1). Recall that κ1 = ∗ → ∗ and κ2 = κ1 → κ1.

Formation.  μ_{κ1} : κ2 → κ1
Introduction. in_{κ1} : ∀Φ^{κ2}∀A. Φ (μ_{κ1}Φ) A → μ_{κ1}Φ A
Elimination.  It_{κ1} : ∀Φ^{κ2}. mon Φ → ∀G^{κ1}. Φ G ⊆ G →
∀A∀B. (A → B) → μ_{κ1}Φ A → G B
Reduction.  It_{κ1} m s f (in_{κ1} t) ⟶_{β} s (m (It_{κ1} m s) f t)

The name “functors” is not by chance. Let Φ be monotone of kind κ2 and m : mon Φ a monotonicity witness. Then M_{κ1}^{μ}(m) is a monotonicity witness for μ_{κ1}Φ, i. e.,

M_{κ1}^{μ}(m) : mon(μ_{κ1}Φ) = ∀A∀B. (A → B) → (μ_{κ1}Φ)A → (μ_{κ1}Φ)B,

hence M_{κ1}^{μ}(m) is the “functorial action” or map function for μ_{κ1}Φ. Note, however, that the functor laws are beyond our intensional treatment. They could be proven in a theory with extensional equality.

Example 2 (Powerlists). A famous example for a heterogeneous datatype are lists of length 2^{n}, also called powerlists [BGJ00] or perfectly balanced, binary leaf trees [Hin00]. This datatype is present in our system as the least fixed point of the rank-2 constructor PListF = λF λA. A + F (A × A).

We obtain the type of powerlists with its data constructors and its monotonicity witness in a schematic way.

PList : ∗ → ∗  := μ_{κ1} PListF
plistf : mon PListF  := λsλf. either f (s (fork f))
plist : mon PList  := M_{κ1}^{μ}(plistf)
zero : ∀A. A → PList A  := λa. in_{κ1}(inl a)
succ : ∀A. PList(A × A) → PList A := λl. in_{κ1}(inr l)

A reversal algorithm for powerlists is simply derived from a different monotonicity witness for PListF.

swap : mon(λA.A × A) := λfλp. ⟨f (p.1), f (p.0)⟩
plistfrev : mon PListF  := λsλf. either f (s (swap f))
rev′ : mon PList  := M_{κ1}^{μ}(plistfrev)
rev : ∀A. PList A → PList A := rev′ id

Note that the freedom in using monotonicity witnesses demonstrated by the previous definition goes beyond the capabilities of Functorial ML [JBM98]. Although that system uses constants witnessing monotonicity to describe iteration, the behavior of those witnesses is fixed by the generic programming approach and consequently only yields the behavior of fork in the case of λA.A × A.

Example 3 (de Bruijn terms). Bird & Paterson [BP99b] and Altenkirch & Reus [AR99] have shown that nameless untyped λ-terms can be represented by a heterogeneous datatype. In our system this type is obtained as the least fixed point of the monotone rank-2 constructor LamF.

LamF : κ2  := λF λA. A + (F A × F A + F (1 + A))
lamf : mon LamF := λsλf. either f (either (fork (s f)) (s (maybe f)))

Now we can define the datatype Lam A of de Bruijn terms with free variables in A, plus its constructors var, app and abs. Furthermore, we give an auxiliary function weak which lifts each variable in a term to provide space for a fresh variable.

Lam : κ1  := μ_{κ1} LamF
lam : mon Lam  := M_{κ1}^{μ}(lamf)
var : ∀A. A → Lam A  := λa. in_{κ1}(inl a)
app : ∀A. Lam A → Lam A → Lam A := λt_{1}λt_{2}. in_{κ1}(inr (inl ⟨t_{1}, t_{2}⟩))
abs : ∀A. Lam(1 + A) → Lam A  := λr. in_{κ1}(inr (inr r))
weak : ∀A. Lam A → Lam(1 + A)  := lam (λa. inr a)

Example 4 (de Bruijn terms with explicit substitutions). We consider an extension of the untyped λ-calculus by explicit substitutions t{σ} where σ provides a term t_{i} for each of the n free variables x_{i} of t. We can view t{σ} as a term which has the same structure as t but with variables whose names are taken from the set {t_{1}, …, t_{n}}. This means that the variable names are itself λ-terms. Hence, for the data constructor êxs which makes an explicit substitution a term, the type L̂am(L̂am A) → L̂am A is justified. In this case we have to deal with a truly nested datatype.

L̂amF : κ2  := λF λA. LamF F A + F (F A)
l̂amf : mon L̂amF := λsλf. either (lamf s f) (s (s f))

The nesting of the type transformers F in L̂am is reflected by the nesting of the transformations s in the respective monotonicity witness. The datatype L̂am with its constructors is now obtained mechanically.

L̂am : κ1  := μ_{κ1} L̂amF
l̂am : mon L̂am  := M_{κ1}^{μ}(l̂amf)
v̂ar : ∀A. A → L̂am A  := λa. in_{κ1}(inl (inl a))
âpp : ∀A. L̂am A → L̂am A → L̂am A := λt_{1}λt_{2}. in_{κ1}(inl (inr (inl ⟨t_{1}, t_{2}⟩)))
âbs : ∀A. L̂am(1 + A) → L̂am A  := λr. in_{κ1}(inl (inr (inr r)))
êxs : ∀A. L̂am(L̂am A) → L̂am(A) := λe. in_{κ1}(inr e)

Example 5 (Host). Bird and Paterson [BP99a, Example 3.3] introduce the type transformer Host as an instructive example of true nesting. In GMIC this datatype can be represented as follows.

HostF : κ2  := λF λA. 1 + A × F (A × F A)
hostf : mon HostF := λsλf. maybe (pair f (s (pair f (s f))))
Host : κ1  := μ_{κ1} HostF
host : mon Host := M_{κ1}^{μ}(hostf)

The mapping function host has the following reduction behavior.

host f ∘ in_{κ1} ⟶_{β} in_{κ1} ∘ hostf host f
⟶^{+} in_{κ1} ∘ maybe (pair f (host (pair f (host f))))

Note that the reduct corresponds to the right-hand side of the defining recursive equation of host in the original work [BP99a]. However, their solution was only considered to exist in the semantical model of functor categories. Our system GMIC gives a direct operational justification—host is just an instance of the iterator It_{κ1}. Contrast this with Bird and Paterson’s higher-order iterator hfold, which is too weak to implement mapping functions like this one.

To overcome the shortcomings of hfold, Bird and Paterson introduce generalized folds (gfold), which allow them to define desired operations on nested datatypes like Host; we achieve the same with our notion of iteration and Kan extensions (see Sect. 3.1 below). Existence of gfold relies on the existence of mapping functions like host, whose termination is not thoroughly addressed in their work, but justified by our results.

Coinductive functors (κ = κ1).

Formation.  ν_{κ1} : κ2 → κ1
Introduction. Coit_{κ1} : ∀Φ^{κ2}. mon Φ → ∀G^{κ1}. G ⊆ Φ G →
∀A∀B. (A → B) → G A → ν_{κ1}Φ B
Elimination.  out_{κ1} : ∀Φ^{κ2}∀A. ν_{κ1}Φ A → Φ (ν_{κ1}Φ) A
Reduction.  out_{κ1} (Coit_{κ1} m s f t) ⟶_{β} m (Coit_{κ1} m s) f (s t)

Similar to the inductive case, functoriality of ν_{κ1}Φ is witnessed by the uniform construction M_{κ1}^{ν}(m) for m any monotonicity witness for Φ.

Example 6 (Functions over binary trees). Thorsten Altenkirch [Alt01] shows how to encode functions over regular inductive types by elements of nested coinductive types of rank 2. In the following we present his example of functions over unlabelled binary trees (λA. BT → A) as functor (TFun) in our system.

TFunF : κ2  := λF λA. A × F (F A)
tfunf : mon TFunF := λsλf. pair f (s (s f))

The coinductive type TFun is now obtained as the greatest fixed point of TFunF. We can derive its two destructors head and tail from the general destructor out for coinductive constructors.

TFun : κ1  := ν_{κ1}TFunF
head : ∀A. TFunA → A  := λb. (out_{κ1}b).0
tail : ∀A. TFunA → TFun(TFunA) := λb. (out_{κ1}b).1

Every function g : BT → A can be transformed via the function lamBT into an infinite object lamBT g : TFunA. We implement lamBT by coiteration.

lamBT′ : (λA. BT → A) ≤ TFun
lamBT′ := Coit_{κ1} tfunf (λf. ⟨f leaf, λlλr. f (span l r)⟩)
lamBT : ∀A. (BT → A) → TFunA
lamBT := lamBT′ id

Conversely, an object b : TFunA can be applied to a binary tree t : BT to yield an element appBT t b : A. The application function appBT can be encoded by iteration on the tree t.

appBT : BT → ∀A. TFunA → A
appBT := ItBT(λtλb. case (t, . head b, p. (p.1 (p.0 (tail b))))

2.3 Beyond Rank 2

To the knowledge of the authors, inductive datatypes having type transformers as arguments are rarely considered. An example would be

λA.μ_{κ1→κ1→∗}(λΦ^{κ1→κ1→∗}λF λG. F (F A) + (ΦF (G × G) + Φ(F × G)(G × G)))

with F × G := λA.F A × GA. It has been studied in [Oka99] for the efficient representation of square matrices. Squareness is ensured by types but without the use of dependent types, by which one would just express that there is an n such that the matrix has n rows and n columns. The argument to μ_{κ1→κ1→∗} clearly has a monotonicity witness.

As a toy example, we mention μ_{κ1→∗}Ψ with Ψ := λF^{κ1→∗}λG^{κ1}.G(F (G∘G)). mon Ψ is inhabited by λsλt.t(s(t ∘ t)).

2.4 Subject Reduction and Confluence

The extensions to system F^{ω} we made to incorporate (co)inductive constructors are orthogonal to the existing constructions like function space, products, sums etc. The new reduction rules do not interfere with any of the old ones and there are no critical pairs. Hence, confluence of GMIC immediately follows from standard results. To show subject reduction for GMIC, we only have to make sure that the new reduction rules preserve typing.

Proposition 1 ((Co)iteration is type-preserving). Let κ = κ → ∗ be an arbitrary kind and F : κ → κ, G : κ and X_{i}, Y_{i} : κ_{i} (for 1 ≤ i ≤ |κ|) be constructors. Furthermore let f_{i} : X_{i} ≤_{κ_{i}} Y_{i} be terms for 1 ≤ i ≤ |κ| and m : mon F.

1. Provided terms s : F G ⊆ G and t : F (μ_{κ}F)X, the following typing derivations are correct.

\begin{aligned}It_{κ}F m G s X Y f (in_{κ}F X t) & : & G Y \\ ⟶_{β}^{Church} s Y (m (μ_{κ}F) G (It_{κ}F m G s) X Y f t) & : & G Y \end{aligned}

2. Provided terms s : G ⊆ F G and t : GX we have the following typings.

out_{κ}F Y (Coit_{κ}F m G s X Y f t) : F (ν_{κ}F)Y
⟶_{β}^{Church} m G (ν_{κ}F) (Coit_{κ}F m G s) X Y f (s X t) : F (ν_{κ}F)Y

Proof. By trivial type-checking. Note that the notation is slightly sloppy: instead of X Y f, it should be X_{1}Y_{1}f_{1} … X_{|κ|}Y_{|κ|}f_{|κ|}.

Subject reduction would follow trivially for a corresponding formulation of the whole term rewrite system à la Church (where ⟶_{β}^{Church} above would give the reduction rules pertaining to iteration and coiteration), but consequently by standard techniques also for our Curry-style presentation of GMIC. The desired property of strong normalization requires more work; in the following we prepare for an embedding into system F^{ω}.

3 Kan Extensions

In this section we define Kan extensions for constructors of arbitrary rank, show their most fundamental properties and demonstrate their use in programming with iterators. Finally, we use them to establish logical equivalence between the notion of monotonicity in [Mat01] and rank-2 monotonicity mon_{κ2} Φ proposed in this article.

Kan extensions along the identity. Let G : κ → ∗ and Y_{i} : κ_{i} (0 ≤ i < |κ|) be constructors. Then the right Kan extension of G Y along the identity is a type defined by recursion on the length of Y as follows:

Ran G (·)  := G
Ran G (Y^{κ}, Y ) := ∀Z^{κ}. Y ≤_{κ} Z → Ran (GZ) (Y )

Similarily, the left Kan extension of G Y along the identity is the following type:

Lan G (·)  := G
Lan G (Y^{κ}, Y ) := ∃X^{κ}. X ≤_{κ} Y × Lan (GX) (Y )

These definitions are a syntactic rendering of the Kan extensions in category theory [Lan98, chapter 10] which become especially simple due to the presence of universal and existential types. We will not discuss any of their categorytheoretic properties. At this point, let us only note how Kan extensions relate to our notion “≤_{κ}”.

Proposition 2. Let F, G : κ → ∗. The following types are logically equivalent:^{2}

1. F ≤ G,

2. ∀X^{κ}. F X → Ran G (X), and

3. ∀Y^{κ}. Lan F (Y ) → G Y .

Proof. By induction on κ. Part 1. ⟺ 2. is done by rearranging quantifiers and arguments, Part 2. ⟺ 3. by currying and uncurrying.

Rank-1 right Kan extension along a functor H. For programming with iterators (see next section), we need the more general right Kan extension along H for some type transformer H. We define for constructors G, H of pure kind κ1 the type

Ran_{H} G (A) := ∀B. (A → HB) → GB

For the special case of the identity functor H = λA.A we obtain the right Kan extension defined above. We will write Ran_{H} G for λA. Ran_{H} G (A) and Ran G for λA. Ran G (A). The left Kan extension could be modified similarly, but for our purposes the right Kan extension is sufficient.

3.1 Programming with Kan extensions

In this section we demonstrate how right Kan extensions provide a general tool to program with rank-2 inductive datatypes. It is known [BP99a,Hin00] that a function f : μ_{κ1}Φ ∘ H ⊆ G for G, H : κ1 cannot be defined by iteration directly if H ≠ λA.A. The solution to this difficulty proposed in the cited articles is generalized iteration (also called “generalized fold”). Another solution (but related to the first one as a method for the justification of generalized iteration [BP99a, section 6.2]), is to define a more general auxiliary function g of type μ_{κ1}Φ ≤ Ran_{H} G, from which we get f by the trivial specialization f := λr. g id r id. We will demonstrate this technique by continuing our examples from Section 2.

2 A and B are called logically equivalent if there are closed terms in system F^{ω} of types A → B and B → A. It is thus equivalence in second-order propositional logic.

Example 7 (Summing up a powerlist). Assume a type Nat of natural numbers with addition “+”, written infix. A function sum which adds up all entries in a powerlist of naturals has type PList Nat → Nat. This is an instance of the problem described above where G = H = λA.Nat. The right Kan extension of G along H simplifies to λA. (A → Nat) → Nat, hence we define the following auxiliary function.

sum′ : PList ≤ (λA. (A → Nat) → Nat)
sum′ := It_{κ1} plistf stepSum
stepSum : PListF(λA. (A → Nat) → Nat) ⊆ (λA. (A → Nat) → Nat)
stepSum := λtλf. case (t, a. f a, l. l (λp. f (p.0) + f (p.1)))

Following our general recipe, the summation function is obtained as sum := λl. sum′ id l id.

Example 8 (Substitution for de Bruijn terms). De Bruijn terms constitute a Kleisli triple (Lam, var, subst) with unit var : ∀A. A → Lam A and bind operation

subst : ∀A. Lam A → ∀B. (A → Lam B) → Lam B.

The reader will note that the type of subst can also be written as ∀A. Lam A → Ran_{Lam} Lam (A). This suggests that substitution can be defined by iteration (proven by Altenkirch/Reus [AR99]).

subst′ : Lam ≤ Ran_{Lam} Lam
subst′ := It_{κ1} lamf stepSub
stepSub : LamF (Ran_{Lam} Lam) ⊆ Ran_{Lam} Lam
stepSub := λtλσ. case (t, a. σ a, t′. case (t′,
p. app (p.0 σ) (p.1 σ),

r. abs (r λx. case (x, u. var (inl u), a. weak (σ a)))))

The substitution function is obtained by specialization: subst := subst′ id.

From the “Kleisli triple” formulation of Lam we get the “monad” formulation (Lam, var, join) mechanically, since join : ∀A. Lam(Lam A) → Lam A can be obtained from subst as join := λt. subst t id.

Example 9 (Resolving explicit substitutions). The set of de Bruijn terms Lam can be embedded into the set of de Bruijn terms L̂am with explicit substitution. The embedding function emb : ∀A. Lam A → L̂am A can be defined by iteration in a straightforward manner. The other direction is handled by a function eval : ∀A. L̂am A → Lam A which has to resolve the explicit substitutions.

eval′ : L̂am ≤ Lam
eval′ := It_{κ1} l̂amf stepEv
stepEv : L̂amF Lam ⊆ Lam
stepEv := λt. case (t, t′. in_{κ1} t′, e. join e)

Note how join is used to carry out the substitutions. The evaluation function is just eval := eval′ id.

3.2 Comparison with Special Monotonicity [Mat01]

In [Mat01], the second author has introduced another notion of monotone inductive and coinductive constructors with μ_{κ} and ν_{κ} exclusively for κ ∈ {∗, ∗ → ∗}. The associated notions of monotonicity are for constructors of kind κ1 and κ2. Certainly, for κ1, there is only the definition we use in the present article. However, the notion for κ2 has been the following:

\underline{mon} Φ := (∀F. mon F → mon ΦF) × (∀G∀H.G ⊆ H → (mon G → ΦG ⊆ ΦH) × (mon H → ΦG ⊆ ΦH))

This “special” notion of monotonicity has been designed so that it is as close as possible to what one expects from category theory, but departing from it as much as needed so that, by help of Kan extensions, inhabitation of \underline{mon} Φ → mon(μ_{κ1}Φ) could be shown. Moreover, many closure properties of monotonicity could be established, going far beyond algebraic datatypes such as the ones in our present examples. Unfortunately, that notion does not seem to extend to other kinds of rank 2, not to speak of arbitrary ranks.

Here, we show that, from a logical point of view, there is no difference between special monotonicity \underline{mon} Φ and general monotonicity mon Φ, i. e., both types are logically equivalent. With respect to the rewrite rules, there are differences which cannot be addressed here for lack of space.

In this subsection, F, G, H always have kind κ1 and Φ has kind κ2. The direction from general monotonicity to special monotonicity does not require Kan extensions and can be programmed as follows:

c00  : ∀Φ. mon Φ → ∀F. mon F → mon ΦF
c00  := λmλn. m n
monSubLeq : ∀G∀H. mon G → G ⊆ H → G ≤ H
monSubLeq := λmλgλfλx. g (m f x)
subMonLeq : ∀G∀H. G ⊆ H → mon H → G ≤ H
subMonLeq := λgλmλfλx. m f (g x)
c10  : ∀Φ. mon Φ → ∀G∀H. G ⊆ H → mon G → ΦG ⊆ ΦH
c10  := λmλℓλnλt. m (monSubLeq n ℓ) id t
c11  : ∀Φ. mon Φ → ∀G∀H. G ⊆ H → mon H → ΦG ⊆ ΦH
c11  := λmλℓλnλt. m (subMonLeq ℓ n) id t
gmsm  : ∀Φ. mon Φ → \underline{mon} Φ
gmsm  := λm. ⟨c00 m, λℓ. ⟨c10 m ℓ, c11 m ℓ⟩⟩

We come to the interesting direction from special monotonicity to general monotonicity: Under the assumptions \underline{mon} Φ, G ≤ H and A → B, we have to show ΦGA → ΦHB. This is done via two intermediate types: We show ΦGA → Φ(Ran H)A → Φ(Ran H)B → ΦHB. The first step is an instance of ΦG ⊆ Φ(Ran H) which follows from \underline{mon} Φ, G ⊆ Ran H and mon(Ran H).

monRan : ∀H. mon(Ran H)
monRan := λfλkλg. k (g ∘ f)
leqRan : ∀G∀H. G ≤ H → G ⊆ Ran H (as an instance of proposition 2)
leqRan := λsλxλf. sfx
t1  : ∀Φ. \underline{mon} Φ → ∀G∀H. G ≤ H → ΦG ⊆ Φ(Ran H)
t1  := λmλs. (m.1 (leqRan s)).1 monRan

The second step is just monotonicity of Φ(Ran H), following from \underline{mon} Φ and mon(Ran H).

t2 : ∀Φ. \underline{mon} Φ → ∀H. mon(Φ(Ran H))
t2 := λm. (m.0) monRan

The third step comes from Φ(Ran H) ⊆ ΦH which in turn uses \underline{mon} Φ, Ran H ⊆ H and, once again, mon(Ran H).

subRan : ∀H. Ran H ⊆ H
subRan := λk. k id
t3  : ∀Φ. \underline{mon} Φ → ∀H. Φ(Ran H) ⊆ ΦH
t3  := λm. (m.1 subRan).0 monRan
smgm : ∀Φ. \underline{mon} Φ → mon Φ
smgm := λmλsλfλx. t3 m (t2 m f (t1 m s x))

Apparently, the crucial idea is the formation of the monotone (even non-strictly positive) constructor Ran H from an arbitrary type transformer H.

4 Embedding into System F^{ω}

The purpose of this section is a perspicuous proof of strong normalization of GMIC. In fact, we show that the new constructor and term constants can already be defined in System F^{ω} so that typing is preserved, and that for the defined terms, one has in F^{ω} that

It_{κ→∗} m s f (in_{κ→∗} t)  ⟶^{+} s (m (It_{κ→∗} m s) f t)
out_{κ→∗} (Coit_{κ→∗} m s f t) ⟶^{+} m (Coit_{κ→∗} m s) f (s t).

Therefore, if there is no typable term in F^{ω} with an infinite reduction sequence, there is neither a typable term in GMIC allowing an infinite sequence of reduction steps. In other words, strong normalization is inherited from that of F^{ω} which in turn is a well-known fact [Gir72].^{3}

3 In that original work, only weak normalization has been proven but an extension to strong normalization is standard technology since [Tai75].

Let κ = κ → ∗, set n := |κ|, and define for |f| = n

μ_{κ} := λF^{κ→κ}λY^{κ}. mon F → ∀G^{κ}. (F G ⊆ G) → (Ran G (Y ))
It_{κ} := λmλsλfλr. rmsf
in_{κ} := λtλmλsλf. s (m(It_{κ}ms)ft)
ν_{κ} := λF^{κ→κ}λY^{κ}. mon F × ∃G^{κ}. (G ⊆ F G) × (Lan G (Y ))
Coit_{κ} := λmλsλfλt. ⟨m, pack⟨s, pack⟨f_{1}, … pack⟨f_{n}, t⟩ …⟩⟩⟩
out_{κ} := λr. open (r.1, p_{0}. open (p_{0}.1, p_{1}…. open (p_{n−1}.1, p_{n}. v) …))
with v := r.0(Coit_{κ}(r.0)(p_{0}.0))(p_{1}.0) … (p_{n}.0)(p_{0}.0 (p_{n}.1))

Compared with the classical encoding of (co-)inductive datatypes [Wra89,Geu92], the new ingredients are the relativization to monotone F and the use the Kan extensions. Welltypedness and the purported reduction behaviour are a matter of trivial calculation.

By the reasoning above, this yields the following theorem. (We now use “⟶” to denote the one-step reduction relation of the full system GMIC.)

Theorem 1 (Strong Normalization). Whenever Γ ⊢ r : A in GMIC, then r admits no infinite reduction sequence r ⟶ r_{1} ⟶ r_{2} ⟶ … ⊓ ⊔

5 Conclusions and Further Work

The System GMIC presented in this article is an idealized programming language with support for arbitrarily nested datatypes of arbitrary kind (i. e., higher order type transformers). The key ingredient is a notion of monotonicity which is wider than any notion of positivity and goes far beyond polynomial or algebraic higherorder functors. We have shown that typical examples can be treated easily.

We would hope for many more examples that exploit the capabilities of GMIC—examples that use

– nesting in the second sense of our introduction, i. e., simultaneous inductive and coinductive constructors, combined with heterogeneity,

– non-strict positivity, i. e., arguments that occur an even time to the left of an arrow →,

– monotonicity of μ_{κ1}Φ for the formation of new datatypes such as μ_{∗}(μ_{κ1}Φ),

– μ_{κ} and ν_{κ} for rank rk(κ) > 1.

References

[Abe03] Andreas Abel. Haskell examples for iteration and coiteration on higher-order datatypes. Haskell code accompanying this article, available on the author’s homepage, 2003.

[Alt01] Thorsten Altenkirch. Representations of first order function types as terminal coalgebras. In Samson Abramsky, editor, Fifth International Conference on Typed Lambda Calculi and Applications, volume 2044 of Lecture Notes in Computer Science, pages 8–21. Springer, 2001.

[AM02] Thorsten Altenkirch and Conor McBride. Generic programming within dependently typed programming. To appear in the proceedings of WCGP’02, 2002.

[AR99] Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, 13th International Workshop, CSL ’99, Proceedings, volume 1683 of Lecture Notes in Computer Science, pages 453–468. Springer, 1999.

[Bar92] Henk P. Barendregt. Lambda calculi with types. In Samson Abramsky, Dov M. Gabbay, and Tom S. E. Maibaum, editors, Background: Computational Structures, volume 2 of Handbook of Logic in Computer Science, pages 117–309. 1992.

[BFPS81] Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, volume 897 of Lecture Notes in Mathematics. Springer Verlag, 1981.

[BGJ00] Richard Bird, Jeremy Gibbons, and Geraint Jones. Program optimisation, naturally. In Millenial Perspectives in Computer Science, Palgrave, 2000.

[BM98] Richard Bird and Lambert Meertens. Nested datatypes. In Johan Jeuring, editor, Mathematics of Program Construction, MPC’98, Proceedings, volume 1422 of Lecture Notes in Computer Science, pages 52–67. Springer Verlag, 1998.

[BP99a] Richard Bird and Ross Paterson. Generalised folds for nested datatypes. Formal Aspects of Computing, 11(2):200–222, 1999.

[BP99b] Richard S. Bird and Ross Paterson. De Bruijn notation as a nested datatype. Journal of Functional Programming, 9(1):77–91, 1999.

[Geu92] Herman Geuvers. Inductive and coinductive types with iteration and recursion. In Bengt Nordström, Kent Pettersson, and Gordon Plotkin, editors, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden, June 1992, pages 193–217, 1992. Only published

via ftp://ftp.cs.chalmers.se/pub/cs-reports/baastad.92/proc.dvi.Z.

[Gir72] Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État, Université de Paris VII, 1972.

[Hag87] Tatsuya Hagino. A typed lambda calculus with categorical type constructors. In D. H. Pitt, A. Poigné, and D. E. Rydeheard, editors, Category Theory and Computer Science, volume 283 of Lecture Notes in Computer Science, pages 140–157. Springer Verlag, 1987.

[Hin00] Ralf Hinze. Efficient generalized folds. In Johan Jeuring, editor, Proceedings of the Second Workshop on Generic Programming, WGP 2000, Ponte de Lima, Portugal, July 2000.

[Hin02] Ralf Hinze. Polytypic values possess polykinded types. Science of Computer Programming, MPC Special Issue, 43:129–159, 2002.

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

[JBM98] C. Barry Jay, Gianna Bellè, and Eugenio Moggi. Functorial ML. Journal of Functional Programming, 8(6):573–619, 1998.

[Lan98] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer Verlag, second edition, 1998.

[Lei90] Daniel Leivant. Contracting proofs to programs. In Piergiorgio Odifreddi, editor, Logic and Computer Science, volume 31 of APIC Studies in Data Processing, pages 279–327. Academic Press, 1990.

[Mat98] Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. PhD thesis, Ludwig-Maximilians-University, May 1998.

[Mat01] Ralph Matthes. Monotone inductive and coinductive constructors of rank 2. In Laurent Fribourg, editor, Proceedings of CSL 2001, volume 2142 of Lecture Notes in Computer Science, pages 600–614. Springer Verlag, 2001.

[Men87] Nax P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, N.Y., pages 30–36. IEEE Computer Society Press, 1987.

[Oka99] Chris Okasaki. From fast exponentiation to square matrices: An adventure in types. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, September 27-29, 1999, volume 34 of SIGPLAN Notices, pages 28–35. ACM, 1999.

[Tai75] William W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor, Logic Colloquium Boston 1971/72, volume 453 of Lecture Notes in Mathematics, pages 240–251. Springer Verlag, 1975.

[Wra89] G. C. Wraith. A note on categorical datatypes. In D. H. Pitt, A. Poigné, and D. E. Rydeheard, editors, Category Theory and Computer Science, volume 389 of Lecture Notes in Computer Science, pages 118–127. Springer Verlag, 1989.

A System F^{ω}

In the following we present Curry-style System F^{ω} enriched with binary sums and products, empty and unit type and existential quantification over constructors. Although we choose a human-friendly notation of variables, we actually mean the nameless version à la de Bruijn which identifies α-equivalent terms. (Captureavoiding) Substitution of an expression e for a variable x in expression f is denoted by f[x := e].

Kinds and rank.

κ  ::= ∗ | κ → κ′
rk(∗)  := 0
rk(κ → κ′) := max(rk(κ) + 1, rk(κ′))

Constructors. (Denoted by uppercase letters)

\begin{aligned}A, B, F, G & ::= & X | λX.F | F G | ∀F^{κ}. A | ∃F^{κ}. A | A → B \\ & | & 0 | A + B | 1 | A × B \end{aligned}

Equivalence on constructors. Equivalence F = F′ for constructors F and F′ is given as the compatible closure of the following axiom.

(λX.F) G =_{β} F [X := G]

We identify constructors up to equivalence, which is a decidable relation due to normalization and confluence of simply-typed λ-calculus (where our constructors are the terms and our kinds are the types of that calculus).

Objects (Terms). (Denoted by lowercase letters)

r, s, t ::= x | λx.t | r s | abort r | inl t | inr t | case (r, x. s, y. t)
| ⟨⟩ | ⟨t_{1}, t_{2}⟩ | r.0 | r.1 | pack t | open (r, x. s)

Contexts. Variables in a context Γ are assumed to be distinct.

Γ ::= · | Γ, X^{κ} | Γ, x:A

Judgments. (Simultaneously defined)

Γ cxt  Γ is a wellformed context
Γ ⊢ F : κ F is a wellformed constructor of kind κ in context Γ
Γ ⊢ t : A t is a wellformed term of type A in context Γ

Wellformed contexts. Γ cxt

· cxt  {Γ cxt \atop Γ, X^{κ} cxt}  {Γ ⊢ A : ∗ \atop Γ, x:A cxt}

Wellkinded constructors. Γ ⊢ F : κ

{X^{κ} ∈ Γ  Γ cxt \atop Γ ⊢ X : κ}  {Γ, X^{κ} ⊢ F : κ′ \atop Γ ⊢ λX.F : κ → κ′}  {Γ ⊢ F : κ → κ′  Γ ⊢ G : κ \atop Γ ⊢ F G : κ′}

{Γ, X^{κ} ⊢ A : ∗ \atop Γ ⊢ ∀X^{κ}. A : ∗}  {Γ, X^{κ} ⊢ A : ∗ \atop Γ ⊢ ∃X^{κ}. A : ∗}  {Γ ⊢ A : ∗  Γ ⊢ B : ∗ \atop Γ ⊢ A → B : ∗}

{Γ cxt \atop Γ ⊢ 0 : ∗}  {Γ ⊢ A : ∗  Γ ⊢ B : ∗ \atop Γ ⊢ A + B : ∗}  {Γ cxt \atop Γ ⊢ 1 : ∗}  {Γ ⊢ A : ∗  Γ ⊢ B : ∗ \atop Γ ⊢ A × B : ∗}

Welltyped terms. Γ ⊢ t : A

{(x:A) ∈ Γ  Γ cxt \atop Γ ⊢ x : A}  {Γ, x:A ⊢ t : B \atop Γ ⊢ λx.t : A → B}  {Γ ⊢ r : A → B  Γ ⊢ s : A \atop Γ ⊢ r s : B}

{Γ, X^{κ} ⊢ t : A \atop Γ ⊢ t : ∀X^{κ}.A}  {Γ ⊢ t : ∀X^{κ}.A  Γ ⊢ F : κ \atop Γ ⊢ t : A[X := F]}

{Γ ⊢ t : A[X := F]  Γ ⊢ F : κ \atop Γ ⊢ pack t : ∃X^{κ}.A}  {Γ ⊢ r : ∃X^{κ}.A  Γ, X^{κ}, x:A ⊢ s : C \atop Γ ⊢ open (r, x. s) : C}

{Γ cxt \atop Γ ⊢ ⟨⟩ : 1}  {Γ ⊢ t : A  Γ ⊢ B : ∗ \atop Γ ⊢ inl t : A + B}  {Γ ⊢ t : B  Γ ⊢ A : ∗ \atop Γ ⊢ inr t : A + B}

{Γ ⊢ r : A + B  Γ, x:A ⊢ s : C  Γ, y:B ⊢ t : C \atop Γ ⊢ case (r, x. s, y. t) : C}  {Γ ⊢ r : 0  Γ ⊢ C : ∗ \atop Γ ⊢ abort r : C}

{Γ ⊢ s : A  Γ ⊢ t : B \atop Γ ⊢ ⟨s, t⟩ : A × B}  {Γ ⊢ r : A_{0} × A_{1} i ∈ \{0, 1\} \atop Γ ⊢ r.i : A_{i}}

Reduction. The one-step reduction relation t ⟶ t′ between terms t and t′ is defined as the closure of the following axioms under all term constructors.

(λx.t) s  ⟶_{β} t[x := s]
case (inl r, x. s, y. t) ⟶_{β} s[x := r]
case (inr r, x. s, y. t) ⟶_{β} t[y := r]
⟨t_{0}, t_{1}⟩.i ⟶_{β} t_{i} if i ∈ {0, 1}
open (pack t, x. s) ⟶_{β} s[x := t]

We denote the transitive closure of ⟶ by ⟶^{+} and the reflexive-transitive closure by ⟶^{∗}.

The defined system is a conservative extension of System F^{ω}. Reduction is type-preserving, confluent and strongly normalizing.

B Notation for Typing Derivations

As is usual, typing derivations for F^{ω} will be communicated in a short-hand form, namely by the raw terms of a Church-style variant for which, given a context, typing and type-checking is a trivial matter. Here, we introduce those raw terms simultaneously with their typing rules.

The rules for x, rs, ⟨⟩, ⟨s, t⟩ and r.i are the same as for F^{ω}. The others are:

{Γ, x:A ⊢ t : B \atop Γ ⊢ λx^{A}.t : A → B}  {Γ ⊢ r : 0  Γ ⊢ C : ∗ \atop Γ ⊢ abort_{C} r : C}

{Γ, X^{κ} ⊢ t : A \atop Γ ⊢ ΛX^{κ}t : ∀X^{κ}.A}  {Γ ⊢ t : ∀X^{κ}.A  Γ ⊢ F : κ \atop Γ ⊢ tF : A[X := F]}

{Γ ⊢ F : κ  Γ ⊢ t : A[X := F] \atop Γ ⊢ pack_{∃X^{κ}.A}(F, t) : ∃X^{κ}.A}  {Γ ⊢ r : ∃X^{κ}.A  Γ, X^{κ}, x:A ⊢ s : C \atop Γ ⊢ open (r, X^{κ}.x^{A}. s) : C}

{Γ ⊢ t : A  Γ ⊢ B : ∗ \atop Γ ⊢ inl_{B} t : A + B}  {Γ ⊢ t : B  Γ ⊢ A : ∗ \atop Γ ⊢ inr_{A} t : A + B}

{Γ ⊢ r : A + B  Γ, x:A ⊢ s : C  Γ, y:B ⊢ t : C \atop Γ ⊢ case (r, x^{A}. s, y^{B}. t) : C}