A Dependently Typed Calculus with Polymorphic
Subtyping
Mingqi Xue, Bruno C. d. S. Oliveira
The University of Hong Kong

Abstract
A polymorphic subtyping relation, which relates more general types to more
specific ones, is at the core of many modern functional languages. As those languages start moving towards dependently typed programming a natural questionis how can polymorphic subtyping be adapted to such settings.
This paper presents the dependent implicitly polymorphic calculus (λ∀I ): asimple dependently typed calculus with polymorphic subtyping. The subtyping relation in λ∀I generalizes the well-known polymorphic subtyping relation
by Odersky and Läufer (1996). Because λ∀I is dependently typed, integrating
subtyping in the calculus is non-trivial. To overcome many of the issues arisingfrom integrating subtyping with dependent types, the calculus employs unified
subtyping, which is a technique that unifies typing and subtyping into a single relation. Moreover, λ∀I employs explicit casts instead of a conversion rule, allowing
unrestricted recursion to be naturally supported. We prove various non-trivial
results, including type soundness and transitivity of unified subtyping. λ∀I andall corresponding proofs are mechanized in the Coq theorem prover.
Keywords: Type Systems, Dependent Types, Subtyping, Polymorphism

1. Introduction
A polymorphic subtyping relation, which relates more general types to more
specific ones, is at the core of many modern functional languages. Polymorphic subtyping enables a form of (implicit) parametric polymorphism, wheretype arguments to polymorphic functions are automatically instantiated and theprogrammer does not specify them. Traditionally, variants of polymorphic subtyping (in the form of a more-general-than relation) have been used in functional
languages based on the Hindley-Milner (Hindley, 1969; Milner, 1978; Damas andMilner, 1982) type system, which supports full type-inference without any type
annotations. However, the Hindley-Milner type system only supports rank-1(or first-order) polymorphism, where all universal quantifiers only occur at the
top-level of a type. Modern functional programming languages, such as Haskell,
go beyond Hindley-Milner and support higher-ranked polymorphism (Odersky
and Läufer, 1996; Peyton Jones et al., 2007) with a more expressive polymorphic
Preprint submitted to Elsevier

April 27, 2021

subtyping relation. With higher-ranked polymorphism there is no restriction on
where universal quantifiers can occur.
Odersky and Läufer (1996) proposed a simple declarative specification forpolymorphic subtyping, which supports higher-ranked polymorphism. Since
then several algorithms have been proposed that implement variants of this specification. Most notably, the algorithm proposed by Peyton Jones et al. (2007)
forms the basis for the implementation of type inference in the GHC compiler.
Dunfield and Krishnaswami (2013) (DK) provide an elegant formalization ofanother sound and complete algorithm, which has also inspired implementations of type-inference in some polymorphic programming languages, such as
PureScript (Freeman, 2017) or DDC (Disciple Development Team, 2017). Morerecently Zhao et al. (2019) have mechanized DK’s type system in a theorem
prover.
In recent years dependent types (Coquand and Huet, 1988; Augustsson, 1998;
Altenkirch et al., 2010; Sjöberg et al., 2012; Stump et al., 2008; Weirich et al.,2013; Casinghino et al., 2014; Sjöberg and Weirich, 2015) have become a hot
topic in programming language research. Several newer functional programming
languages, most notably Agda (Norell, 2007) and Idris (Brady, 2013), are now
dependently typed. Moreover a number of existing functional languages, such as
Haskell, have started to move towards dependently typed programming (Weirich
et al., 2017). Dependent types naturally lead to a unification between types andterms, which enables both additional expressiveness and economy of concepts.
The key enabler for unifying terms and types in dependently typed calculi is the
adoption of a style similar to Pure Type Systems (PTSs) (Barendregt, 1991).
In PTSs there is only a single level of syntax for terms, i.e. the types (or kinds)
are expressed using the same syntax as the terms. This is in contrast with more
traditional calculi, where distinct pieces of syntax (terms, types and kinds) are
separated.
Unified syntax, typical of dependently typed languages, poses some challenges for language design and implementation. A first challenge arises fromthe interaction between recursion and dependent types. Essentially recursion
breaks strong normalization, which many common properties in dependently
typed calculi depend upon. One of the most typical properties among them isthe decidability of type checking, which simply cannot be guaranteed if some
type-level computations are non-terminating. However, this area has been actively investigated in the last few years, and a general approach (Stump et al.,2008; Sjöberg et al., 2012; Kimmell et al., 2012; Sjöberg and Weirich, 2015; Yanget al., 2016) based on explicit casts for type-level computations, has emerged
as an interesting solution for integrating general recursion in dependently typed
calculi. By avoiding the implicit type-level computation entirely, whether programs strongly normalize or not no longer matters for the decidability of typechecking. Current proposals for dependently typed versions of Haskell (Weirich
et al., 2017), for instance, adopt explicit casts for type-level computation.
The second challenge, for calculi that employ subtyping, is that smoothly
integrating dependent types and subtyping is difficult. Subtyping is a substantial difference to traditional PTSs, which do not have this feature. The issue2with subtyping is well summarized by Aspinall and Compagnoni (1996): “Onething that makes the study of these systems difficult is that with dependent types,
the typing and subtyping relations become intimately tangled, which means that
tested techniques of examining subtyping in isolation no longer apply”. Recent
work on unified subtyping (Yang and Oliveira, 2017) provides a simple techniqueto address this problem. Following the same spirit as Pure Type Systems, whichattempt to unify syntax and the typing and well-formedness relations, unified
subtyping suggests unifying typing and subtyping into a single relation. Thissolves the problem of dependencies in that now there is only a single relationthat depends only on itself. Furthermore, it results in a compact specificationcompared to a variant with multiple independent relations.
In this paper, we investigate how polymorphic subtyping can be adapted
into a dependently typed calculus with general recursion and explicit casts for
type-level computation. We employ unified subtyping to address the issues ofcombining dependent types with subtyping. The use of explicit casts for typelevel computation means that type equality is essentially syntactic (or rather
up-to α-equivalence). This avoids the use of a traditional conversion rule thatallows concluding β-equivalent types to be equal. In essence, the use of theconversion rule requires (implicit) type-level computation, since terms have to
be normalized using β-reduction to conclude whether or not they are equal.
Dependent type systems with a conversion rule have some major complications.
A well-known one is that type-inference for such systems requires higher-orderunification, which is known to be undecidable (Goldfarb, 1981). By employing asystem with α-equivalence only we stay closer to existing languages like Haskell,
where type equality (at least at the core language level) is also essentially only
up-to α-equivalence.
We present a calculus called λ∀I , and show three main results in this paper:transitivity of subtyping, type soundness, and completeness of λ∀I ’s polymorphic
subtyping with respect to Odersky and Läufer’s formulation. Transitivity is a
non-trivial result (like in most calculi combining dependent types and subtyping) and requires a proof based on sizes and a property that guarantees theuniqueness of kinds in our language. Type soundness is also non-trivial andwe need to take a different approach than that employed by existing work on
polymorphic subtyping (Odersky and Läufer, 1996; Peyton Jones et al., 2007),
where type-safety is shown by an elaboration to System F. In essence elaboration into a target language brings significant complications to the metatheory ina dependently typed setting. Thus, instead of elaboration, we use a direct operational semantics approach, which is partly inspired by the approach used in the
Implicit Calculus of Constructions (ICC) (Miquel, 2001; Barras and Bernardo,
2008), to prove type soundness. Similar to ICC, we adopt the restriction thatarguments for implicit function types are computationally irrelevant (i.e. theycannot be used in runtime computation). However, our unified subtyping setting is significantly different from ICC due to the presence of subtyping, whichbrings complications the ICC does not have. We also prove that any valid sub∀typing statement in the Odersky and Läufer relation is valid in λ∀I . Thus λI ’s
unified subtyping subsumes the polymorphic subtyping relation by Odersky and3

Läufer.
λ∀I and all the proofs reported in this paper are formalized in the Coq theorem prover (Coq development team). This paper does not address decidability
or soundness and completeness of λ∀I to an algorithmic formulation, which areoutside of the scope of this work. Nonetheless, these are important and challenging questions for practical implementations of λ∀I , which are left open for
future work.
In summary, the contributions of this paper are:
• The λ∀I calculus, which is a dependently typed calculus with explicit
casts, general recursion and implicit higher-ranked polymorphism.
• Type-soundness and transitivity of subtyping. We show that λ∀I istype-sound and unified subtyping is transitive.
• Subsumption of Odersky and Läufer’s polymorphic subtyping.
We show that λ∀I ’s unified subtyping can encode all valid polymorphic
subtyping statements of Odersky and Läufer’s relation.
• Mechanical formalization. All the results have been mechanically formalized in the Coq theorem prover. The formalization is available online
at: https://github.com/VinaLx/dependent-polymorphic-subtyping.
2. Overview
In this section, we introduce λ∀I by going through some interesting examples
to show the expressiveness and major features of the calculus. Then we discuss
the motivation, rationale of our design, and challenges. The formal system ofλ∀I will be discussed in Sections 3 and 4.
2.1. A Tour of λ∀I
The λ∀
calculusfeatures a form of implicit higher-ranked polymorphism withI
the power of dependent types. Thus the main feature of λ∀I is the ability to
implicitly infer universally quantified arguments.
A First Example of Implicit Polymorphism. Like most of functional languages,
λ∀I supports (implicit) parametric polymorphism. The first simple example isthe polymorphic identity function:
id : ∀(A:⋆). A → A
id = λ(x:A). x
answer : Natanswer = id 42 -- No type argument needed at the call of id
The polymorphic parameter A is annotated with its type, which is ⋆. The
type ⋆ is the type of types (also known as kind ). In λ∀I , the parameters oflambda abstractions are annotated with their types, and the A in the definitionrefers back to the polymorphic parameter. In the examples below, we drop the4parentheses around variables and their type annotations such as λx:A. x for
conciseness.
Similar to implicit polymorphism in other languages, the polymorphic parameters of the ∀ types are implicitly instantiated during applications. Thus, inthe call of the identity function (id 42), we do not need to specify the argumentused for instantiation. In contrast, in an explicitly polymorphic language (suchas System F) we would need to call id with an extra argument that specifies
the instantiation of A: id Nat 42.
Recursion and Dependent Types. λ∀I is dependently typed, and universal quantifications are not limited to work on arguments of type ⋆, but it allows arguments of other types. This is a key difference compared to much of thework on type-inference for higher-ranked polymorphism (Dunfield and Krishnaswami, 2013; Le Botlan and Rémy, 2003; Leijen, 2008; Vytiniotis et al., 2008;
Peyton Jones et al., 2007) which has been focusing on System F-like languages
where universal quantification can only have arguments of type ⋆. Furthermore,λ∀I supports general recursion at both the term and the type-level.
Using these features we can encode an indexed list, a map operation overit , and we illustrate how the implicit instantiation allows us to use the mapfunction conveniently. However, because λ∀I is just a core calculus there is nobuilt-in support yet for algebraic datatypes and pattern matching. We expectthat a source language would provide a more convenient way to define the mapfunction using pattern matching and other useful source-level constructs. To
model algebraic datatypes and pattern matching in λ∀I , we use an encoding
by Yang and Oliveira (Yang and Oliveira, 2019), which is based on the Scott
Encodings (Mogensen, 1992). The Scott Encoding encodes datatypes with different cases via Continuation-Passing-Style (CPS) function types. The return
branches of these function types correspond to each case of the datatypes. Case
analyses of terms are encoded via applications of the CPS functions. Since thedetails of the encoding are not relevant to this paper, here we omit the code formost definitions and show only their types.
In a dependently typed language a programmer could write the following
definition for our formulation of indexed lists:
data Nat = Zero | Succ Nat
data List (a : ⋆) (n : Nat) = Nil | Cons a (List a (Succ n))
In this definition, the index grows towards the tail of the list, which is admittedly not the most useful definition. The reason why we did not choose the morepractical example, where the index represents the length of the list, is that it
requires encodings of GADT-like datatypes (Cheney and Hinze, 2003; Xi et al.,2003). Such encodings are more complex than encodings of regular algebraic
datatypes as they require explicit equality proofs and more language-level supports for such proofs (Yang and Oliveira, 2019). Thus we use the simpler, but
still dependently typed example here. Here we encode List and its constructors
as conventional terms. We show the definition for List, and the types for theconstructors next (implementation omitted):5

List : ⋆ → Nat → ⋆List = µL:(⋆ → Nat → ⋆).λa:⋆.λn:Nat.Πr:⋆.
r-- Nil branch→ (a → L a (Succ n) → r) -- Cons branch→ r
Nil : ∀a:⋆.∀n:Nat. List a n
Cons : ∀a:⋆.∀n:Nat. a → List a (Succ n) → List a n
In subsequent examples we will just assume some Haskell-style syntactic sugarfor datatype definitions and constructors. Using the definitions above, we candefine a map function over List with the type:map : ∀a:⋆.∀b:⋆.∀n:Nat. a → b → List a n → List b n
An example of application of map is:
map Succ (Cons 1 (Cons 2 Nil))which increases every natural in the list by one. Note that since the typeparameters for map, Cons, and Nil are all implicit, they can be all omitted andthe arguments are instantiated implicitly. Thus the map function only requires
two explicit arguments, making it as convenient to use as in most functional
language implementations.
There are a few final points worth mentioning about the example. Firstly,
List is an example of a dependently typed function, since it is parameterized
by a natural value. Secondly, following the design of PITS (Yang and Oliveira,2019), fixpoint operators (µ) in λ∀I serve a dual purpose of defining recursive
types and recursive functions. Besides its usual use of defining term-level generalrecursive functions, fixpoint operators can be used to define recursive types, as
shown in the encoding of List above. Moreover, recursion is unrestricted andthere is no termination checking, much like approaches such as Dependently
Typed Haskell (Eisenberg, 2016), and unlike various other dependently typed
languages such as Agda (Norell, 2007) or Idris (Brady, 2013).
Implicit Higher-Kinded Types. The implicit capabilities also extend to the realmof higher-kinded types (Pierce, 2002). For example, we can define a record type
Functor, to mimic the type class (Wadler and Blott, 1989; Kaes, 1988) Functor
in Haskell:data Functor (F : ⋆ → ⋆) =MkF { fmap : ∀a:⋆.∀b:⋆. (a → b) → F a → F b }Here Functor is a record type with a single field. MkF is the data constructor,
and fmap is the field accessor (which encodes the type class method fmap). The
type of fmap is:
fmap : ∀F:⋆ → ⋆. Functor F → (∀a:⋆.∀b:⋆. (a → b) → F a → F b)
Importantly this example illustrates that universal variables can quantify overhigher-kinds (i.e. F : ⋆ → ⋆). We can define instances of functor in a standardway:
6

data Id a = MkId { runId : a }idFunctor : Functor Id
idFunctor =MkF { fmap = λf:(a → b).λx:(Id a). MkId (f (runId x)) }and then use fmap with three arguments:
fmap idFunctor Succ (MkId 0)
Note that, because our calculus has no mechanism like type classes we pass the“instance” explicitly. Nonetheless, three other arguments (the F, a, and b) are
implicitly instantiated.
Higher-Ranked Polymorphic Subtyping. In calculi such as the ICC (Miquel,2001), a form of implicit instantiation also exists. However, such calculi do not
employ subtyping, instead, they only apply instantiation to top-level universal
quantifiers. Our next example illustrates how subtyping enables instantiation
to be applied also in nested universal quantifiers, thus enabling more types tobe related.
When programming with continuations (Sussman and Steele, 1998) one of
the functions that are typically needed is call-with-current-continuation (callcc).
In a polymorphic language, there are several types that can be assigned tocallcc. One of these types is a rank-3 type, while another one is a rank-1 type.
Using polymorphic subtyping we can show that the rank-3 type is more generalthan the rank-1 type. Thus the following program type-checks:
callcc’ : ∀a:⋆. ((∀b:⋆. a → b) → a) → a
callcc : ∀a:⋆.∀b:⋆. ((a → b) → a) → a
callcc = callcc’
The type ∀b:⋆. a → b appears in a positive position of the whole signature,and it is a more general signature than a → b for an arbitrary choice of b.
Our language captures this subtyping relation so that we can assign callcc’ tocallcc (but not the other way around). In contrast, in approaches like the ICC,
the types of callcc and callcc’ are not compatible and the example above
would be rejected.
2.2. Key Features
We briefly discuss the major features of λ∀I itself and its formalization. Moreformal and technical discussions will be left to Sections 3 and 4.
Polymorphic Subtyping Relation. Figure 1 shows the syntax of types, monomorphic types (or monotypes), and the polymorphic subtyping relation in Dunfield
and Krishnaswami (2013) variation of Odersky and Läufer’s declarative typesystem (Odersky and Läufer, 1996). Although there are slight differences between the two versions of subtyping relations, since they essentially express thesame idea, we use DK’s and Odersky and Läufer’s polymorphic subtyping relation interchangeably in this article. Here the syntax includes ∀ types that7

TypesMonotypes

A, B
τ, σ

∶∶=
∶∶=

x ∣ N ∣ A → B ∣ ∀x. A
x ∣N∣τ →σΓ ⊢DK A ≤ B(Polymorphic Subtyping)

≤Var

≤→

x∈Γ

Γ ⊢DK B1 ≤ A1

≤IntΓ ⊢DK x ≤ xΓ ⊢DK N ≤ N

Γ ⊢DK A2 ≤ B2

Γ ⊢DK A1 → A2 ≤ B1 → B2

≤∀L

≤∀R

Γ ⊢DK τΓ ⊢DK [τ /x] A ≤ B

Γ ⊢DK ∀x. A ≤ B

Γ, x ⊢DK A ≤ B
Γ ⊢DK A ≤ ∀x. B

Figure 1: The Dunfield and Krishnaswami (2013) variation of the polymorphic subtyping
relation by Odersky and Läufer (1996).

represent polymorphic types (or polytypes), which are universally quantified
over type parameters. The definition of monotypes is standard and includes
all types without occurrences of universal quantifiers. Context Γ is a list of
type variables that are allowed to occur free in types A and B in the subtyping relation. The polymorphic subtyping relation captures a more-general-thanrelation between types. The key rules in their subtyping relation are rules ≤∀Land ≤∀R:• In rule ≤∀L, a polytype (∀x. A) is considered more-general than anothertype (B), when we can find an arbitrary monotype (τ ) so that the instantiation is more general than B. Importantly note that this relation does
not guess arbitrary (poly)types, but just monotypes. In other words, therelation is predicative (Martin-Löf, 1998). This restriction ensures thatthe relation is decidable.
• In rule ≤∀R a type (A) is considered more general than a polytype (∀x. B)
when it is still more general than the head of the polytype, with the typeparameter instantiated by an abstract variable x.
This subtyping relation sets a scene for our work, which generalizes thisrelation to a dependently typed setting.
Generalizing Polymorphic Subtyping. The parameters of universal types canonly be types in the polymorphic subtyping relation by Odersky and Läufer.
In λ∀I , we generalize the polymorphic parameters so that they can be values orother kinds of types as well. The first idea for a direct generalization is:

8

≤∀L′

≤∀R′

Γ⊢τ ∶AΓ ⊢ [τ /x] B ≤ CΓ, x ∶ B ⊢ A ≤ CΓ ⊢ ∀x ∶ A . B ≤ C

Γ ⊢ A ≤ ∀x ∶ B . C

The parameters for universal types can have any type (and not just ⋆). Hence,
instead of requiring the monotype τ to be a well-formed type in rule ≤∀L, in rule≤∀L′ it is required that τ is well-typed regarding the type of the parameter inthe universal quantifier. Similarly, for rule ≤∀R′ the context for the subtyping
rule should include typing information for the universally quantified variable.
However, this idea introduces the issue of potential mutual dependency between
subtyping and typing judgments, so further adjustments have to be made toformalize this idea, which is discussed later in this section, Sections 3.3 and 4.1.
Higher-Ranked Polymorphic Subtyping. As the callcc example in Section 2.1
shows, the subtyping rules based on polymorphic subtyping, combined withother subtyping rules, are able to handle the subtyping relations that occur at
not only top-level but also at a higher-ranked level. This feature distinguishes
our λ∀
I from the Implicit Calculus of Constructions (ICC) (Miquel, 2001) which
also discusses the implicit polymorphism of dependent type languages. The ICC
features these two related rules in their typing relation:instΓ ⊢ e ∶ ∀ x ∶ A. B

Γ ⊢ e1 ∶ A

gen

Γ, x ∶ A ⊢ e ∶ BΓ ⊢ e ∶ [e1 /x ] BΓ ⊢ ∀ x ∶ A. B ∶ kΓ ⊢ e ∶ ∀ x ∶ A. B

Without an explicit subtyping relation, the ICC is not always able to handle
subtyping at higher-ranked positions. The approach taken by the ICC is similar
to that of the Hindley-Milner type system (Hindley, 1969; Damas and Milner, 1982), which is also designed for dealing only with rank-1 polymorphism.
Hindley-Milner’s declarative system also has a GEN rule to convert expressions
to polymorphic types, and an INST rule to instantiate polymorphic parameters. Similar to rules GEN and INST shown above, both rules in HM work only
for polymorphic types at top-level positions. In Hindley-Milner the universal
quantifier can only quantify over types, whereas in the ICC it can quantify overterms of an arbitrary type (including types themselves). In generalizations ofhigher-ranked polymorphic type-inference (Dunfield and Krishnaswami, 2013;
Le Botlan and Rémy, 2003; Leijen, 2008; Vytiniotis et al., 2008; Peyton Joneset al., 2007), it has been shown that rules like ≤∀L and ≤∀R generalize rules likeGEN and INST. Since we aim at higher-ranked polymorphic generalization, we
follow a similar, more general, approach in λ∀I.
Unified Subtyping. The revised subtyping relation with ≤∀L′ and ≤∀R′ rules
suffers from an important complication compared to the Odersky and Läufer
formulation: there is now a notorious mutual dependency between typing and9subtyping. In Odersky and Läufer’s rules, the subtyping rules do not dependon typing. In particular the rule ≤∀L depends only on well-formedness (Γ ⊢ τ ).
In contrast, note that rule ≤∀L′ now mentions the typing relation in its premise(Γ ⊢ τ ∶ A). Moreover, as usual, the subsumption rule of the typing relation
depends on the subtyping relation as shown below.
t-sub

Γ⊢e∶A

Γ⊢A≤B

Γ⊢e∶B
This mutual dependency has been a significant problem when combining subtyping and dependent types (Aspinall and Compagnoni, 1996; Hutchins, 2010), andpresents itself on our way to the direct generalization of polymorphic subtyping.
To tackle this issue, we adopt a technique called the unified subtyping (Yangand Oliveira, 2017). Unified subtyping merges the typing relation and subtyping
relation into a single relation to avoid this mutual dependency:Γ ⊢ e1 ≤ e2 ∶ A
The interpretation of this judgment is: under context Γ, e1 is a subtype of e2
and they both are of type A. The judgments for subtyping and typing are both
special forms of unified subtyping:Γ⊢A≤B≜Γ⊢A≤B∶⋆

Γ⊢e∶A≜Γ⊢e≤e∶A

The technique simplifies the formalization of dependently typed calculi with
subtyping, and especially the proof of transitivity in the original work by Yang
and Oliveira (2017). After applying the technique, an ideal generalization of thepolymorphic subtyping would be:
≤∀L′′

≤∀R′′

Γ⊢τ ∶AΓ ⊢ [τ /x] B ≤ C ∶ ⋆Γ ⊢ ∀x ∶ A. B ≤ C ∶ ⋆Γ, x ∶ B ⊢ A ≤ C ∶ ⋆Γ ⊢ A ≤ ∀x ∶ B. C ∶ ⋆The basic idea of our own formalization essentially follows a similar design,
although the actual rules in λ∀I are slightly more sophisticated. The details will
be discussed in Section 3.3.
“Explicit” Implicit Instantiation. With polymorphic subtyping the instantiationof universally quantified type parameters is done implicitly instead of being
manually applied. In non-dependent type systems, implicit parameters are types(i.e. terms are not involved in implicit instantiation). For example:(λx. x) 42 Ð→ 42
Here λx. x has type ∀A. A → A, and instantiation implicitly discovers that A =Int. Notably, and in contrast with explicitly polymorphic languages like System
10F, implicit instantiation is not reflected anywhere at term level. The design that
we adopt still provides implicit instantiation, but it is more explicit regarding thebinding of implicit parameters. We adopt this design to ensure that polymorphic
variables are well-scoped in type annotations of terms. Thus we use anotherbinder, of the form Λ(x ∶ A).e, for terms. Nonetheless, instantiations are still
implicit as shown in the following example:(ΛA ∶ ⋆. λx ∶ A. x) 42 Ð→ 42
Here ΛA ∶ ⋆. λx ∶ A. x has type ∀A ∶ ⋆. A → A, and the polymorphic parameter
A is explicitly stated in the polymorphic term. However as the reduction shows,the instantiations are still implicit. We purposely omitted the explicit binders
for implicit parameters for all the examples in Section 2.1 for conciseness. Such
explicit binders can be recovered with a simple form of syntactic sugar:e ∶ ∀(x ∶ A). B ≜ Λx ∶ A. e ∶ ∀(x ∶ A). B
Computational Irrelevance. Implicit parameters in traditional languages withpolymorphic subtyping, the ICC (Miquel, 2001; Barras and Bernardo, 2008),
and λ∀
I are computationally irrelevant. In traditional (non-dependently) typed
languages, types cannot affect computation, thus computational irrelevance isquite natural and widely adopted. Furthermore, computational irrelevance canbenefit performance, since irrelevant arguments can simply be erased at runtime.
In dependently typed systems, however, there can be some programs where it
is useful to have computationally relevant implicit parameters. For example,
accessing the length of a length-indexed vector in constant time:
length : ∀n:Nat. Vector n → Nat
length = Λn:Nat.λv:(Vector n). n
Here the implicit parameter n is computationally relevant as it is used as thereturn value of the function which is likely to be executed at runtime. Languages
like Agda, Coq, and Idris support such programs. However, computationally
relevant implicit parameters are challenging for proofs of type soundness. Due tosuch challenges (see also the discussion in Section 3.2), the ICC has a restrictionthat parameters for implicit function types must be computationally irrelevant.
Since we adopt a similar technique for the type soundness proof, we also havea similar restriction and thus cannot encode programs such as the above.
Type-level Computation and Casts. λ∀I features the fixpoint operator that supports general recursion at both type and term level. In order to avoid diverging
computations at type checking, we do not provide the conversion rule (or congruence rule) like other dependently typed systems such as the Calculus ofConstructions (Coquand and Huet, 1988) to support implicit type-level reduc-11

tion.
CongΓ⊢e ∶AA =β BΓ⊢e ∶BThe presence of the conversion rule makes the decidability of type checking relyon the strong normalization of type-level computation (to determine whether
two types are β-equivalent). But the presence of general recursion denies thestrong normalization property of our language.
Instead of using a conversion rule, we adopt the call-by-name design of Pure
Iso-Type Systems (PITS) (Yang et al., 2016; Yang and Oliveira, 2019), andprovide cast⇓ and cast⇑ operators to explicitly trigger one-step type reductions
or expansions as shown in the typing rules below.
CastupΓ⊢e ∶BA Ð→ B

CastdnΓ⊢A∶kΓ⊢e ∶AΓ ⊢ cast⇑ [A] e ∶ A

A Ð→ BΓ⊢B ∶kΓ ⊢ cast⇓ e ∶ BNow, since reductions only perform one step per use of cast operators, whether
a term strongly normalizes or not no longer affects the decidability of typechecking. Note that there are some other cast designs in the literature (Stumpet al., 2008; Sjöberg et al., 2012; Kimmell et al., 2012; Sjöberg and Weirich,2015), we adopt the PITS design here for simplicity. We believe that other castdesigns could also be adopted instead, but leave this for future work.
3. The Dependent Implicitly Polymorphic Calculus
This section introduces the static and dynamic semantics of λ∀I : a dependently typed calculus with type casts and implicit polymorphism. The calculus
employs unified subtyping (Yang and Oliveira, 2017) and has a single relationthat generalizes both typing and subtyping. The calculus can be seen as a variant of the Calculus of Constructions (Coquand and Huet, 1988), but it uses a
simple form of casts (Yang et al., 2016; Yang and Oliveira, 2019) with cast⇑ andcast⇓ operators instead of the conversion rule and features unrestricted recursion with the fixpoint operator. We present the syntax, the unified subtyping
relation, and operational semantics for λ∀I.
3.1. Syntax
Figure 2 shows the syntax of λ∀I . The syntax is similar to the Calculus ofConstructions, featuring unified terms and types, and a kind hierarchy with ⋆and ◻. The kind ⋆ is the type (or kind) of other types like N and Π types, thekind ◻ is the type of ⋆, but ◻ itself has no type/kind. Due to the unified syntax, types and expressions (e, A and B) are used interchangeably, but we mostly
adopt the convention of using A and B for contexts where the expressions areused as types and e for contexts where the expressions represent terms. The
12

KindsExpressions

ke, A, BMono-Expressions

τ, σValuesv

Contexts
Syntactic Sugar

Γ
A→B

∶∶=
∶∶=
∣
∣
∶∶=
∣
∶∶=
∣
∶∶=
≜

⋆∣◻
x ∣ n ∣ k ∣ N ∣ e1 e2 ∣ λ x ∶ A. e ∣ Π x ∶ A. B
Λ x ∶ A. e ∣ ∀ x ∶ A. B ∣ µ x ∶ A. ecast⇑ [A] e ∣ cast⇓ e
x ∣ n ∣ k ∣ N ∣ τ1 τ2 ∣ λ x ∶ τ. σ ∣ Π x ∶ τ. σΛ x ∶ τ. σ ∣ µ x ∶ τ. σ ∣ cast⇑ [τ ] σ ∣ cast⇓ τk ∣ n ∣ N ∣ λ x ∶ A. e ∣ Π x ∶ A. B ∣ Λ x ∶ A. e
∀ x ∶ A. B ∣ cast⇑ [A] e∅ ∣ Γ, x ∶ A
Π x ∶ A. B
where x ∉ FV(B)Figure 2: Syntax of λ∀I.

syntax includes all the constructs of the calculus of constructions: variables (x ),kinds (k ), function applications (e1 e2 ), lambda expressions (λ x ∶ A. e), dependent function types (Π x ∶ A. B ) as well as integer types (N) and integers (n).
Moreover, there are several additional language constructs to support implicit
polymorphism, recursion, and explicit type-level computation via casts. These
constructs are discussed next.
Implicit Polymorphism. In λ∀I , universal types ∀ x ∶ A. B generalize implicit
polymorphic types (∀x. A) in conventional functional languages. The parameterx in ∀ x ∶ A. B ranges over all well-typed expressions besides well-formed types(i.e. x can have any type A instead of just kind ⋆). The idea of monomorphic
types (or monotypes) is also generalized. Mono-expressions τ exclude polymorphic types (∀ x ∶ A. B ) from the syntax, which follows a similar design in various
work about predicative higher-ranked polymorphism (Odersky and Läufer, 1996;
Dunfield and Krishnaswami, 2013; Peyton Jones et al., 2007). With dependent
types, only generalized universal types are excluded, but not any other related
expressions.
Notably, generalized “polymorphic types” are naturally dependent, and ∀types can be viewed as the implicit counterpart of Π types. So we also have
implicit lambda expressions (Λ x ∶ A. e), which is different from the “usual” λexpressions and explicit function types (Π types), for which arguments should
be explicitly passed. The arguments of implicit lambda (Λ) expressions are
deduced during type checking. This is a similar design to the Implicit Calculusof Constructions (ICC∗ ) (Barras and Bernardo, 2008), which employs similar
constructs for implicit dependent products.
Recursion and Explicit Type-level Computation. The λ∀I calculus adopts isotypes (Yang et al., 2016; Yang and Oliveira, 2019), featuring explicit type-levelcomputation with cast operators cast⇓ and cast⇑ . These operators respectively
perform one-step type reduction and expansion based on the operational semantics. The reduction in cast operators is deterministic, thus type annotations are13

only needed during type expansions (cast⇑ ). We add fixpoints (µ x ∶ A. e) to
support general recursion for both term-level and type-level. Iso-recursive types
are supported by cast⇑ and cast⇓ operators, which correspond to the fold andunfold operations when working on conventional iso-recursive types.
3.2. Operational Semantics
For the operational semantics we employ two different, but closely related
reduction relations. The first reduction relation is non-deterministic, and it isused at the type-level to allow type conversions induced by the cast operators.
The second reduction relation is deterministic and is employed to give the runtime semantics of expressions.
Non-deterministic Implicit Instantiations. Figure 3 presents the small-step operational semantics of λ∀I . It mostly follows the “Call-By-Name” (CBN) variantof Pure Iso-Type Systems (PITS) (Yang and Oliveira, 2019) corresponding to
the calculus of constructions. In such variant the arguments of the β-reduction(rule r-beta) and expressions in the rule r-cast-elim are not required to bevalues. Reductions can be performed inside cast⇓ terms (rules r-castdn andr-cast-inst). Note that here rule r-castdn reflects the term-level reduction ofcast⇓ terms themselves, the one-step type-level reductions triggered by the cast⇓operator are reflected in the typing rules. Following the CBN semantics of PITS,
cast⇑ terms are considered to be values to avoid nondeterministic reduction ofterms like cast⇓ (cast⇑ [A] e), where e is reducible (either performing reduction
on e, or the reduction via rule r-cast-elim could be the choice, should cast⇑terms be reducible). There is an alternative design following the “call-by-value”
variant of PITS, which we will discuss in Section 5.2. Also, the unfold operationof the fixpoint operator is supported by rule r-mu.
Due to the presence of instantiation of implicit parameters, the direct operational semantics is not deterministic, and potentially not type-preserving
because of rules r-inst and r-cast-inst. The indeterminacy is caused by theguess of τ , which can be an arbitrary mono-expression, since we do not haveaccess to any typing information in the dynamic semantics.
Deterministic Erased Reduction. We address the issue of determinacy of the
dynamic semantics with a design similar to ICC∗ (Barras and Bernardo, 2008),
employing type-erased expressions. The erased expressions essentially mirror
the syntax and semantics of normal expressions, except for the elimination oftype annotations in λ, Λ, µ, and cast⇑ expressions. Figure 4 shows the syntax ofthe erased expressions and the companion operational semantics. Restrictions
are imposed in the typing rules to forbid the implicit parameter occurring inruntime-relevant parts of the expression, i.e. the erased expressions (see Section
3.3). With such restriction, implicit parameters can be directly eliminated inrules er-elim and er-cast-inst. For a well-typed expression, the reduction of
its erasure is deterministic. Although the implicit parameter does not matter atruntime, the erasure function preserves the structure of the original syntax by
not eliminating the implicit binder altogether. This design has the advantage14e1 Ð→ e2(Operational Semantics)
r-app

e1 Ð→ e2r-betae1 e3 Ð→ e2 e3(λ x ∶ A. e1 ) e2 Ð→ [e2 /x ] e1

r-instr-mu(Λ x ∶ A. e1 ) e2 Ð→ ([τ /x ] e1 ) e2

µ x ∶ A. e Ð→ [µ x ∶ A. e/x ] er-castdn

e1 Ð→ e2r-cast-inst

cast⇓ e1 Ð→ cast⇓ e2cast⇓ (Λ x ∶ A. e) Ð→ cast⇓ ([τ /x ] e)r-cast-elim

cast⇓ (cast⇑ [B ] e) Ð→ e

Figure 3: Operational semantics of λ∀I.

that the correspondence between the original and the erased expression can beestablished more easily, when the reductions of erased expressions corresponddirectly to their erased counterpart. The proof of type safety of our system isbuilt around this idea of correspondence, which is discussed in Section 4.4.
3.3. Unified Subtyping
Figure 5 shows the (sub)typing rules of the system. We adopt a simplified
design based on unified subtyping (Yang and Oliveira, 2017). The subtyping
rules and typing rules are merged into a single judgment Γ ⊢ e1 ≤ e2 ∶ A.
Unified subtyping solves the challenging issue of mutual dependency between
typing and subtyping in a dependent type system. The interpretation of thisjudgment is “under context Γ, e1 is a subtype of e2 and they are both of type
A”. In this form of formalization, the typing judgment Γ ⊢ e ∶ A is a special
case of the unified subtyping judgment Γ ⊢ e ≤ e ∶ A, and the well-formednessof types Γ ⊢ A is expressed by Γ ⊢ A ∶ ⋆.
Subtyping Rules for Universal Quantifications. The subtyping rules for universal quantifications (rules s-forall-l and s-forall-r) follow the spirit of theOdersky and Läufer’s polymorphic subtyping (Odersky and Läufer, 1996; Dunfield and Krishnaswami, 2013), where the subtyping relation is interpreted asa “more-general-than” relation. A polymorphic type ∀ x ∶ A. B is more generalthan another type C when its well-typed instantiation is more general than C(rule s-forall-l). A polymorphic type ∀ x ∶ B . C is less general than a typeA, if C is less general than A when the argument with the polytype (x ∶ B) is
instantiated abstractly (rule s-forall-r).

15Erased Expressions

E, A, B

Erased Valuesev∣x ∣ = x

∶∶=
∣
∶∶=
∣

x ∣ n ∣ k ∣ N ∣ E1 E2 ∣ λ x . E ∣ Π x ∶ A. B
Λ x . E ∣ ∀ x ∶ A. B ∣ µ x . E ∣ cast⇑ E ∣ cast⇓ E
k ∣ n ∣ N ∣ λ x . E ∣ Π x ∶ A. B ∣ Λ x . E∀ x ∶ A. B ∣ cast⇑ E∣n∣ = n∣k ∣ = k∣e1 e2 ∣ = ∣e1 ∣ ∣e2 ∣∣N∣ = N∣µ x ∶ A. e∣ = µ x. ∣e∣∣λ x ∶ A. e∣ = λ x. ∣e∣∣Π x ∶ A. B ∣ = Π x ∶ ∣A∣. ∣B ∣∣Λ x ∶ A. e∣ = Λ x. ∣e∣∣cast⇑ [A] e∣ = cast⇑ ∣e∣∣∀ x ∶ A. B ∣ = ∀ x ∶ ∣A∣. ∣B ∣∣cast⇓ e∣ = cast⇓ ∣e∣

E1 Ô⇒ E2

(Erased Semantics)

er-appE1 Ô⇒ E2

er-beta

E1 E3 Ô⇒ E2 E3(λ x . E1 ) E2 Ô⇒ [E2 /x ] E1

er-elimer-mu(Λ x . E1 ) E2 Ô⇒ E1 E2µ x . E Ô⇒ [µ x . E/x ] E

er-castdn

E1 Ô⇒ E2

er-cast-inst

cast⇓ E1 Ô⇒ cast⇓ E2cast⇓ (Λ x . E) Ô⇒ cast⇓ E

er-cast-elim

cast⇓ (cast⇑ E) Ô⇒ E

Figure 4: Erased Expressions and Operational Semantics

16

⊢Γ

(Well-formed Context)
wf-cons⊢Γ

wf-nilx fresh in Γ

⊢∅

Γ⊢A∶k

⊢ Γ, x ∶ AΓ ⊢ e1 ≤ e2 ∶ A
s-var

⊢Γ

(Unified Subtyping)s-lit

x ∶A ∈ ΓΓ⊢x ≤x ∶A

⊢Γ

s-int

s-starΓ⊢N≤N∶⋆

Γ⊢⋆≤⋆∶◻

⊢ΓΓ⊢n ≤n ∶Nabs⊢ΓΓ ⊢ A ∶ k1
Γ, x ∶ A ⊢ B ∶ k2 Γ, x ∶ A ⊢ e1 ≤ e2 ∶ Bs-app

Γ ⊢ λ x ∶ A. e1 ≤ λ x ∶ A. e2 ∶ Π x ∶ A. B

Γ ⊢ e1 τ ≤ e2 τ ∶ [τ /x ] B

s-piΓ⊢τ ∶AΓ ⊢ e1 ≤ e2 ∶ Π x ∶ A. B

Γ ⊢ A2 ≤ A1 ∶ k1
Γ, x ∶ A1 ⊢ B1 ∶ k2
Γ, x ∶ A2 ⊢ B1 ≤ B2 ∶ k2s-muΓ⊢τ ∶kΓ ⊢ Π x ∶ A1 . B1 ≤ Π x ∶ A2 . B2 ∶ k2

Γ, x ∶ τ ⊢ σ ∶ τΓ ⊢ µ x ∶ τ. σ ≤ µ x ∶ τ. σ ∶ τs-bindΓ⊢A∶kΓ, x ∶ A ⊢ B ∶ ⋆ Γ, x ∶ A ⊢ e1 ≤ e2 ∶ B
x ∉ FV(∣e1 ∣) ∪ FV(∣e2 ∣)Γ ⊢ Λ x ∶ A. e1 ≤ Λ x ∶ A. e2 ∶ ∀ x ∶ A. B

s-castupΓ ⊢ A ∶ k A Ð→ B
Γ ⊢ e1 ≤ e2 ∶ BΓ ⊢ cast⇑ [A] e1 ≤ cast⇑ [A] e2 ∶ A

s-forall-ls-castdn

Γ ⊢ B ∶ k A Ð→ B
Γ ⊢ e1 ≤ e2 ∶ AΓ⊢A∶kΓ⊢τ ∶AΓ, x ∶ A ⊢ B ∶ ⋆Γ ⊢ [τ /x ] B ≤ C ∶ ⋆Γ ⊢ cast⇓ e1 ≤ cast⇓ e2 ∶ BΓ ⊢ ∀ x ∶ A. B ≤ C ∶ ⋆s-forall-rΓ⊢A∶⋆Γ⊢B ∶kΓ, x ∶ B ⊢ A ≤ C ∶ ⋆s-forallΓ⊢A∶kΓ ⊢ A ≤ ∀ x ∶ B. C ∶ ⋆Γ, x ∶ A ⊢ B ≤ C ∶ ⋆Γ ⊢ ∀ x ∶ A. B ≤ ∀ x ∶ A. C ∶ ⋆s-subΓ ⊢ e1 ≤ e2 ∶ A

Γ⊢A≤B ∶kΓ ⊢ e1 ≤ e2 ∶ B
Syntactic SugarsΓ⊢e ∶A≜Γ⊢e ≤e ∶AΓ⊢A≜Γ⊢A≤A∶⋆Γ⊢A≤B≜Γ⊢A≤B ∶⋆Figure 5: Unified Subtyping Rules of λ∀I.

17Notably, our formalization is not the direct generalization of Odersky and
Läufer’s polymorphic subtyping, as we mentioned in Section 2.2. As highlighted
in Figure 5: we add rule s-forall that axiomatizes the subtyping relation
between two universal types, and additional premises are added to rules sforall-l and s-forall-r besides the ones that appear in rules ≤∀L′′ and≤∀R′′ in Section 2.2. We discuss the motivations for these changes in moredetail in Section 4.1.
Mono-expression Restrictions. As in other predicative relations (such as theone by Odersky and Läufer), the type arguments for instantiation in rule sforall-l are required to be mono-expressions, which has cascading effects on
typing rules of other expressions. The arguments for applications are required
to be mono-expressions, and the whole fixpoint expression is required to be a
mono-expression. We shall discuss the rationale to impose these restrictions in
Section 4.
Kind Restriction for Universal Types. For the kinding of types, we mainly follow the design of the Calculus of Constructions (Coquand and Huet, 1988).
However, we specifically restrict the polymorphic type ∀ x ∶ A. B to only havekind ⋆, but not ◻. Without this restriction, types of kind ⋆ (such as N) areable to have “polymorphic kinds” like ∀ x ∶ N. ⋆ through rules s-forall-l, sforall-r, and s-sub, which significantly complicates the kinding reasoning in
the metatheory. Practically speaking, “polymorphic kinds” are not very common, so this restriction has little impact on the expressiveness of our language.
Since we expect the types of well-typed expressions to be well-kinded, therestriction propagates to the introduction rule of ∀ types (rule s-bind). In thisrule, B is required to only have kind ⋆ but not ◻. In contrast, for rule s-abs, thetype B at a similar position can have any kind. As a result, implicit polymorphic
functions at type level are never well-typed. For example, Λa ∶ ⋆. λb ∶ n. a is not
well-typed since it would have been a polymorphic function of type ∀a ∶ ⋆. a →⋆, which is not well-kinded due to the kinding restriction of universal types.
Moreover, type-level function applications that involve implicit abstractions (Λexpressions) are also never well-typed because of the restriction. So well-typed
non-deterministic implicit instantiation can never occur at the type-level.
Computational Irrelevance of Implicit Parameters. As mentioned in Section 2.2,
our language does not handle computationally relevant implicit parameters.
The direct operational semantics shown in Figure 3 chooses arbitrary monoexpressions to instantiate the implicit arguments, which potentially breaks typesafety. Thus, we adopt a restriction in rule s-bind that is similar to the Implicit
Calculus of Constructions (ICC) (Miquel, 2001). We only allow the implicit
parameters to occur in type annotations in the body of implicit abstraction, sothat the choices of implicit parameters are not relevant at runtime. The typesafety of the direct operational semantics is proved indirectly in Section 4.4 withthe help of the erasure of expressions.

18

Redundant Premises. All the premises boxed by dash lines are redundant ina way that the system without them is proved equivalent to the system withthem. These redundant premises are there to simplify the mechanized proofs ofcertain lemmas, but can be safely dropped in an actual implementation.
4. The Metatheory of λ∀IThis section presents the metatheory of λ∀I , and discusses several challenges
that arose during the design of the typing rules to ensure desired subtyping
and typing properties in our system. The three main results of the metatheory are: transitivity of unified subtyping, type-soundness and completeness withrespect to Odersky and Läufer’s polymorphic subtyping. Transitivity of subtyping is a general challenge for dependent type systems due to the mutual
dependency of typing and subtyping, and the Odersky and Läufer style subtyping brings new issues to the table. For type-soundness, the key challenge is thenon-deterministic and non-type-preserving nature of the reduction relation. To
address this issue, we employ a type soundness proof technique that makes useof the erased reduction relation shown in Figure 4.
4.1. Polymorphic Subtyping in a Dependently Typed Setting
The polymorphic subtyping relation by Odersky and Läufer features thefollowing two rules:
Γ ⊢DK τΓ, x ⊢DK A ≤ B

Γ ⊢DK [τ /x] A ≤ B

Γ ⊢DK ∀x. A ≤ B≤∀LΓ ⊢DK A ≤ ∀x. B≤∀RIn order for the well-formedness (Dunfield and Krishnaswami, 2013) property(If Γ ⊢DK A ≤ B, then Γ ⊢DK A and Γ ⊢DK B) to hold in Läufer and Odersky’s
system, these two rules rely on certain properties that do not hold in our dependently typed generalization. So we make several adjustments in our adaptation
to address these issues, which result in the difference between our current system
and a direct generalization mentioned in Section 2.2.
Reverse Substitution of Well-Formedness. Rule ≤∀L relies on the reverse substitution property, but this property does not hold in a dependently typed setting.
Thus we need an alternative design that still ensures well-formedness, but without relying on the reverse substitution property.
The reverse substitution property is: If Γ ⊢DK [B/x] A and Γ ⊢DK B, thenΓ, x ⊢DK A. That is if we have a type A with all occurrences of x substituted by
B and B is well-formed, we can conclude that A is well-formed under Γ, x. Ina dependently typed setting, a possible form of generalization of this property
would be: If Γ ⊢ [B /x ] A ∶ ⋆ and Γ ⊢ B ∶ C , then Γ, x ∶ C ⊢ A ∶ ⋆, which unfortunately does not hold. In a dependent type system, the values of expressions
also matter during type checking besides their types, a counter-example of the19

property is:F ∶ N → ⋆, a ∶ F 42 ⊢ (λy ∶ F 42 . N) a ∶ ⋆F ∶ N → ⋆, a ∶ F 42, x ∶ N ⊢ (λy ∶ F x . N) a ∶ ⋆We cannot “reverse substitute” the 42 in the type annotation to a variable ofthe same type: the application expression depends specifically on the value 42
in order for the type of argument a to match the type of the parameter. So
we add a premise Γ, x ∶ A ⊢ B ∶ ⋆ in rule s-forall-l to directly ensure thewell-formedness of types in the conclusion.
Strengthening of Contexts. Rule ≤∀R relies on a strengthening lemma: if Γ, x ⊢A and x does not occur in A, then Γ ⊢ A, which is trivial to prove in theirsystem. However the admissibility of its generalization: if Γ, x ∶ B ⊢ A ∶ ⋆ andx does not occur in A, then Γ ⊢ A ∶ ⋆, is much more complicated to reason
about. We can construct the following example:
F ∶ N → ⋆, A ∶ ⋆, a ∶ A ⊢ F ((Λ x ∶ A. λ y ∶ N. y) 42) ∶ ⋆The variable a does not appear in any expression, but plays a crucial role when
considering the subtyping statement Γ ⊢ ∀x ∶ A. N → N ≤ N → N, which arises
when type-checking the application (Λ x ∶ A. λ y ∶ N. y) 42. In this case, wecannot apply rule s-forall-l unless we find a well-typed instance for the polymorphic parameter. So the variable a in the context is needed even though it
does not occur anywhere in the final judgment. Note that, since our system
has a fixpoint operator, theoretically we could construct a diverging programµ x ∶ A. x to instantiate the implicit parameter, but this possibility leads toseveral other issues which we will discuss in Section 5.6. Furthermore, such an
approach would not work for calculi without fixpoints.
Due to these complications, we assume that strengthening does not hold in
our system for now. We add a premise Γ ⊢ A ∶ ⋆ to rule s-forall-r to workaround this issue, requiring A to be a well-kinded type without the help of the
fresh variable. A consequence of adding this premise is that we will encounter acircular proof while trying to prove Γ ⊢ ∀ x ∶ A. B ≤ ∀ x ∶ A. B ∶ ⋆, for arbitrary
A and B by first applying rule s-forall-r. We resolve this issue by adding
rule s-forall.
4.2. Typing Properties of λ∀IWith our rules properly set up, we can prove most of the basic properties
using techniques borrowed from the unifed subtyping (Yang and Oliveira, 2017)
approach. We introduce reflexivity, weakening, context narrowing, substitution
and type correctness in this section.
Theorem 1 (Reflexivity). If Γ ⊢ e1 ≤ e2 ∶ A, then Γ ⊢ e1 ∶ A and Γ ⊢ e2 ∶ A.
Usually, a subtyping relation is reflexive when any well-formed type is a subtype of itself. With unified subtyping, the well-formedness of types is expressed20

by subtyping relation as well, so the reflexivity looks more like the generalized
well-formedness mentioned in the previous section. Reflexivity breaks down into
two parts, left reflexivity and right reflexivity.
Lemma 2 (Left Reflexivity). If Γ ⊢ e1 ≤ e2 ∶ A, then Γ ⊢ e1 ∶ A.
Lemma 3 (Right Reflexivity). If Γ ⊢ e1 ≤ e2 ∶ A, then Γ ⊢ e2 ∶ A.
Both of the branches are proved by induction on the derivation of Γ ⊢ e1 ≤ e2 ∶ A.
Left reflexivity and right reflexivity when derivations end with rule s-forall-l
and rule s-forall-r respectively are directly solved by rule s-forall.
Theorem 4 (Weakening). If Γ1 , Γ3 ⊢ e1 ≤ e2 ∶ A and ⊢ Γ1 , Γ2 , Γ3 , then
Γ1 , Γ2 , Γ3 ⊢ e1 ≤ e2 ∶ A.
Weakening is proved by induction on the derivation of Γ1 , Γ3 ⊢ e1 ≤ e2 ∶ A. The
redundant premises discussed in Section 3.3 help to simplify the proof, by creating the induction hypotheses about the type annotation of various expressions.
Otherwise, we are not able to prove ⊢ Γ1 , Γ2 , Γ3 , x ∶ A with only ⊢ Γ1 , Γ3 , x ∶ Agiven and no help from induction hypotheses.
Theorem 5 (Context Narrowing). If Γ1 , x ∶ B , Γ2 ⊢ e1 ≤ e2 ∶ C and Γ1 ⊢A ≤ B ∶ k , then Γ1 , x ∶ A, Γ2 ⊢ e1 ≤ e2 ∶ C .
Lemma 6 (Well-formedness of Narrowing Context). If ⊢ Γ1 , x ∶ B , Γ2and Γ1 ⊢ A ≤ B ∶ k , then ⊢ Γ1 , x ∶ A, Γ2 .
Theorem 5 and Lemma 6 are proved by mutual induction on the derivations of
Γ1 , x ∶ B , Γ2 ⊢ e1 ≤ e2 ∶ C and ⊢ Γ1 , x ∶ B , Γ2 . Rule s-var is the only non-trivial
case to solve: it relies on weakening to conclude Γ1 , x ∶ A, Γ2 ⊢ A ≤ B ∶ k from
Γ1 ⊢ A ≤ B ∶ k , in order to derive Γ1 , x ∶ A, Γ2 ⊢ x ∶ B through rule s-sub.
Theorem 7 (Substitution). If Γ1 , x ∶ A, Γ2 ⊢ e1 ≤ e2 ∶ B and Γ1 ⊢ τ ∶ A, then
Γ1 , [τ /x ] Γ2 ⊢ [τ /x ] e1 ≤ [τ /x ] e2 ∶ [τ /x ] B .
Notably substitution has a mono-expression restriction on the substituted expression. This is due to the mono-expression restriction on the instantiation ofpolymorphic parameters in rule s-forall-l.
Take the following derivation as an example:
A ∶ ⋆, F ∶ A → ⋆, a ∶ A ⊢ [ a /x] F x ≤ F a ∶ ⋆A ∶ ⋆, F ∶ A → ⋆, a ∶ A ⊢ ∀x ∶ A. F x ≤ F a ∶ ⋆s-forall-l

Assuming that we have no mono-expression restrictions on substitution andrule s-app. If we substitute a with an arbitrary poly-expression, the derivation
stops working because rule s-forall-l requires a mono-expression instantiation
and rule s-app requires the argument of both sides to be syntactically the same.
21

Worth mentioning is that while substitution of poly-expressions breaks thesubtyping aspect of the language, a special case of the substitution theorem
that discusses the typing of one expression (If Γ1 , x ∶ A, Γ2 ⊢ e ∶ B and Γ1 ⊢e1 ∶ A, then Γ1 , [e1 /x ] Γ2 ⊢ [e1 /x ] e ∶ [e1 /x ] B ) does not hold for similar reasons.
Because, in dependently typed languages, substitutions are also involved in thetypes of expressions as well. Due to the presence of rule s-sub, we still haveto maintain the potential subtyping relation of the types of expressions after
substitution, for example:
A ∶ ⋆, F ∶ A → ⋆, a ∶ A, b ∶ ∀x ∶ A. F x ⊢ b ∶ ∀x ∶ A. F x
A ∶ ⋆, F ∶ A → ⋆, a ∶ A, b ∶ ∀x ∶ A. F x ⊢ b ∶ F a

s-sub

As a result, the substitution theorem only holds with the mono-expression restriction. This has a cascading effect on typing rules like rules s-app and smu whose expressions trigger substitutions during reduction. So the monoexpression restriction has to be added for those rules for the system to be typesafe.
Lemma 8 (Context Well-formedness of Substitution). If ⊢ Γ1 , x ∶ A, Γ2
and Γ1 ⊢ τ ∶ A, then ⊢ Γ1 , [τ /x ] Γ2 .
After understanding the mono-expression restriction on substitution, the actual
proof is not complicated: it proceeds by mutual induction with Lemma 8 on thederivations of Γ1 , x ∶ A, Γ2 ⊢ e1 ≤ e2 ∶ B and ⊢ Γ1 , x ∶ A, Γ2 . When the derivation ends with rules s-castup and s-castdn, the proof requires the reduction
relation to preserve after the substitution. This property should usually hold,but it puts an interesting constraint which we have to consider when designing
the reduction rules (see Section 5.2).
Lemma 9 (Reduction Substitution). If A Ð→ B , then [τ /x ] A Ð→ [τ /x ] B
Theorem 10 (Type Correctness). If Γ ⊢ e1 ≤ e2 ∶ A, then ∃k. Γ ⊢ A ∶ k or
A = ◻.
Type correctness is a nice property that ensures that what appears in the position of a type is actually a type. The theorem is proved by induction on thederivation of Γ ⊢ e1 ≤ e2 ∶ A. The only non-trivial case is when the derivationends with rule s-app. We make use of the substitution lemma and the inductive hypothesis to demonstrate the head of a Π type preserves its kind after theargument is applied.
4.3. Transitivity
Transitivity is typically one of the most challenging properties to prove incalculi with subtyping and it was also one of the harder proofs in λ∀I . The proofof transitivity requires a generalization of the usual transitivity property:
22

Theorem 11 (Generalized Transitivity). If Γ ⊢ e1 ≤ e2 ∶ A and Γ ⊢ e2 ≤e3 ∶ B , then Γ ⊢ e1 ≤ e3 ∶ A.
where the types of the premises are potentially different. To prove this property
we employ sizes for the inductive argument. Moreover we rely on a subtle
property of uniqueness of kinds.
Uniqueness of Kinds. Assuming that the second premise of generalized transitivity is derived by rule s-forall-r, then we face the following problem:Γ ⊢ e1 ≤ e2 ∶ A

Γ, x ∶ B ⊢ e2 ≤ C ∶ ⋆Γ ⊢ e1 ≤ ∀ x ∶ B . C ∶ A
Before applying rule s-forall-r to the conclusion, we have to establish therelationship between A and ⋆. Were there no restrictions on the kinding of ∀types, this would be a much more complicated situation, where the inversion
lemmas of about kinds and transitivity depend on each other. This is one of
the main reasons why we forbid ∀ types having kind ◻. Then we can have thefollowing theorem:
Theorem 12 (Kind Uniqueness). If Γ ⊢ e ∶ k and Γ ⊢ e ∶ A, then A = k.
The proof is achieved by generalizing the shape of k to be Πx ∶ A. . . . Πx ∶ B. . . . kfor obtaining useful inductive hypotheses when Γ ⊢ e ∶ k is derived by rule sapp. Then the proof proceeds with induction on the derivation of the generalizedΓ ⊢ e ∶ k and assembling various lemmas of kinding to solve different cases.
With the help of kind uniqueness, we ensure the equivalence of A and ⋆ on
this and other similar situations.
The Induction. We prove generalized transitivity by performing a strong induction on the ordered 3-tuple of measures:⟨#∀(e1 ) + #∀(e2 ) + #∀(e3 ), size(e1 ) + size(e3 ), D1 + D2 ⟩where• #∀(e) counts the number of ∀ quantifiers in expression e, which solves
cases when either side of the premise is derived by rules s-forall, sforall-l, and s-forall-r.
• size(e) measures the size of the syntax tree of expression e. The sum of
expression sizes solves most of the other standard recursive cases.
• D1 and D2 denote the sizes of the derivation trees of the first and thesecond premise respectively. The sum of sizes of derivation tree solves thecase involving rule s-sub where the sizes of expressions do not decrease.

23

The proof is mainly inspired by DK’s transitivity proof of their declarative
subtyping system of induction on the pair of ⟨#∀(e2 ), D1 + D2 ⟩ (Dunfield andKrishnaswami, 2013), with some adjustments to fit in our system.
The most problematic case to solve is when the first premise is derived byrule s-forall-r, and the second is derived by rule s-forall-l. Essentially wehave to show the following:
Γ, x ∶ A ⊢ e1 ≤ B ∶ ⋆Γ ⊢ [τ /x ] B ≤ e3 ∶ ⋆Γ⊢τ ∶AΓ ⊢ e1 ≤ e3 ∶ ⋆Here the only decreasing measure we can rely on is that #∀([τ /x ] B ) is one
less than #∀(∀ x ∶ A. B ) (since τ is a monotype which does not contain any ∀quantifier). To solve this case, we first perform a substitution on the premiseΓ, x ∶ A ⊢ e1 ≤ B ∶ ⋆ with the help of the fact that x does not occur in e1 ,obtaining Γ ⊢ e1 ≤ [τ /x ] B ∶ ⋆, then we use the inductive hypothesis provided
by #∀(e2 ).
The reason why we cannot directly copy DK’s proof measure is because of thecase when both premises end with rule s-pi, where we encounter the following
problem:Γ, x ∶ A2 ⊢ B1 ≤ B2 ∶ k

Γ, x ∶ A3 ⊢ B2 ≤ B3 ∶ k

Γ ⊢ A3 ≤ A2 ∶ k2

Γ, x ∶ A3 ⊢ B1 ≤ B3 ∶ k
The first and the second premise above do not share the same context, whichmust be unified with the context narrowing theorem to be able to use the inductive hypothesis. However context narrowing potentially increases the size of thederivation tree, so we are not able to use the inductive hypothesis of D1 + D2 ,and resort to the sizes of expressions (size(e1 ) + size(e3 ))We have to make adjustments to solve the cases which preserve the size ofderivation tree, but not the sizes of the expressions, which is when the firstpremise is derived by rule s-forall-l:Γ ⊢ [τ /x ] B ≤ e2 ∶ ⋆Γ ⊢ e2 ≤ e3 ∶ CΓ ⊢ ∀ x ∶ A. B ≤ e3 ∶ ⋆In this case, #∀([τ /x ] B ) is one less than #∀(∀ x ∶ A. B ), so it can be solved byapplying rule s-forall-l and the inductive hypothesis of #∀(e1 ). Additionally,#∀(e3 ) is added to make the measure “symmetric” to handle the contravariancecase of rule s-pi.
Then, most of the cases that do not involve ∀ can be solved by applying theinductive hypothesis corresponding to size(e1 )+size(e3 ). Finally, D1 +D2 solves
the cases where either premise ends with rule r-sub, where the only decreasing
measure is the size of the derivation trees when the sizes of expressions remain
the same.

24

Corollary 13 (Transitivity). If Γ ⊢ e1 ≤ e2 ∶ A and Γ ⊢ e2 ≤ e3 ∶ A, thenΓ ⊢ e1 ≤ e3 ∶ A.
Transitivity is a special case of generalized transitivity where A = B.
4.4. Type Safety
Since the reduction rules of λ∀I do not have access to typing information,
they cannot perform valid instantiation checks of the implicit arguments during
applications. Thus, the runtime semantics is non-deterministic and potentiallynon-type-preserving. We tackle this issue by employing designs that make thechoices of implicit instantiations irrelevant at runtime with the occurrence restrictions in rule s-bind. We define an erasure function (shown in Figure 4)
that eliminates the type annotations in some expressions (λ, Λ, µ and cast⇑ ),and keep implicit parameters from occurring in the erased expressions. Thisway the choices of implicit instantiations only affect type annotations, which
are not relevant for runtime computation.
We show that λ∀I is type-safe in the sense that, if an expression is well-typed,
then the reduction of its erased version does not “go wrong”. Figure 4 shows
the semantics of erased expressions. The erasure semantics mostly mirrors thesemantics shown in Figure 3, except for rules er-elim and er-cast-elim, whichconveys the idea of the irrelevance of implicit instantiation by eliminating theparameter directly.
Progress. We show the progress property for both the original expressions andthe erased expressions.
Theorem 14 (Generalized progress). If ∅ ⊢ e1 ≤ e2 ∶ A, then ∃ e′1 . e1 Ð→ e′1
or e1 is a value, and ∃ e′2 . e2 Ð→ e′2 or e2 is a value.
Theorem 15 (Generalized progress on erased expressions). If ∅ ⊢ e1 ≤e2 ∶ A, then ∃ E1′ . ∣e1 ∣ Ô⇒ E1′ or ∣e1 ∣ is an erased value, and ∃ E2′ . ∣e2 ∣ Ô⇒ E2′ or∣e2 ∣ is an erased value.
We prove a generalized version of progress that involves both sides of the expressions with unified subtyping. Note that they are not necessarily simultaneously
reducible or irreducible due to the presence of rules s-forall-l and s-forallr. The left-hand-side may be reducible with the right-hand-side being a value
or vice versa.
Both theorems are proved by induction on the derivation of ∅ ⊢ e1 ≤ e2 ∶ A.
The proof is mostly straightforward except when the derivation ends with cast⇓ ,where we have to show that the inner expressions e of cast⇓ e either reduces, oris a cast⇑ or a Λ-expression. We prove another fact to solve the situation: fora well-typed expression whose type reduces, that expression cannot be a value
unless it is a cast⇑ or Λ-expression.
Lemma 16 (Reducible Type). If Γ ⊢ e ∶ A, A Ð→ B and e is not cast⇑ or aΛ-expression, then e is not a value.
25

e∶A

e′ ∶ A
Annotation

ErasureE

E′

Figure 6: Diagram for Erased Preservation without Subtyping

Lemma 17 (Erased Value to Value). If ∣e∣ is an erased value, then e is avalue.
This lemma is also useful for the proof of progress for erased expressions.
Since the value definitions are very similar, we can use the property of values
on erased values.
Lemma 18 (Value to Erased Value). If e is a value, then ∣e∣ is an erased
value.
Corollary 19 (Progress). If ∅ ⊢ e ∶ A, then ∃ e′ . e Ð→ e′ or e is a value.
Corollary 20 (Progress on erased expressions). If ∅ ⊢ e ∶ A, then ∃ E ′ . ∣e∣ Ô⇒
E ′ or ∣e∣ is an erased value.
Both corollaries directly follow from their generalized versions.
Preservation. The direct operational semantics is not generally type-preserving
and deterministic because of the implicit instantiations. Thus, we show preservation with the help of the erased expressions (where implicit parameters do
not matter to the computation). For other reduction rules that do not involve
such issues, we discuss them as though we are proving a normal preservation
for brevity.
Theorem 21 (Subtype Preservation). If Γ ⊢ e1 ≤ e2 ∶ A, ∣e1 ∣ Ô⇒ E1′ and∣e2 ∣ Ô⇒ E2′ , then ∃ e′1 e′2 . ∣e′1 ∣ = E1′ , ∣e′2 ∣ = E2′ , e1 Ð→ e′1 , e2 Ð→ e′2 and Γ ⊢ e′1 ≤e′2 ∶ A.
The theorem might look a little complicated at first glance. It breaks down into
two aspects: the erasure-annotation process and the subtype preservation.
Figure 6 shows the idea of our preservation lemma without considering thesubtyping aspect (assuming Γ ⊢ e ∶ A instead of Γ ⊢ e1 ≤ e2 ∶ A). Here weuse annotation as the reverse process of erasure. If an expression (e) is welltyped, and its erasure (E) reduces to another erased expression (E ′ ), we canfind a “annotated” expression of E ′ (e′ ) that is reduced by e and also preserves
the type A. When no implicit instantiation happens in the reduction, thene Ð→ e′ is deterministic: i.e. it is just normal type preservation. When there are
implicit instantiations, if the erased expression can reduce, we show that there
exists a valid instantiation for e that preserves its type after the reduction, and26

this instantiation only affects type annotations. In other words, the runtime
semantics of λ∀I can be implemented only with erased expressions.
Aside from the erasure aspect of our preservation lemma, we also consider thegeneralized version of preservation in our unified subtyping system, the subtype
preservation, where reductions not only preserve the type of expressions, theyalso preserve the subtyping relation between expressions as well.
The theorem is proved by induction on the derivation of Γ ⊢ e1 ≤ e2 ∶ A,
cases for rules r-beta and r-mu are solved with the substitution theorem, cases
rules r-app and r-castdn are solved by inductive hypotheses. The interestingcases to prove are rule r-cast-elim and cases involving implicit instantiation(rules r-inst and r-cast-inst).
Cast Elimination. The main issue of the cast elimination case can be demonstrated by the following derivation:
A1 Ð→ A2
Γ ⊢ A1 ≤ B1 ∶ k
B1 Ð→ B2Γ ⊢ e ∶ A2

Γ ⊢ cast⇑ [A1 ] e ∶ A1

Γ ⊢ cast⇑ [A1 ] e ∶ B1
Γ ⊢ cast⇓ (cast⇑ [A1 ] e) ∶ B2

s-castups-subs-castdn

Here the typing of the inner cast⇑ is not directly derived by rule r-castup,
but by the subsumption rule instead. We want to show that after the castelimination (following rule r-cast-elim), expression e has type B2 , while inreality it has type A2 (as highlighted). Therefore want to show Γ ⊢ A2 ≤ B2
with the information that Γ ⊢ A1 ≤ B1 , A1 Ð→ A2 and B1 Ð→ B2 , which depends
on the property we want to prove initially, subtype preservation. Since subtype
preservation needs to solve the cast elimination case, here we have a circulardependency of properties. This problem was also observed by Yang and Oliveira(2017). They solved this situation by a delicate approach with the help of an
essential lemma reduction exists in the middle (If Γ ⊢ e1 ≤ e2 ∶ A, Γ ⊢ e2 ≤ e3 ∶ A
and e1 Ð→ e′1 , e3 Ð→ e′3 , there exists e′2 such that e2 Ð→ e′2 ). Unfortunately
this lemma does not hold in our system since universal types, which are not
reducible, can appear in the middle of two reducible types, so we cannot adopt
their proof on this case.
We tackle this problem from another direction, with the observation thatthe demand for subtype preservation property shifts from the term-level to thetype-level. With the Calculus-of-Constructions-like kind hierarchy, our system
only has limited layers in types (type N has kind ⋆, kind ⋆ has kind ◻). In
fact, we only need to go up one layer in the type hierarchy to be able to obtain
subtype preservation directly, since there is no subtyping at the kind level, hence
no problem for the cast elimination there. Even better, we show that by goingup one level in the type hierarchy (only discussing the types of terms), theoptions for the reduction that can be performed by a well-typed term are very
limited. Implicit abstractions cannot occur in type computation due to the kind27

A1 Ð→D A2(Deterministic Reduction)

dr-appe1 Ð→D e2

dr-betae1 e3 Ð→D e2 e3(λ x ∶ A. e1 ) e2 Ð→D [e2 /x ] e1

dr-mu

µ x ∶ A. e Ð→D [µ x ∶ A. e/x ] e

Figure 7: Deterministic Reduction.

restriction of universal types as explained in Section 3.3. Furthermore, we also
prove that well-typed reductions never occur for kinds, so cast operators also
do not occur in type-level computation.
Figure 7 shows the effective reduction rules inside cast operators.
Lemma 22 (Deterministic Reduction). If A Ð→D A1 and A Ð→D A2 ,then A1 = A2 .
Lemma 23 (Deterministic Type Reduction). If Γ ⊢ A1 ∶ k and A1 Ð→
A2 , then A1 Ð→D A2 .
The cases for implicit abstractions are easy to prove. For the cast operators
we have the following lemma.
Lemma 24 (Expressions of kind ◻ are never reduced). If A Ð→ B andΓ ⊢ e ∶ A, then B does not have kind ◻.
At first sight, the result of this lemma may be surprising because it meansthat we cannot construct a reducible expression like: (λ x ∶ N. ⋆) 42 which
has kind ◻. In reality, the lambda expression must be of type N → ◻ for theapplication to be well-typed. However, as we employ the conventional typing
rule for lambda abstractions of Calculus of Constructions (Coquand and Huet,
1988), the function types of the lambda abstractions themselves must be wellkinded (see rule s-abs). Since ◻ itself does not have a kind, N → ◻ is not
well-kinded, therefore the whole application is not well-typed. For this reason,
the position where kind ⋆ can occur in a well-typed expression is very restricted,
hence the lemma is provable.
With the previous lemmas, the subtype preservation lemma for type computation is easily shown.
Lemma 25 (Subtype Preservation for Types). If Γ ⊢ A1 ≤ B1 ∶ k , A1 Ð→DA2 and B1 Ð→D B2 , then Γ ⊢ A2 ≤ B2 ∶ k .

28

Implicit Instantiations. The proof of two cases for implicit instantiations (rules rinst and r-cast-inst) are quite similar. In our language, implicit instantiationsof implicit functions are only triggered by rule s-forall-l, which is exactly
where polymorphic types are instantiated. The implicit argument is the same
mono-expression (τ ) that instantiates the polymorphic type in rule s-forall-l.
The type of the instantiation result of Λ expression is the same as the instantiation of the polymorphic types, with the same argument.
With the observations above, the remaining proofs are finished by standard
inversion lemmas, with the help of the substitution theorem to handle typepreservation after the instantiations.
4.5. Equivalence to a Simplified System
We mentioned in Section 3.3 that the premises boxed by dashed lines in
the unified subtyping rules are redundant. They help in the formalization,
but the calculus is equivalent to a variant of the calculus without them. We
define unified subtyping relation Γ ⊢s e1 ≤ e2 ∶ A, whose rules are the same as
the unified subtyping rules of λ∀I , but with all redundant premises eliminated.
Also, rules s-castdn and s-castup are simplified to use deterministic reduction(A Ð→D B) instead of the reduction rule A Ð→ B as shown below (other rules
are omitted):Γ ⊢s e1 ≤ e2 ∶ A(Simplified Unified Subtyping)ss-castdn

ss-castupΓ ⊢s cast⇓ e1 ≤ cast⇓ e2 ∶ BΓ ⊢s cast⇑ [A] e1 ≤ cast⇑ [A] e2 ∶ BΓ ⊢s e1 ≤ e2 ∶ A
A Ð→D BΓ ⊢s B ∶ kΓ ⊢s e1 ≤ e2 ∶ B
A Ð→D BΓ ⊢s A ∶ k

We prove that the two system are equivalent in terms of expressiveness.
Theorem 26 (Equivalence of λ∀I and the Simplification). If Γ ⊢ e1 ≤ e2 ∶A then Γ ⊢s e1 ≤ e2 ∶ A. And if Γ ⊢s e1 ≤ e2 ∶ A then Γ ⊢ e1 ≤ e2 ∶ A.
4.6. Subsumption of Polymorphic Subtyping
Finally we show that the subtyping aspect of λ∀I subsumes Odersky and
Läufer’s polymorphic subtyping (Odersky and Läufer, 1996). To be more precise we show that our unified subtyping relation subsumes DK’s declarative
subtyping relation (Dunfield and Krishnaswami, 2013), whose syntax and subtyping relation are shown in Figure 1.
Figure 8 shows the transformation from DK’s types to λ∀I ’s types. Then
we prove the subsumption in terms of type well-formedness and subtyping byfollowing the interpretation of unified subtyping.
Theorem 27 (Subsumption of Type Well-formedness). If Γ ⊢DK A, then⌈Γ⌉ ⊢ ⌈A⌉ ∶ ⋆29⌈x⌉ = x⌈N⌉ = N⌈A → B⌉ = ⌈A⌉ → ⌈B⌉⌈∅⌉ = ∅⌈∀x. A⌉ = ∀x ∶ ⋆. ⌈A⌉⌈Γ, x⌉ = ⌈Γ⌉, x ∶ ⋆Figure 8: Lifting Types and Contexts in Polymorphic Subtyping to λ∀I

Straightforward. For the case where A = ∀x.B, rule s-forall can be useddirectly bypassing the complications of rule s-forall-l and rule s-forall-r.
Theorem 28 (Subsumption of Polymorphic Subtyping). If Γ ⊢DK A ≤B, then ⌈Γ⌉ ⊢ ⌈A⌉ ≤ ⌈B⌉ ∶ ⋆The interesting cases are when the premise is derived by ≤∀L or ≤∀R, because of the addition of premises in our generalized system (Γ, x ∶ A ⊢ B ∶ ⋆in rule s-forall-l, Γ ⊢ A ∶ ⋆ in rule s-forall-r). Both cases can be solved
with the help of the well-formedness lemma in DK’s system. We can conclude
Γ, x ⊢DK A from Γ ⊢DK ∀x. A ≤ B for the ≤∀L case, and conclude Γ ⊢DK A fromΓ ⊢DK A ≤ ∀x. B for the ≤∀R case. Then Theorem 27 can be used to solve theadditional premises in λ∀I.
5. Discussions and Future WorkIn this section we discuss some design choices and alternatives, as well as
possible future work.
5.1. Open Terms Reduction
Usually, only closed terms are considered when designing the operationalsemantics, and irreducible open terms like variables are not considered to bevalues. However, since in λ∀I the reduction relation e1 Ð→ e2 is also used in
the unified subtyping relation, the reduced expressions can be open terms andwell-typed under contexts. Yang and Oliveira (2017) observed this issue andincluded inert terms (Accattoli and Guerrieri, 2016) as values to handle the situation that open terms like x e (applying variable x to the argument e) is also
irreducible, which considerably complicates their metatheory around the operational semantics. Fortunately, our call-by-name reduction rules do not rely on
the notion of value, which for closed terms, represents irreducible forms. In otherwords, there is no premise in our reduction rules that require some expression
to be a value or irreducible. Thus, the definition of values or irreducible terms
does not matter when reasoning about type-level call-by-name reductions, andwe do not have to complicate the metatheory of our system with inert terms.

30

5.2. Call-by-value Semantics of Cast Operators
An alternative design around cast operators is the call-by-value (CBV) style (Yangand Oliveira, 2019), by not considering all cast⇑ terms as values, and performing cast elimination only when the expression inside two casts is a value. Suchdesign requires us to have a more general definition of value, and there would
be a need for inert terms as mentioned in Section 5.1
However, a simple design with CBV-style cast semantics and inert terms
potentially leads to a system where reduction substitution (see Section 4.2) does
not hold. With the CBV-style reduction rules, which consist of the following
rules:
cbv-r-castdn

cbv-r-castup

cast⇓ e1 Ð→cbv cast⇓ e2cast⇑ [A] e1 Ð→cbv cast⇑ [A] e2

e1 Ð→cbv e2

e1 Ð→cbv e2

cbv-r-cast-elimvalue ecast⇓ (cast⇑ [A] e) Ð→cbv e
Assuming that the notion of value is properly defined to capture irreducible
open terms, these rules allow reductions like:cast⇓ (cast⇑ [A] (f x)) Ð→cbv f x
The reduction substitution property breaks if we substitute f to a lambda expression:[λy ∶ B. x/f ] cast⇓ (cast⇑ [A] (f x)) Ð→cbv cast⇓ (cast⇑ [A] x)
The reduction rule prioritizes reducing the inner expression of two casts, while
reduction substitution expects [λy ∶ B. x/f ] cast⇓ (cast⇑ [A] (f x)) to reduce to(λy ∶ B. y) x.
So we stick with the call-by-name style semantics for cast operators for now
and leave the discussion of other possibilities of design in future work.
5.3. Kind Restrictions on Polymorphic Types
Currently, we impose restrictions on the kinding of polymorphic types (∀x ∶A. B) to require that they only have kind ⋆ but not ◻. We believe that thishas little impact on the usability of our system since polymorphic kinds suchas ∀ x ∶ N. ⋆ do not appear frequently in practice. It would be reasonable
not to have this restriction, but this would complicate the development of themetatheory significantly.
One of the obstacles to removing the kind restriction is that there is a mutual
dependency between the transitivity theorem and the subtyping reasoning of31

polymorphic kinds. We wish to have some lemma like this:Γ⊢e ∶AΓ⊢e ∶⋆Γ⊢⋆≤A∶◻
which depends on transitivity when the derivation of Γ ⊢ e ∶ A ends with subsumption rule (rule s-sub).
Note that the reverse variant of the lemma (If Γ ⊢ e ∶ A and Γ ⊢ e ∶ ⋆ thenΓ ⊢ A ≤ ⋆ ∶ ◻) is not generally true. A counter example is A ∶ ⋆ ⊢ ∀a ∶ A. ⋆ ≤ ⋆,which does not hold if we are unable to find a well-typed instantiation of anarbitrary type A. In turn, this breaks transitivity, when the derivation of thefirst premise ends with rule s-forall-l:Γ ⊢ [τ /x ] e1 ≤ e2 ∶ ⋆Γ ⊢ e2 ≤ e3 ∶ BΓ⊢τ ∶AΓ ⊢ ∀ x ∶ A. e1 ≤ e3 ∶ ⋆We cannot apply rule s-forall-l unless we can show e3 is of type ⋆. One ofthe possibilities in this scenario is to show Γ ⊢ B ≤ ⋆ ∶ ◻, which does not always
hold for the reason discussed above.
Moreover, we expect complexities while reasoning about the kinding of types
after we lose the kinding uniqueness in other parts of the metatheory. Therefore
we leave the relaxation of the kinding restrictions for future work.
5.4. Runtime Relevance of Implicit Arguments
In our language, the implicit arguments have no computational impact atruntime and only provide the necessary scoping for type annotations. This isa similar design to ICC (Miquel, 2001) and ICC* (Barras and Bernardo, 2008)
to simplify the development of a direct operational semantics for our language.
Such a restriction can be lifted if we prove the runtime type-safety by elaboration
to a second language, such as the Calculus of Constructions (Coquand and Huet,
1988), instead of providing the direct operational semantics.
We can elaborate implicit function types (universal types) to Π types, implicit abstractions to lambda expressions, and implicit instantiations to explicit
applications during type checking (when we have full information about the
choice of implicit instantiations). However the elaboration on a unified subtyping system is not an easy task. The subtyping relation cannot simply beinterpreted as a coercion between values of different types, since some of our
subtyping rules involve a relation between terms instead of types. In otherwords, unified subtyping generalizes conventional subtyping relations that are
defined on types only, to a relation defined on general terms. Therefore we leave
the exploration of how elaboration can be done on a unified subtyping system
as future work.
5.5. Algorithmic System and Challenges
λ∀I does not currently have an algorithmic system since we consider a formalized algorithm for dependent type system itself a substantial challenge. Thus, an32algorithmic formulation it is left for future work. While comparing to existingalgorithmic systems for higher-ranked polymorphic type inference for System
F-like languages (Dunfield and Krishnaswami, 2013; Zhao et al., 2019), we
identify one of the interesting challenges to develop an algorithmic system forλ∀I.
In dependent type systems, the type of applications potentially depends onthe values of their arguments. Therefore the unification problem we meet ispotentially inside binders and depends on the value of the arguments. For an
example in λ∀I , consider:λF ∶ N → ⋆. λf ∶ F 42 → N. f ((ΛA ∶ ⋆. µx ∶ A. x) 42)
Here the type of ΛA ∶ ⋆. µx ∶ A. x should be ∀A ∶ ⋆. A. In a non-dependentsetting, one can easily conclude the instantiation for type A to be F 42 → N.
However in our system, the type of A is a dependent function type, with theshape of (Πx ∶ N. F e), where expression e satisfies the equation [42/x] e = 42
according to rule s-app. Here we have two choices for the instantiation of e,
namely x and 42, but neither choice (Πx. F x or Πx. F 42) for type A leads toa more general solution than choosing the other.
Notably, for a similar reason, the decidable pattern fragment of higher-orderunification (Miller, 1991a) specifically forbids scenarios where a unification variable applies to constants. The case shown above is similar, where the “application” is A 42 (dependent function type A “applies” to 42) with unification
variable A. Nonetheless, because our system does not allow implicit type-levelcomputation (hence unifications remain at first-order), the choices of A are restricted to Πx ∶ N. F e1 where [42/x] e1 = 42. With higher-order unification, we
would instead have Πx ∶ N. e2 where [42/x] e2 = F 42.
There are potentially multiple approaches to this problem. For example, we
can impose a similar restriction to the pattern unification and refuse to solve thiskind of conflict entirely. Alternatively, we can only infer non-dependent function
types when facing a unification variable, which is the choice by Eisenberg (2016).
But which is the better method for our system remains to be studied.
5.6. The Issues of Strengthening
The current lack of a proof for strengthening leads to non-trivial changes during the generalization of polymorphic subtyping relation as described in Section
4.1. It would be nice to be able to have strengthening to simplify λ∀I . However
the issues are quite tricky.
Type Inhabitation. As we mentioned earlier, one of the issues is centered aroundnot being able to find a well-typed instantiation for an arbitrary type in general.
Some instantiations can only be found in the presence of seemingly unusedvariables, which is a key reason for strengthening not holding in general. For
example:A ∶ ⋆, a ∶ A ⊢ (Λ x ∶ A. λ y ∶ N. y) 42 ∶ N
33

Here, to conclude that Λ x ∶ A. λ y ∶ N. y has type N → N, we want toderive ∀x ∶ A. N → N ≤ N → N by using rule s-forall-l. That would require
a well-typed instantiation for the abstract type A, which is where the variable
a in the context comes to rescue, although not being used anywhere in theoriginal conclusion. Thus, unlike other calculi where it is possible to drop unusedvariables in the context and still have a valid typing statement, in λ∀I , it is
not always possible. In the example above dropping a ∶ A from the context
sabotages the subtyping relation ∀x ∶ A. N → N ≤ N → N we rely on to conclude
the typing relation. (unless we can find another inhabitant for type A somehow).
However, since λ∀I supports fixpoints, all monotypes in our system are easily
inhabited with diverging programs as inhabitants (recall that, due to the issue
discussed in Section 4.1, our fixpoints only support monotypes). For instance,
we do not need the variable a in the context in the example above, we can justfind the instantiation µ x ∶ A. x to satisfy rule s-forall-l for any monotype A.
Moreover, it is likely that any polytype is inhabited with the help of monotype
fixpoints. For example, type ∀A ∶ ⋆. A → B with B being an abstract type, has
an inhabitant ΛA ∶ ⋆. λ x ∶ A. µ y ∶ B . y.
Nevertheless, since polymorphic types in our system also serve as “implicit
function types”, it would be weird to infer diverging programs as their implicit
arguments. Inferring infinite loops is not a big deal for the time being, because
we guarantee the runtime irrelevance of all the implicit arguments. But thisdesign will not be reasonable if we are going to relax the restriction of runtime
irrelevance of implicit parameters in the future. Furthermore, it is also reasonable to consider similar language designs without fixpoints (for instance, if
our goals are to develop theorem provers or strongly normalizing languages). In
this case, the approach of finding inhabitants by creating non-terminating terms
would not be possible. Thus such an approach would not be very generalizable.
Occurrences of variables that matter. Another issue for the strengthening isthat even if we have the issue of inhabitability covered, it is tricky to guaranteethat a variable unused in the final subtyping conclusion, does not matter for
the whole derivation. For example, in rule s-app, where type A in the premises
does not occur at all in the conclusion, we cannot guarantee that a variable notoccurring in the conclusion, does not occur in type A. We can construct thefollowing example:
T ∶ ⋆ ⊢ 42 ∶ ∀y ∶ T → T. N

T ∶ ⋆ ⊢ λ x ∶ N. x ∶ (∀y ∶ T → T. N) → N

T ∶ ⋆ ⊢ (λ x ∶ N. x ) 42 ∶ N

s-app

Here the variable T does not occur in the conclusion (other than in the context,
of course), but occurs in the premises. The interesting part is that although it occurs in the premises, without it, the conclusion holds with a different derivation
tree (by directly deriving ⊢ 42 ∶ N). For this example, although the strengthening property holds, we do not currently know how to determine whether avariable really matters for a derivation in general, so that we can safely remove34

it from the context.
So for the two issues we discussed above, we decide to live with the lackof strengthening property in our system for now, at the cost of a slightly more
complicated system with additional kinding premises in rule s-forall-r andthe addition of rule s-forall.
6. Related Work
Implicit Dependent Type Calculus. Implicit polymorphism in a dependently
typed setting is discussed in the implicit calculus of constructions (ICC) (Miquel,2001) and ICC*(Barras and Bernardo, 2008). The ICC features generalizedpolymorphic types and typing rules to express the idea of implicit instantiation.
The ICC does not explicitly have a subtyping relation between polymorphic
types. Therefore the expressiveness of reasoning between polymorphic types islimited to top-level polymorphic types. Like in λ∀I , implicit parameters does not
impact the runtime semantics of the ICC.
Implicit function types in ICC* are not interpreted as polymorphic function
types. The main focus is on the distinction between implicit functions (universal types and implicit abstraction) and explicit functions (Π-types and lambda
abstraction). The typing rules about the implicit part and explicit part of thelanguage mirror each other. The generalization and instantiation aspect of theimplicit function types are not featured. ICC* depends on its transformation to
ICC to obtain type safety of the language, therefore the parameters of implicit
functions have no impact on runtime behaviour as well.
Type-inference and unification with dependent types. There has been little workon formalizing type inference for calculi with dependent types, although essentially all implementations of theorem provers or dependently typed languages
perform some form of type-inference. One important challenge for type inference in systems with dependent types and a conversion rule is that theyrequire higher-order unification, which is known to be undecidable (Goldfarb,1981). The pattern fragment (Miller, 1991b) is a well-known decidable fragment. Much literature on unification for dependent types (Reed, 2009; Abeland Pientka, 2011; Gundry and McBride, 2013; Cockx et al., 2016; Ziliani andSozeau, 2015; Coen, 2004) is built upon the pattern fragment. Algorithms for
type-inference used in Agda and (Dependent) Haskell have been described andformalized to some degree in various theses (Norell, 2017; Gundry, 2013; Eisenberg, 2016). However, as far as we know there is not a clear specification andcomplete metatheory (let alone mechanized) for such algorithms.
The current GHC Haskell’s language of types and kinds is already dependently typed, but has no type conversion. Thus it is able to avoid higher-orderunification. Recent work by Xie et al. (2020) describes algorithms and specifications for the form of (dependently typed) kind-inference currently present in
GHC Haskell. The dependently typed language of types and kinds is closely
related to λ∀I . In particular in both calculi type equality is based only on αequivalence. One difference is that in GHC Haskell and, more precisely, in the35core language employed by GHC, there are no type-level lambdas. The GHC
Haskell source language does allow type families (Chakravarty et al., 2005),
which mimic type-level functions. However, type families, unlike lambda functions, are not first class, and do not support partial application. They are
encoded in terms of equality constraints, casts and mechanisms similar to those
employed by type classes. There is some work to make type-level functions
provided type families first-class (Kiss et al., 2019) and also partially applied,but this still does not enable full type-level lambdas (see also the discussion in
Section 8.1 of Kiss et al. (2019) for more details). In our work we do allow
type-level lambdas but lambdas can only be equal up to α-equivalence. Another difference is that the kind-inference system formalized by Xie et al. is
not higher-ranked like ours. In this way Xie et al. manage to avoid the mutual
dependency issue that we have in our polymorphic subtyping relation.
Type-inference for higher-ranked polymorphism. Type-inference for higher-ranked
polymorphism (HRP) (Dunfield and Krishnaswami, 2013; Le Botlan and Rémy,
2003; Leijen, 2008; Vytiniotis et al., 2008; Peyton Jones et al., 2007; Serrano
et al., 2018; Odersky and Läufer, 1996; Zhao et al., 2019) extends the classic Hindley-Milner algorithm (Hindley, 1969; Milner, 1978; Damas and Milner,
1982), removing the restriction of top-level (let) polymorphism only. Type inference for HRP aims at providing inference for System F-like languages. In
particular existing HRP approaches allow synthesis of type arguments and use
type annotations to aid inference, since type-inference for full System F is wellknown to be undecidable (Wells, 1999).
The work on HRP is divided into two strands: predicative HRP (Dunfield and Krishnaswami, 2013; Peyton Jones et al., 2007; Odersky and Läufer,
1996; Dunfield and Krishnaswami, 2019; Zhao et al., 2019) and impredicative
HRP (Le Botlan and Rémy, 2003; Leijen, 2008; Vytiniotis et al., 2008; Serrano
et al., 2018). In predicative HRP instantiations can only synthesize monotypes,
whereas in impredicative HRP there’s no such restriction. However, impredicative HRP is quite complex because the polymorphic subtyping relation for
impredicative HRP is undecidable (Tiuryn and Urzyczyn, 1996). Thus reasonable restrictions that work well in practice are still a focus of active research.
The monotype restriction on predicative instantiation is considered reasonable
and practical for most programs. It is currently in use by languages such as(GHC) Haskell, Unison (Chiusano and Bjarnason, 2015) and PureScript (Freeman, 2017). The original work on polymorphic subtyping by Odersky and Läufer
also enforces the monotype restriction in their subtyping rules (rule ≤∀L) to prevent choosing a polytype in the instantiation. Based on polymorphic subtyping
as their declarative system, Dunfield and Krishnaswami (2013) (DK) develop
an algorithmic system for predicative HRP type inference. DK’s algorithm was
manually proved to be sound, complete, and decidable. With a more complex
declarative system (Dunfield and Krishnaswami, 2019), DK extended their original work with new features. Recently Zhao et al. (2019) formalized DK’s typesystem in the Abella theorem prover.

36

Dependent Types and Subtyping. A major difficulty in languages with subtyping
is that the introduction of dependent types makes typing and subtyping dependon each other. This causes several difficulties in developing the metatheory
for calculi that combine dependent types and subtyping. Almost all previous
work (Aspinall and Compagnoni, 1996; Zwanenburg, 1999; Castagna and Chen,
2001; Chen, 1997, 2003) attempts to address such problem by somehow untangling typing and subtyping, which has the benefit that the metatheory forsubtyping can be developed before the metatheory of typing. Nevertheless,several results and features prove to be challenging.
Our work builds on the work done on Pure Iso-Type Systems (PITS) (Yangand Oliveira, 2019), and unified subtyping (Yang and Oliveira, 2017). PITS
is a variant of pure type systems (PTSs), which captures a family of calculi
with iso-types. Iso-types generalize iso-recursive types (Pierce, 2002), and provide a simple form of type casts to address the combination of recursion anddependent types. Yang and Oliveira (2017) introduce a calculus, called λI , supporting OOP features such as higher-order subtyping (Pierce and Steffen, 1997),
bounded quantification and top types. To address the challenges posed by the
combination of dependent types and subtyping, λI employs unified subtyping: a
novel technique that unifies typing, subtyping and well-formedness into one relation. Therefore, λI takes a significantly different approach compared to previous
work, which attempts to fight the entanglement between typing and subtyping.
In contrast, λI embraces such tangling by collapsing the typing and subtyping
relations into the same relation. This approach is different from Hutchins’ technique, which eliminates the typing relation and replaces it with a combinationof subtyping, well-formedness and reduction relations. In contrast, unified subtyping retains the traditional concepts of typing and subtyping, which are justtwo particular cases of the unified subtyping relation.
Although the λI calculus formalized by Yang and Oliveira shares the use of
unified subtyping with λ∀I , there are substantial differences between the two calculi. Most importantly, λI only has explicit polymorphism via Π types. There
are no implicit functions and universal quantification (∀ types) in λI , and also
no guessing of monotypes. λ∀I supports implicit polymorphism, and guessing themonotypes used for instantiation brings significant complications, for instancefor proving type safety (as discussed in Section 4.4). The subtyping rules foruniversal quantification (which do not exist in λI ) also bring considerable challenges for transitivity, and the proof technique used by λ∀I differs considerablyfrom the proof technique used in λI. Unlike λI , λ∀I does not support bounded
quantification, which brings some welcome simplifications to some of the unified
subtyping rules. Besides these differences other differences include the use of acall-by-name semantics in λ∀I (see also the discussion in Sections 5.1 and 5.2),
and the use of the ⋆ ∶ ◻ axiom in λ∀I versus the use of ⋆ ∶ ⋆ in λI .
Dependent Types with Explicit Casts. Another problem is the interaction between dependent types and recursion. For this problem, a general solution thathas recently emerged is the use of type casts to control type-level computation.
In such an approach explicit casts are used for performing type-level compu37

tations. A motivation for using type casts is to decouple strong normalizationfrom the proofs of metatheory, which also makes it possible to allow generalrecursion. There have been several studies (Stump et al., 2008; Sjöberg et al.,2012; Kimmell et al., 2012; Sjöberg and Weirich, 2015; Weirich et al., 2013; vanDoorn et al., 2013; Yang et al., 2016) working on using explicit casts insteadof conversion rule in a dependently typed system. In λ∀I we adopt a simple
formulation of casts based on iso-types (Yang et al., 2016), but we believe that
more powerful notions of casts could work too.
Dependent Object Types. Dependent Object Types (DOT) (Amin et al., 2012,2014; Rompf and Amin, 2016) is another family of systems that discusses subtyping in a dependently typed setting. Unlike the traditional dependent typesystems that are based on lambda calculus, DOT embraces the idea of “everything is an object” and features the path-dependent types. The path-dependent
type is a restricted form of dependent types. Path-dependent types support
return types of functions to mention their parameters, but only member accessing operations are allowed for the “depended value”, and instead of all terms,
only variable names can occur in the accessing path. This restriction rules out
traditional problems in dependent type systems like handling type-level computation, and allows DOT to focus more on the subtyping aspect like reasoning
about type bounds. Also, thanks to this restriction, DOT can more easily separate the concept of terms and types unlike conventional dependent type systems.
Therefore, the mutual dependency of typing and subtyping is also not an issue
for DOT.
DOT with Implicit Functions (DIF) (Jeffery, 2019) is an interesting extension of DOT that adds implicit functions. Since path-dependent types can
encode parametric polymorphism, adding implicit functions implies adding implicit polymorphism. The treatment of implicit parameters in DIF is quite
similar to ICC (Miquel, 2001) in terms of the generalization (GEN) and instantiation (INST) rules shown in Section 2.2. Hence their system shares a similar
constraint of being unable to handle implicits at higher-ranked positions. However in DIF, implicit arguments are runtime relevant, and can be retrieved by aspecial variable. This comes with a restriction that implicit arguments can only
be variables in the typing context when inferred.
Refinement Types and Manifest Systems. Manifest systems (Greenberg et al.,2010) is one of the styles of contract-oriented programming (in contrast to thelatent systems (Hinze et al., 2006)), where contracts (the conditions that programmers expect to satisfy) are expressed in the type system. λH (Flanagan,
2006; Greenberg et al., 2010) is one calculus that includes dependent types andsubtyping simultaneously. The subtyping relation expresses the implication relation between contract satisfaction conditions. Unfortunately, this brings thedifficulty of potential mutual dependency between typing and subtyping. To
overcome this issue, λH builds another layer of denotational semantics on topof subtyping rules to avoid that subtyping depends on typing. However, thisintroduces other complications in their metatheory. System FH (Belo et al.,38

2011) and FσH (Sekiyama et al., 2017) provide another interesting idea to deal
with this mutual dependency. They get rid of the subtyping aspect in their
type system, but later “recover” it after the system is defined to prove the ideas
expressed by subtyping hold for their systems. Sekiyama et al. (2017) called
this technique the subsumption-free formulation. However, it is likely that suchtechnique is difficult to apply for systems that reason about implicit polymorphism, since systems like ICC (Miquel, 2001) that mentions subtyping relations
post facto often fail to reason about polymorphism at higher ranks.
Feature Comparison. Lastly we present a summary comparing λ∀I and some of
the closest related calculi in the literature in Table 1. Table 2 contains theshorthand and references for the calculi used in the comparison in Table 1. We
select the following features for the comparison:• Dependent types: Whether the system supports dependent types.
• Subtyping: Whether there is a subtyping relation in the typing rules.
The complexity of subtyping relations varies but we do not dive into details
here.
• Implicit arguments: Whether some form of implicit polymorphism is
supported. The monotype restriction on instantiation is assumed.
• Relevant arguments: Whether implicit instantiations can be runtime
relevant.
• Rank-n polymorphism: Whether polymorphic subtyping supports higherranked polymorphism.
• Mechanization: Whether the correctness of metatheory (and algorithm,
if available) is mechanically checked instead of manually.
We use ✓, if a feature is supported, × if it is not supported. The featuresof relevant (implicit) arguments and rank-n polymorphism only make sense incalculi with implicit arguments. Thus for calculi without implicit arguments we
use − to mean “does not apply”.
7. Conclusion
In this article, we presented a design of a dependently typed calculus called
λ∀
.
λ∀
I
I generalizes non-dependent polymorphic subtyping by Odersky and
Läufer (Odersky and Läufer, 1996) and contains other features like general recursion and explicit casts for type-level computations. We adopt the techniquesof the Unified Subtyping (Yang and Oliveira, 2017) to avoid the mutual dependency between typing and subtyping relation to simplify the formalization.
Besides other relevant theorems about typing and subtyping, transitivity andtype safety are proved mechanically with the Coq proof assistant.

39

Dependent types
Subtyping
Implicit arguments
Relevant arguments
Rank-n polymorphism
Mechanization

ICC
✓
×
✓
×
×
×

λI≤
✓
✓
×
✓

Zhao19
×
✓
✓
×
✓
✓

DK19
Equalitya
✓
✓
×
✓
×

DH
✓
×
✓
✓
✓
×

λ∀
I
✓
✓
✓
×
✓
✓

Table 1: Feature Comparison of calculi closely related to λ∀I.
a Only type-level equality is dependent, other parts of the system are not.

Shorthand
ICC
λI≤
Zhao19
DK19
DH
λ∀
I

Reference/Description
Implicit Calculus of Constructions (Miquel, 2001).
Unified Subtyping calculus by Yang and Oliveira (2017).
Zhao et al. (2019) mechanization of DK’s type system.
Dunfield and Krishnaswami (2019)
Dependent Haskell (Eisenberg, 2016).
Our calculus.
Table 2: Description of the calculi in Table 1.

In the future, we will attempt to lift various restrictions that originally simplify the metatheory, such as the kind restriction on polymorphic types and theruntime irrelevance of implicit arguments. We would also like to study the impact to the metatheory of adding ⊺ types to our language, which is a common
feature of a subtyping relation. Most importantly, we consider the developmentof a well-specified algorithmic system a major challenge in our future work. The
current formulation of λ∀I is declarative due to the mono-expression guesses.
While λ∀
still
has
some
limitations, we believe that it already includes manyIof the core features that are important for typed functional languages. Assuming that we have an implementation of a core language based on λ∀I , weexpect that interesting and expressive functional languages can be built on
top of such core language. For instance, all the features of Haskell 98, including higher-kinds, algebraic datatypes and type classes (Kaes, 1988; Wadler
and Blott, 1989) should be easily encodable in λ∀I . Furthermore, some features not in Haskell 98, but available in modern versions of GHC Haskell, suchas higher-ranked polymorphism or certain kinds of dependent types are also
supported in λ∀I . GADTs (Cheney and Hinze, 2003; Xi et al., 2003) and typefamilies (Chakravarty et al., 2005) are more challenging as they require a more
powerful form of casts and additional support for equality. Previous work on
PITS has shown how some forms of GADTs and equality can be modelled using
a variant of cast operators that employ a more powerful parallel reduction relation. We believe that λ∀I can also employ such variant of casts, although thisalso remains future work.

40

Acknowledgements
We are grateful to anonymous reviewers that helped improving the presentation of our work. This work has been sponsored by Hong Kong Research Grant
Council projects number 17209519 and 17209520.
References
R. Hindley, The principal type-scheme of an object in combinatory logic, Transactions of the American Mathematical Society 146 (1969) 29–60.
R. Milner, A theory of type polymorphism in programming, Journal of computerand system sciences 17 (1978) 348–375.
L. Damas, R. Milner, Principal type-schemes for functional programs, in: POPL
’82, 1982.
M. Odersky, K. Läufer, Putting type annotations to work, in: POPL ’96, 1996.
S. Peyton Jones, D. Vytiniotis, S. Weirich, M. Shields, Practical type inference
for arbitrary-rank types, Journal of functional programming 17 (2007) 1–82.
J. Dunfield, N. R. Krishnaswami, Complete and easy bidirectional typechecking
for higher-rank polymorphism, in: ICFP ’13, 2013.
P. Freeman, PureScript, 2017. URL: http://www.purescript.org/.
Disciple Development Team, The Disciplined Disciple Compiler, 2017. URL:
http://disciple.ouroborus.net/.
J. Zhao, B. C. d. S. Oliveira, T. Schrijvers, A mechanical formalization ofhigher-ranked polymorphic type inference, in: ICFP ’19, 2019.
T. Coquand, G. Huet, The calculus of constructions, Information and Computation 76 (1988) 95–120.
L. Augustsson, Cayenne — A language with dependent types, in: ICFP ’98,
ACM, 1998, pp. 239–250.
T. Altenkirch, N. A. Danielsson, A. Löh, N. Oury, ΠΣ: Dependent types without
the sugar, in: Functional and Logic Programming, Springer, 2010, pp. 40–55.
V. Sjöberg, C. Casinghino, K. Y. Ahn, N. Collins, H. D. E. III, P. Fu, G. Kimmell, T. Sheard, A. Stump, S. Weirich, Irrelevance, heterogenous equality,
and call-by-value dependent type systems, in: MSFP ’12, 2012, pp. 112–162.
A. Stump, M. Deters, A. Petcher, T. Schiller, T. Simpson, Verified programmingin Guru, in: PLPV ’09, 2008, pp. 49–58.
S. Weirich, J. Hsu, R. A. Eisenberg, System FC with explicit kind equality, in:
ICFP ’13, ACM, 2013, pp. 275–286.
41

C. Casinghino, V. Sjöberg, S. Weirich, Combining proofs and programs in adependently typed language, in: POPL ’14, ACM, 2014, pp. 33–45.
V. Sjöberg, S. Weirich, Programming up to congruence, in: POPL ’15, ACM,
2015, pp. 369–382.
U. Norell, Towards a practical programming language based on dependent typetheory, Ph.D. thesis, Chalmers University of Technology, 2007.
E. Brady, Idris, a general-purpose dependently typed programming language:
Design and implementation, Journal of Functional Programming 23 (2013)
552–593.
S. Weirich, A. Voizard, P. H. A. de Amorim, R. A. Eisenberg, A specification
for dependent types in Haskell, in: ICFP ’17, Association for Computing
Machinery, 2017.
H. Barendregt, Introduction to generalized type systems, Journal of Functional
Programming 1 (1991) 125–154.
G. Kimmell, A. Stump, H. D. E. III, P. Fu, T. Sheard, S. Weirich, C. Casinghino,
V. Sjöberg, N. Collins, K. Y. Ahn, Equational reasoning about programs withgeneral recursion and call-by-value semantics, in: PLPV ’12, 2012, pp. 15–26.
Y. Yang, X. Bi, B. C. d. S. Oliveira, Unified syntax with iso-types, in: APLAS’16, Springer, 2016, pp. 251–270.
D. Aspinall, A. Compagnoni, Subtyping dependent types, in: LICS ’96, 1996,
pp. 86–97.
Y. Yang, B. C. d. S. Oliveira, Unifying typing and subtyping, in: OOPSLA ’17,
2017.
W. D. Goldfarb, The undecidability of the second-order unification problem,
Theoretical Computer Science 13 (1981) 225–230.
A. Miquel, The implicit calculus of constructions extending pure type systems
with an intersection type binder and subtyping, in: TlCA ’01, Springer, 2001,
pp. 344–359.
B. Barras, B. Bernardo, The implicit calculus of constructions as a programming
language with dependent types, in: International Conference on Foundationsof Software Science and Computational Structures, Springer, 2008, pp. 365–
379.
Coq development team, The coq proof assistant, http://coq.inria.fr/, ????
D. Le Botlan, D. Rémy, MLF: Raising ML to the power of System F, in: ICFP
’03, 2003.

42

D. Leijen, HMF: Simple type inference for first-class polymorphism, in: ICFP
’08, 2008.
D. Vytiniotis, S. Weirich, S. Peyton Jones, FPH: First-class polymorphism for
Haskell, in: ICFP ’08, 2008.
Y. Yang, B. C. Oliveira, Pure iso-type systems, Journal of Functional Programming 29 (2019).
T. Æ. Mogensen, Efficient self-interpretation in lambda calculus, Journal of
Functional Programming (1992) 345–364.
J. Cheney, R. Hinze, First-class phantom types, Technical Report, Cornell University, 2003.
H. Xi, C. Chen, G. Chen, Guarded recursive datatype constructors, in: POPL
’03, 2003, pp. 224–235.
R. Eisenberg, Dependent Types in Haskell: Theory and Practice, Ph.D. thesis,
University of Pennsylvania, 2016.
B. C. Pierce, Types and programming languages, MIT press, 2002.
P. Wadler, S. Blott, How to make ad-hoc polymorphism less ad hoc, in: POPL
’05, 1989, pp. 60–76.
S. Kaes, Parametric overloading in polymorphic programming languages, in:
ESOP ’88, 1988, pp. 131–144.
G. J. Sussman, G. L. Steele, Scheme: A interpreter for extended lambda calculus, Higher-Order and Symbolic Computation 11 (1998) 405–439.
P. Martin-Löf, An intuitionistic theory of types, in: G. Sambin, J. M. Smith(Eds.), Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, Oxford University Press, 1998, pp. 127–172.
D. S. Hutchins, Pure subtype systems, in: POPL ’10, ACM, 2010, pp. 287–298.
J. Dunfield, N. R. Krishnaswami, Lemmas and proofs for “complete and easy
bidirectional typechecking for higher-rank polymorphism” (2013).
B. Accattoli, G. Guerrieri, Open call-by-value, in: APLAS ’16, Springer, 2016,
pp. 206–226.
D. Miller, A logic programming language with lambda-abstraction, function
variables, and simple unification, Journal of logic and computation 1 (1991a)
497–536.
D. Miller, Unification of simply typed lambda-terms as logic programming(1991b).

43

J. Reed, Higher-order constraint simplification in dependent type theory, in:
LFMTP ’09, ACM, 2009, pp. 49–56.
A. Abel, B. Pientka, Higher-order dynamic pattern unification for dependent
types and records, in: TLCA ’11, Springer, 2011, pp. 10–26.
A. Gundry, C. McBride, A tutorial implementation of dynamic pattern unification, Unpublished draft (2013).
J. Cockx, D. Devriese, F. Piessens, Unifiers as equivalences: Proof-relevant
unification of dependently typed data, in: ICFP ’16, ACM, New York, NY,
USA, 2016, pp. 270–283. doi:10.1145/2951913.2951917.
B. Ziliani, M. Sozeau, A unification algorithm for Coq featuring universe polymorphism and overloading, in: ICFP ’15, ACM, New York, NY, USA, 2015,
pp. 179–191.
C. S. Coen, Mathematical knowledge management and interactive theorem proving, Ph.D. thesis, University of Bologna, 2004. Technical Report UBLCS 20045, 2004.
U. Norell, Towards a practical programming language based on dependent typetheory, Ph.D. thesis, Chalmers University of Technology and Göteborg University, 2017.
A. Gundry, Type Inference, Haskell and Dependent Types, Ph.D. thesis, University of Strathclyde, 2013.
N. Xie, R. Eisenberg, B. C. d. S. Oliveira, Kind inference for datatypes, in:
POPL ’20, 2020.
M. M. Chakravarty, G. Keller, S. P. Jones, S. Marlow, Associated types withclass, in: POPL ’05, 2005, pp. 1–13.
C. Kiss, T. Field, S. Eisenbach, S. Peyton Jones, Higher-order type-level programming in haskell, Proc. ACM Program. Lang. (2019).
A. Serrano, J. Hage, D. Vytiniotis, S. Peyton Jones, Guarded impredicative
polymorphism, in: PLDI ’18, 2018.
J. B. Wells, Typability and type checking in System F are equivalent andundecidable, Annals of Pure and Applied Logic 98 (1999) 111–156.
J. Dunfield, N. R. Krishnaswami, Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types, in:
POPL ’19, 2019.
J. Tiuryn, P. Urzyczyn, The subtyping problem for second-order types is undecidable, 1996.
P. Chiusano, R. Bjarnason, Unison, 2015. URL: http://unisonweb.org.
44J. Zwanenburg, Pure type systems with subtyping, in: TLCA ’99, 1999, pp.
381–396.
G. Castagna, G. Chen, Dependent types with subtyping and late-bound overloading, Information and Computation 168 (2001) 1–67.
G. Chen, Subtyping calculus of construction, Mathematical Foundations ofComputer Science 1997 (1997) 189–198.
G. Chen, Coercive subtyping for the calculus of constructions, in: POPL ’03,
ACM, 2003, pp. 150–159.
B. C. Pierce, M. Steffen, Higher-order subtyping, Theoretical computer science
176 (1997) 235–282.
F. van Doorn, H. Geuvers, F. Wiedijk, Explicit convertibility proofs in puretype systems, in: LFMTP ’13, ACM, 2013, pp. 25–36.
N. Amin, A. Moors, M. Odersky, Dependent object types, in: FOOL ’12, ACM,
2012.
N. Amin, T. Rompf, M. Odersky, Foundations of path-dependent types, in:
OOPSLA ’14, ACM, 2014, pp. 233–249.
T. Rompf, N. Amin, Type soundness for dependent object types (dot), in:
OOPSLA ’16, ACM, 2016, pp. 624–641.
A. Jeffery, Dependent object types with implicit functions, in: Proceedings of
the Tenth ACM SIGPLAN Symposium on Scala, 2019, pp. 1–11.
M. Greenberg, B. C. Pierce, S. Weirich, Contracts made manifest, in: POPL
’10, 2010, pp. 353–364.
R. Hinze, J. Jeuring, A. Löh, Typed contracts for functional programming, in:International Symposium on Functional and Logic Programming, Springer,
2006, pp. 208–225.
C. Flanagan, Hybrid type checking, in: POPL ’06, 2006, pp. 245–256.
J. F. Belo, M. Greenberg, A. Igarashi, B. C. Pierce, Polymorphic contracts, in:
ESOP ’11, Springer, 2011, pp. 18–37.
T. Sekiyama, A. Igarashi, M. Greenberg, Polymorphic manifest contracts, revised and resolved, ACM Transactions on Programming Languages and Systems (TOPLAS) 39 (2017) 1–36.

45