Giving Haskell a Promotion
Brent A. Yorgey
Stephanie Weirich
University of Pennsylvania{byorgey,sweirich}@cis.upenn.edu

Julien Cretin
INRIA
julien.cretin@inria.fr

Simon Peyton Jones
Dimitrios Vytiniotis
Microsoft Research Cambridge{simonpj,dimitris}@microsoft.com

José Pedro Magalhães
Utrecht University
jpm@cs.uu.nl

Abstract
Static type systems strive to be richly expressive while still being
simple enough for programmers to use. We describe an experimentthat enriches Haskell’s kind system with two features promoted
from its type system: data types and polymorphism. The new system has a very good power-to-weight ratio: it offers a significant
improvement in expressiveness, but, by re-using concepts that programmers are already familiar with, the system is easy to understand and implement.
Categories and Subject Descriptors D.3.3 [Language Constructs
and Features]: Data types and structures, Polymorphism; F.3.3[Studies of Program Constructs]: Type structure
General Terms Languages, Design
Keywords Haskell, promotion, kinds, polymorphism

1.

Introduction

Static type systems are the world’s most successful applicationof formal methods. Types are simple enough to make sense toprogrammers; they are tractable enough to be machine-checked on
every compilation; they carry no run-time overhead; and they plucka harvest of low-hanging fruit. It makes sense, therefore, to seek tobuild on this success by making the type system more expressive
without giving up the good properties we have mentioned.
Every static type system embodies a compromise: it rejects
some “good” programs and accepts some “bad” ones. As thedependently-typed programming community knows well, the ability to express computation at the type level can improve the “fit”;
for example, we might be able to ensure that an alleged red-blacktree really has the red-black property. Recent innovations in Haskell
have been moving in exactly this direction. Notably, GADTs [24]and type families [25] turn the type system into a (modest) programming language in its own right.

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
TLDI’12, January 28, 2012, Philadelphia, PA, USA.
Copyright © 2012 ACM 978-1-4503-1120-5/12/01. . . $10.00

But, embarrassingly, type-level programming in Haskell is almost entirely untyped, because the kind system has too few kinds(?, ? → ?, and so on). Not only does this prevent the programmer
from properly expressing her intent, but stupid errors in type-level
programs simply cause type-level evaluation to get stuck rather
than properly generating an error (see §2). In addition to being too
permissive (by having too few kinds), the kind system is also too
restrictive, because it lacks polymorphism. The lack of kind polymorphism is a well-known wart; see, for example, Haskell’s family of Typeable classes (§2.5), with a separate (virtually identical)
class for each kind.
In this paper we describe a design that fixes these problems,
and we sketch its implementation in GHC, our Haskell compiler.
Our design is inspired by Conor McBride’s Strathclyde Haskell
Enhancement (SHE) preprocessor [19], which automatically promotes datatypes to be datakinds. Our work goes well beyond SHE
by also introducing kind polymorphism, and integrating these two
new features with convenient source syntax and full type (and kind)inference.
From a type-theoretic point of view, this paper has little new tosay: full-spectrum dependently typed languages like Coq [31] orAgda [23] are more expressive still. But, as we discuss in more detail in §7, these languages are in some ways too powerful: they havea high barrier to entry both for programmers (who want to write
programs in natural and straightforward ways) and implementors(who have to worry about efficiently executing these programs).
Instead, we start from the other end: we carefully extend a stateof-the-art functional programming language with features that appear in dependently-typed languages. Our primary audience is thecommunity of Designers and Implementors of Typed Languages, towhom we offer a big increase in expressive power for a very modest
cost in terms of intellectual and implementation complexity.
Specifically, our contributions are:
• We extend Haskell with a rich kind system, including kind poly-morphism. Suitable value and type constructors are automatically promoted to become type and kind constructors, respectively (we explain precisely which constructors can be liftedin §3.3). We show, by example, that these modest extensions
offer a large gain in expressiveness (§2).
• We formalize an explicitly-typed intermediate language, Sys-

tem F↑C (pronounced “FC-pro”), that embodies the new kindsystem (§3). F↑C is no toy: we have implemented it in GHC asa modest extension of GHC’s existing intermediate language,
System FC . Our extension to this intermediate language guides

our overall design—going further would require much moresignificant effort.
• GHC uses F↑C throughout its optimization phases, and each op-

timization must ensure that the transformed program is welltyped. So the metatheory of F↑C is of practical importance, especially subject reduction (§4). In addition to subject reduction
we prove progress, which ensures that coercions can be erased
at runtime without compromising type safety.

In our new system the above example is now valid Haskell!
In the declaration of Vec we can see that Nat is used as a kind.
Following SHE, we achieve this effect by automatically promoting(suitable) datatypes to become kinds; and their data constructors(Zero and Succ in this case) to become type-level data. In effectthis gives the Haskell programmer the ability to declare their own
kinds, by declaring datatypes and promoting them up a level.
These datakinds may also be used in GHC’s indexed type families (i.e. type functions). For example,• We describe the modifications to GHC’s type inference engine

type family Plus (a :: Nat) (b :: Nat) :: Nat
type instance Plus Zerob=btype instance Plus (Succ a) b
= Succ (Plus a b)(§5) and the source language extensions (§6) to support the
new features. (Haskell is a large language, so these sections arenecessarily informal.)Finally, we discuss related work (§7) as well as directions for future
research (§8).
Our goal throughout is to provide maximum gain for minimum
pain. One could go further in terms of supported features, but
we believe we have found a sweet spot. The new extensions are
fully implemented, and will soon be released as part of GHC. The
experience of GHC’s users will then inform our understanding of
possible future developments in the design space of dependentlytyped programming languages.

2.

Typed type-level programming

We begin with an informal motivation for the extensions of oursystem.
2.1

Promoting datatypes

Consider the following standard implementation of length-indexed
vectors in Haskell:data Zerodata Succ ndata Vec :: ? → ? → ? where
Nil :: Vec a ZeroCons :: a → Vec a n → Vec a (Succ n)
We declare two empty datatypes, Zero and Succ, to serve as“type-level values”, and use a generalized algebraic datatype(GADT) [24] to define a type Vec whose first argument is the typeof its elements and whose second argument is a type-level natural
number reflecting the length of its values.
However, for a language like Haskell with a strong, static typesystem, this example is rather embarrassing: it is untyped! The
type parameter to Succ has kind ?, which gives us no indicationthat we intend for it to always be a type-level representation of anatural number. The same is true of the second parameter to Vec.
Essentially, ? is serving as the single type in a “uni-typed” typesystem.1 We are not prevented from writing nonsensical types suchas Succ Bool or Vec Zero Int.
It would be much better to be able to write
data Nat = Zero | Succ Nat
data Vec :: ? → Nat → ? where
VNil :: Vec a Zero
VCons :: a → Vec a n → Vec a (Succ n)
This is the sort of thing we could write in a language with a fullspectrum dependent type system, such as Agda [23]. We have declared a normal datatype Nat, and Vec takes as its second argument
a value of type Nat. Our intention for the arguments of Vec is now
clear, and writing Vec Zero Int will rightly yield a type error.
1 Well, not quite uni-typed, because we have arrow kinds, but close.

In general, a suitable (§3.3) datatype declaration
data T = C1 T1 | C2 T2 | ...
not only defines a type constructor T and data constructors C1, C2,. . . , but also a kind T, a type constructor C1 of kind T1 → T(using the promoted kinds T and T1), and similarly for the otherconstructors.
2.2

Resolving namespaces

Although in principle a simple idea, in practice this approach leads
to an awkward naming problem for source Haskell programs, because Haskell allows type constructors and data constructors tohave the same name:data T = T Int
If we see “T” in a type, does it refer to the type T (of kind ?) or thepromoted data constructor T (of kind Int → T)? In such cases, we
adopt the following notation: plain T means the type constructor,
while 'T, with a prefixed single quote, denotes the promoted data
constructor. So the fully explicit version of the foregoing example
looks like this:data Nat = Zero | Succ Nat
data Vec :: ? → Nat → ? where
VNil :: Vec a 'Zero
VCons :: a → Vec a n → Vec a ('Succ n)
Where the promotion is unambiguous, the quote may be omitted.
We do not require (or allow) the quote notation in kinds, because there is no ambiguity to resolve. We do not allow promoting
types which are themselves indexed by a promoted data constructor(§3.3), so anything in a kind other than ? can only be a promoted
type.
2.3

Kind polymorphism for promoted types

We also allow promoting parameterized datatypes, such as lists.
For example:
data HList :: [?] → ? where
HNil :: HList '[ ]HCons :: a → HList as → HList (a : as)
Here we have declared HList, the type of heterogeneous singlylinked lists. The index of HList is a list of types which records thetypes of the elements (created by promoting the list datatype). For
example,HCons "Hi" (HCons True HNil) :: HList (String : Bool : '[ ])is a heterogeneous list containing two values of different types.
Haskell allows the syntactic sugar [a, b ] for the explicit list (a :b : [ ]), and we support the same sugar in types, thus:
HCons "Hi" (HCons True HNil) :: HList '[String, Bool]The prefix quote serves, as before, to distinguish the type-level list
from the list type in, say reverse :: [a ] → [a ].
If this promotion is to be allowed, what is the kind of thepromoted data constructor '(:)? Since the data constructor (:) is
type-polymorphic, the promoted constructor '(:) must be kindpolymorphic:'(:) :: ∀X . X → [X ] → [X ]where X is a kind variable.
We have by now seen the most significant modifications to thekind language. Haskell kinds now include the kind of types of values, written ?, other base kinds formed from promoted datatypes,
arrow kinds, and polymorphic kinds. This means that we can only
promote data constructors with types analogous to one of thesekinds. In particular, we will not promote data constructors withconstrained types (including GADTs) or higher-order type polymorphism. We return to this issue in §3.3.
2.4

and can now be used to construct recursive types indexed on kinds
other than ?. For example, here is an explicit construction of the
Vec datatype from §2.2:
data VecF (a :: ?) (f :: Nat → ?) (n :: Nat) where
VFNil :: VecF a f Zero
VFCons :: a → f n → VecF a f (Succ n)
type Vec a n = Mu (VecF a) nThis time, Mu is instantiated to ((Nat → ?) → (Nat → ?)) →(Nat → ?).
2.5

Classes can also usefully be kind-polymorphic. This allows us, forexample, to clean up Haskell’s family of Typeable classes, whichcurrently look like this:class Typeable (a :: ?) where
typeOf :: a → TypeRepclass Typeable1 (a :: ? → ?) where
typeOf1 :: ∀b. a b → TypeRep... and so on ...

Kind polymorphism for datatypes

Kind polymorphism is useful independently of promotion. Consider the following datatype declaration:
data TApp f a = MkTApp (f a)This code has always been legal Haskell, but, lacking kind polymorphism, the kind of TApp was defaulted to (? → ?) → ? → ?
[18, Section 4.6]. However, TApp is naturally kind-polymorphic;
just as we do type generalization for term definitions, we now also
do kind generalization for type definitions. The kind of TApp isthus inferred as ∀X . (X → ?) → X → ?. (Like all datatypes, theresult of TApp must still be ?.)A less contrived example is the following GADT, used to reify
proofs of type equality:
data EqRefl a b where
Refl :: EqRefl a a
The kind of EqRefl also used to default to (? → ? → ?); that
is, EqRefl could only express equality between types of values.
To express equality between type constructors, such as Maybe,required tediously declaring a separate EqRefl-like datatype foreach kind, with the only difference being kind annotations on
EqRefl’s type parameters. However, EqRefl is now inferred to havethe polymorphic kind ∀X . X → X → ?, so it can be usedequally well on any two types of the same kind. We also allow
the programmer to write

The lack of kind polymorphism is particularly unfortunate here;
the library has only a fixed, ad hoc, collection of Typeable classes.
With kind polymorphism we can write
class Typeable a where
typeOf :: Proxy a → TypeRep
We have generalized in two ways here. First, Typeable gets apolymorphic kind: Typeable :: ∀X . X → Constraint3 , so that it
can be used for types of any kind. Second, we need some way togeneralize the argument of typeOf , which we have done via a polykinded data type Proxy:data Proxy a = Proxy
The idea is that, say typeOf (Proxy :: Proxy Int) will return thetype representation for Int, while typeOf (Proxy :: Proxy Maybe)
will do the same for Maybe. The proxy argument carries noinformation—the type has only one, nullary constructor—and is
only present so that the programmer can express the type at which
to invoke typeOf . Because there are no constraints on the kind ofa, it is safe to assign Proxy the polymorphic kind ∀X . X → ?.
The user is allowed to provide instances of the class Typeable
for specific kind and type instantiations, such as:
instance Typeable Int where
typeOf = ... -- some representation for Int
instance Typeable Maybe where
typeOf = ... -- some representation for Maybe

data EqRefl (a :: X ) (b :: X ) where
Refl :: ∀X . ∀(a :: X ). EqRefl a aif they wish to indicate the kind polymorphism explicitly.
A final example of a datatype definition that benefits from kindpolymorphism is a higher-kinded fixpoint operator [21]data Mu f a = Roll (f (Mu f ) a).
Mu can be used to explicitly construct polymorphic recursive types
from their underlying functors2 ; for instance:data ListF f a = Nil | Cons a (f a)type List a = Mu ListF a
Previously, the kind of Mu would have been defaulted to ((? →?) → (? → ?)) → (? → ?); with the addition of kind polymorphism, Mu is given the polymorphic kind
Mu :: ∀X . ((X → ?) → (X → ?)) → (X → ?)Kind polymorphism for classes

Even though the class declaration is kind polymorphic, the instances need not be.
2.6

Kind polymorphism for terms

So far, we have given examples of types with polymorphic kinds.
It is also useful to have terms whose types involve kind polymorphism. We have already seen several, since data constructors ofkind-polymorphic data types have kind-polymorphic types, thus:
Proxy :: ∀X . ∀(a :: X ). Proxy a
Refl :: ∀X . ∀(a :: X ). EqRefl a a
Here is a more substantial example, taken from McBride [20].
Consider, first, the type constructor ( :→) defined as follows:

2 The cognoscenti will know that lists can be expressed with a simpler, first-

3 The Constraint kind is a new base kind introduced to classify the types

order fixpoint operator. We use a higher-kinded one here because it can also
handle an indexed type such as Vec.

of evidence terms, such as type class dictionaries—more about this featurein §3.

type s :→ t = ∀i. s i → t i
If s, t :: κ → ? are type constructors indexed by types of kind κ,then s :→ t is the type of index-preserving functions from s to t.
For example, consider the function vdup which duplicates eachelement of a length-indexed vector, guaranteeing to preserve thelength of the vector:
vdup :: Vec a n→ Vec (a, a) n
vdup VNil= VNilvdup (VCons a as) = VCons (a, a) (vdup as)
Using the type synonym above, vdup’s type can be rewritten as
vdup :: Vec a :→ Vec (a, a).
McBride observes that it is possible (and useful) to define functors that lift index-preserving functions (like vdup) from one indexed set (such as Vec a n) to another (such as square matrices
Vec (Vec a n) n). He introduces the notion of an indexed functor
class IFunctor f whereimap :: (s :→ t) → (f s :→ f t)
and goes on to present several interesting instances of this class.
Now, what are the kinds of s, t, and f ? A bit of thinking (orsimply running GHC’s type checker) reveals that there must be
kinds X1 and X2 such that s, t, and f have the kindss, t :: X1 → ?
f :: (X1 → ?) → (X2 → ?)All three are mentioned in the type of imap, which ought to bepolymorphic over X1 and X2 . The full type of imap must thereforebe∀X1 X2 . ∀f :: (X1 → ?) → (X2 → ?). ∀s, t :: X1 → ?.
IFunctor f ⇒ (s :→ t) → (f s :→ f t).
Note that this type involves two different sorts of ∀ abstractions: thefirst abstracts over the kinds X1 and X2 , whereas the others abstractover the type constructors s, t, and f .
As an aside, this example highlights an interesting difference
between F↑C and SHE [19], which restricts the kind of f to
f :: ('a → ?) → ('b → ?).
That is, using SHE, f can only transform types indexed by somepromoted kinds, whereas in our implementation f can transform
types indexed by arbitrary kinds. This is certainly no failing ofSHE, which places this restriction on kind polymorphism for thesensible reason that promoted kinds can all be “erased” to ?, andas a textual preprocessor SHE cannot be expected to do much else.
However, this does show one of the advantages of a natively implemented, strongly typed implementation over a textual preprocessor.
2.7

Kind-indexed type families

In GHC type families are type-indexed. With the addition of kindpolymorphism we may now write kind- and type-indexed families,
as the example below demonstrates:
type family Shape (a :: X ):: ?
type instance Shape (a :: ?)=atype instance Shape (a :: ? → X ) = Shape (a ())
The above type family is an example of arity-generic programming,
where Shape t denotes the application of the type constructor t to
as many copies of the unit type as its kind allows. This form of kindindexing allows for code reuse, since without it the programmer
would have to declare separate type families at each kind, in amanner similar to the current treatment of the Typeable class.

2.8

Summary

So far, we have demonstrated the nature of programs that can be
written with our two new features:• Automatic promotion of datatypes to be kinds and data con-structors to be types.
• Kind polymorphism, for kinds, types (including kind-indexed

type families and type classes), and terms.
The former allows us to give informative kinds to types, thereby
excluding bad programs that were previously accepted. The latter
accepts a wider class of good programs, and increases re-use, justlike type polymorphism. Both features are integrated with type andkind inference.
Our extensions not only enable programmers to write new andinteresting programs, but also help clean up existing libraries. For
instance, the HList library [13] may be entirely rewritten without
code duplication and extra type classes to track well-kindedness.
Similarly, the Scrap Your Boilerplate library [14, 15] can benefit
from the kind-polymorphic Typeable class described previously.

3.

System F↑C

In this section we present the extensions to GHC’s intermediate
language, System FC [29], that are necessary to support these newsource language features. System FC is an explicitly typed intermediate language which has simple syntax-directed typing rules and isrobust to program transformation. Through the mechanism of type
(and now kind) inference, source Haskell programs are elaborated
to well-typed System FC programs, a process that guarantees thesoundness of type inference.
This section presents the technical details of System FC and its
extensions, to provide a semantics for the new features. Because FC
is a small language, it allows us to make precise exactly what our
new design does and does not support. Moreover, System FC has astraightforward metatheory, so we can justify our design decisions
by demonstrating that our additions do not complicate reasoning
about the properties of the system (§4).
For clarity, we call the extended language of this paper SystemF↑C (pronounced “FC-pro”), reserving the name System FC for theprior version of the language.
3.1

System F↑C overview

The expression syntax of System F↑C is given in Figure 1, withthe differences from System FC highlighted. As the language is
explicitly typed, this syntax references kinds (κ) and types (τ ),which appear in Figure 3 and Figure 4.
The syntax also mentions coercions (γ), which explicitly encode type equalities arising from type family instance declarationsand GADT constructors (plus a Haskell-specific form of type generativity, newtype declarations). For example, each type family
instance declaration gives rise (through elaboration) to an equality axiom that equates the left and the right-hand side of the instance declaration. Such axioms can be composed and transformed
to form coercions between more complex types. The role of coercions is not central to this paper, so we refer the reader to related
work for more details on motivation and uses of coercions [29, 33],or the foundations of type equalities in type theory [16].
This abstract syntax of F↑C makes no mention of the quotemarks of §2.2 because the quotes are required only to resolve
ambiguity in the concrete syntax of Haskell. As a convention, we
use overline notation to stand for a list of syntactic elements, suchas the branches of a case expression p → u. Multi-substitution,such as τ [σ/a], is only well-defined when the lists have the samelength.

e, u

::=
| x
| λx: τ. e | e1 e2| Λa: κ. e | e τ| λc: τ. e | e γ| ΛX . e| eκ
| K| case e of p → u| e .γExpressions
Variables
Abstraction/application
Type abstraction/application
Coercion abstraction/application
Kind abstraction
Kind application
Data constructors
Case analysis
Castingp::=Patterns| K Y b: κ c: σ x: τqData constructor pattern

::=
| x
| K
| c

Term-level names
Term variables
Data constructors
Coercion variables and axioms

w

::=
| a
| H
| F

Type-level names
Type variables
Type constants
Type functions

bnd::= q: τ | w: κ | X: 

BindingsΓ::= ∅ | Γ, bnd

Contexts

Expression typing The typing judgement for terms is syntaxdirected and largely conventional; Figure 2 gives the typing rules
for some of the novel syntactic forms. Explicit type coercions of
the form e . γ are used to cast the type of an expression e from
τ1 to τ2 , given γ, a proof that the two types are equal. Note that
although these coercions are explicit in the intermediate language,
they have no runtime significance and are erased by GHC in a latercompilation stage.
Rule T C ASE is used to typecheck pattern matching expressions
and will be discussed in more detail in §3.2, where we address
datatypes.
ι

::=
| ?
| Constraint

Base kinds
Star
Constraint kind

κ, η

::=
| X
| ι
| κ1 → κ2| ∀X.κ| Tκ

Kinds
Kind variables
Base kinds
Arrow kinds
Kind polymorphism
Promoted type constantFigure 3. Syntax of kinds

H

::=
| T
| (→)
| (∼)

Type constants
Datatypes
Arrow
Equalityσ, τ, ϕ, ψ

::=
| a
| H
| F
| K
| ∀ a: κ. τ
| ∀X.τ
| τ1 τ2| τκ

Types
Variables
Constants
Type functions
Promoted data constructors
Polymorphic types
Kind-polymorphic types
Type application
Kind application

γ, δ

::=
| cκγ
| hτ i| sym γ| γ1 # γ2| ∀ a: κ. γ
| ∀X.γ| γ1 γ2| γκ
| γ[τ ]| γ[κ]

Coercions
Variables and Axioms
Reflexivity
Symmetry
Transitivity
Type polytype cong
Kind polytype cong
Type app cong
Kind app cong
Type instantiation
Kind instantiation

Figure 1. Syntax of expressions and contexts

System FC has three forms of abstraction, over expressions
λx: τ. e, types Λa: κ. e, and coercions λc: τ. e. Figure 1 showsthat System F↑C adds a fourth abstraction form, ΛX . e, to abstractover kinds. Correspondingly, the term language of F↑C includes
four forms of application, for expressions, coercions, types, andkinds. In order to make sure that all subtleties of the semantics areclearly exposed, we choose not to merge the four abstraction forms
into one (and similarly applications), as is customary in pure typesystems [2]; they are, however, combined in our implementation.
Γ `tm e : τΓ `tm e : τ1 Γ `co γ : τ1 ∼ τ2
Γ `tm e . γ : τ2
Γ, X:  `tm e : τΓ `tm ΛX . e : ∀ X . τ

T C AST

T KA BSΓ `tm e : ∀ X . τ Γ `k κ : Γ `tm e κ : τ [κ/X ]T KA PPΓ `tm e : T κ σ
for each
Kj : ∀X . ∀a:κj . ∀Yj . ∀bj :ηj . ψj → ϕj → (T X a) ∈ Γ0
ηj0 = ηj [κ/X ]
ψj0 = ψj κ/X [σ/a]
ϕ0j = ϕj κ/X [σ/a]Γ, Xj : , bj : ηj , cj : ψj0 , xj : ϕ0j `tm uj : τΓ `tm case e of Kj Yj bj : ηj0 cj : ψj0 xj : ϕ0j → uj : τ

Figure 2. Typing rules (selected)| nthi γ

Nth argument projection

Figure 4. Syntax of types and coercions

T C ASE

Kinds The syntax of kinds of F↑C is given in Figure 3. In addition to the familiar ? and κ1 → κ2 kinds, the syntax introduceskind variables X and polymorphic kinds ∀ X . κ. The kind wellformedness rules are given in Figure 5. Kinds are uni-typed in thesense that there exists only one sort of kinds: . Two more notablesyntactic forms of kinds are included in F↑C :• Applications of promoted datatypes (§2), of the form T κ. We

discuss the details of this mechanism in §3.3.

Γ `k κ : Γ `co γ : τKind validity
X:  ∈ ΓΓ `k X : Γ `k ι : 

KV BASEΓ, X:  `k κ : Γ `k ∀ X . κ : 

KV A RRKV A BSΓ `k κ1 :  .. Γ `k κn : ∅ `ty T : ?n → ?
Γ `k T κ : Γ `ty τ : κ

c: ∀X . ∀a:η. (τ1 ∼ τ2 ) ∈ Γ
for each γi ∈ γ,Γ `co γi : σi ∼ ϕi
Γ ` σi , ϕi : (ηi [κ/X ])Γ `co c κ γ : (τ1 κ/X [σ/a]) ∼ (τ2 κ/X [ϕ/a])KV VARΓ `k κ1 :  Γ `k κ2 : Γ `k κ1 → κ2 : 

KV L IFTκK L IFTΓ `k κ :  Γ, a: κ `ty τ : ιΓ `ty ∀ a: κ. τ : ι

K A BSΓ `ty τ1 : κ1 → κ2 Γ `ty τ2 : κ1
Γ `ty τ1 τ2 : κ2
Γ, X:  `ty τ : ιΓ `ty ∀ X . τ : ι

K A PPK KA BSC S YMΓ `co γ1 : τ1 ∼ τ2 Γ `co γ2 : τ2 ∼ τ3
Γ `co γ1 # γ2 : τ1 ∼ τ3

Γ, X:  ` τ1 , τ2 : ιΓ, X:  `co γ : τ1 ∼ τ2
Γ `co ∀ X . γ : ∀ X . τ1 ∼ ∀ X . τ2

C T RANSC TA BSC KA BSΓ ` σ1 , σ2 : κ1 → κ2 Γ ` τ1 , τ2 : κ1Γ `co γ1 : σ1 ∼ σ2 Γ `co γ2 : τ1 ∼ τ2
Γ `co γ1 γ2 : σ1 τ1 ∼ σ2 τ2Γ ` τ1 , τ 2 : ∀ X . κ 0Γ `co γ : τ1 ∼ τ2 Γ `k κ : Γ `co γ κ : τ1 κ ∼ τ2 κ

K KA PPΓ `co γ : ∀ a: κ. τ1 ∼ ∀ a: κ. τ2 Γ `ty σ : κΓ `co γ[σ] : τ1 [σ/a] ∼ τ2 [σ/a]Γ `ty τ1 : ι1 Γ `ty τ2 : ι2Γ `ty τ1 → τ2 : ι2

K A RRTΓ `co γ : ∀ X . τ1 ∼ ∀ X . τ2 Γ `k κ : Γ `co γ[κ] : τ1 [κ/X ] ∼ τ2 [κ/X ]Γ `co γ : H κ τ ∼ H κ τ 0

K EQ

Figure 5. Formation rules for kinds and types

Γ `co nthj γ : τj ∼ τj0

C A PPC KA PPΓ `ty τ : ∀ X . κ Γ `k κ1 : Γ `ty τ κ1 : κ[κ1 /X ]`ΓΓ `ty (∼) : ∀ X . X → X → ConstraintC VAR A X

C R EFLΓ, a: κ ` τ1 , τ2 : ιΓ, a: κ `co γ : τ1 ∼ τ2
Γ `co ∀ a: κ. γ : ∀ a: κ. τ1 ∼ ∀ a: κ. τ2

K VAR` Γ K: τ ∈ Γ ∅ ` τΓ `ty K : κΓ `ty τ : κΓ `co hτ i : τ ∼ τΓ `co γ : τ1 ∼ τ2
Γ `co sym γ : τ2 ∼ τ1

Kinding` Γ w: κ ∈ ΓΓ `ty w : κ

Coercion typing

C TI NSTC KI NSTC N TH

Figure 6. Formation rules for coercions

The kind well-formedness rules in Figure 5 ensure that kinds are
first-order, in the sense that we do not include any kind operators.
In other words, Maybe by itself is not a kind, although Maybe ? is,and there are no classifiers for kind variables other than .

actually formed from the application of the constant (∼) to a kindand two type arguments of that kind. In FC , this equality constraint
was a special form, but the addition of polymorphic kinds meansthat it can be internalized and treated just like any other type
constructor. To keep the syntactic overhead low, we continue to use
the notation τ1 ∼ τ2 to stand for the application (∼) κ τ1 τ2 when
the kind is unimportant or clear from the context.
Another minor point is the use of ι to classify the base kinds
in rules K A BS and K KA BS (Figure 5). A conventional system
would require that a type ∀a.τ has kind ?, but in our system it
can have either kind ? or Constraint, because both classify types
inhabited by values.

Types The types of F↑C are given in Figure 4, and their kinding rules appear in Figure 5. The new constructs include (i) kindpolymorphic types ∀X . τ , (ii) kind application τ κ, and (iii) promoted data constructors. Kind-polymorphic types classify kindabstractions in the expression language. The syntax τ κ applies atype constructor with a polymorphic kind to a kind argument. Thereis no explicit kind abstraction form in the type language for thesame reason that there is no explicit type abstraction form—typeinference in the presence of anonymous abstractions would require
higher-order unification.
The syntax of constants includes the equality constructor (∼),
which has the polymorphic kind ∀ X . X → X → Constraint byrule K E Q. This means that equality constraints written τ1 ∼ τ2 are

Coercions Coercions, also shown in Figure 4, are “proofs” thatprovide explicit evidence of the equality between types. The judgement Γ `co γ : τ1 ∼ τ2 expresses the fact that the coercion γ isa proof of equality between the types τ1 and τ2 . If such a derivation is possible, it is an invariant of the relation that τ1 and τ2 havethe same kind, and that kind instantiates the (∼) constructor in the
conclusion of the relation.
The coercion forms are best understood by looking at their formation rules, shown in Figure 6. Coercion variables and uses ofprimitive axioms are typed by rule C VAR A X. Recall that primitive coercion axioms may be kind-polymorphic since type family
instance declarations in source Haskell may be kind-polymorphic,
such as the last Shape instance from §2.7. When such axioms are• Another small extension of System F↑C is a special base kindConstraint [4], which classifies types representing evidence,such as type class dictionaries and type equalities. While insource Haskell such evidence is implicit, the elaboration ofa source program into F↑C constructs explicit evidence terms
whose types have kind Constraint. We use the metavariable ιto refer to an arbitrary base kind (? or Constraint).

`Γe −→ e 0Context well-formedness
GWF E MPTY`∅
`Γ X #ΓGWF S ORT
` Γ, X: (λc: τ. e) γ −→ [γ/c]eΓ `k κ :  a # Γ` Γ, a: κ

GWF T Y VAR`ΓΓ `k κ :  F # Γ` Γ, F: κ

GWF T Y F UN`Γ(Λa: κ. e) τ −→ [τ /a]e(ΛX . e) κ −→ [κ/X ]e

S CB ETAS TB ETAS KB ETA

Ki Y b: η c: ψ x: ϕ → ui ∈ p → u

S C ASEGWF T Y DATA

case Ki κ σ κ0 τ γ e ofh p →i hu −→ iui [e/x ] [γ/c] τ /b κ0 /Y

GWF VAR(v . γ) e −→ (v (e . sym (nth1 γ))) . nth2 γΓ `ty τ : κ x # Γ` Γ, x: τ(v . γ) τ −→ v τ . γ[τ ]τ = ∀X . ∀a:κ. ∀Y. ∀b:η. (σ → (T X a))` Γ Γ `ty τ : ? K # Γ` Γ, K: ττ = ∀X . ∀a:κ. (τ1 ∼ τ2 )` Γ Γ `ty τ : Constraint c # Γ` Γ, c: τ

GWF C ON

GWF A X

Figure 7. Context formation rules

used, they must be applied to kind and coercion arguments. In thisrule and elsewhere, the notation Γ ` σ, ϕ : κ ensures that bothtypes σ and ϕ have the same kind in the same context.
Coercions include rules for reflexivity, symmetry, transitivity and congruence (rules C TA BS through C KA PP). Coercions
can be destructed, through instantiation (C TI NST and C KI NST)
as well as by appealing to the injectivity of type constructors(C N TH). Notice that in rule C N TH the kinds of the two applications are required to be the same—this syntactically ensures thatcoercions are always between types of exactly the same kind.
System F↑C allows top-level definitions for datatypes T,

Contexts
type functions F, and equality axioms c. Rather than give concrete
syntax for declarations of these three constants, we instead give
formation rules for the initial context in which terms are typechecked, shown in Figure 7. The notation x # Γ indicates that x is
fresh for Γ.
Operational semantics Selected rules of the operational semantics of F↑C appear in Figure 8, including the β-reduction rules for
abstraction forms and for case expressions. The operational semantics includes crucial “push” rules, inherited from FC , which makesure that coercions do not interfere with evaluation. For example,
rule S P USH illustrates a situation where a coercion may interferewith a β-reduction. In that case γ must be a coercion between two
function types, (τ1 → τ2 ) ∼ (σ1 → σ2 ). The rule decomposes γ
into two simpler coercions and rewrites the term to expose opportunities for reduction.
3.2

S B ETA(λx: τ. e) e 0 −→ [e 0 /x ]e`Γκ = ∀X .κ → ?
` Γ Γ `k κ :  T # Γ` Γ, T: κ

One-step reduction

Kind polymorphism and datatypes

We allow datatype definitions to have polymorphic kinds. However,rule GWF T Y DATA requires all type constants to have prenex kind
quantification, 4
T: ∀X .κ → ?.
4 We use the notation ∀X . τ as an abbreviation for ∀X .∀X . . . . τ . Like1
2

wise, κ → ? abbreviates κ1 → κ2 → . . . → ?.

(v . γ) κ −→ v κ . γ[κ]S P USHS TP USH
S KP USH∅ `co γ 0 : T κ σ1 ∼ T κ σ2
K: ∀X . ∀a:κ. ∀Y. ∀b:η. (ψ1 ∼ ψ2 → ϕ → (T X a)) ∈ Γ
ih
i
h

ψ10 = ψ1 τ /b κ0 /Y κ/X
ih
i
h

ψ20 = ψ2 τ /b κ0 /Y κ/X
h
ih
i

ϕ0 = ϕ τ /b κ0 /Y κ/Xfor each γj ∈ γ,
γj0 = sym ([a7→nth γ 0 ]ψ1 j ) # γj # [a7→nth γ 0 ]ψ2 j
for each ej ∈ e,
ej0 = ej . [a7→nth γ 0 ]ϕ0j
S CP USH
case (K κ σ1 κ0 τ γ e) . γ 0 of p → u −→case K κ σ2 κ0 τ γ 0 e 0 of p → u(v . γ1 ) . γ2 −→ v . (γ1 # γ2 )S C OMB

Figure 8. Operational semantics of F↑C (selected rules)
In other words, type constants must take all of their kind arguments
before any of their type arguments. This restriction simplifies theirsemantics. For example, because type constants are injective, equations between them may be decomposed into equations between
their type arguments, as in the rule C N TH. By not allowing kindand type arguments to mix, we can write this rule succinctly.
Data constructors for kind-polymorphic datatypes must themselves be kind polymorphic (the alternative would be to allow kindequalities, just as type equalities are currently allowed for GADTs,
but we do not: see §3.4). Rule GWF C ON requires data constructors to have types of the following form:
K: ∀X . ∀a:κ. ∀Y. ∀b:η. ϕ → (T X a)
Data constructors can be polymorphic over kinds and types, allof which must show up as parameters to the datatypes that they
construct. Furthermore, data constructors can take additional kindand type arguments that do not appear in the result type, as wellas term arguments whose types may include constraints on any ofthe quantified type variables. As a result, data constructor values
carry six lists of arguments. (Above, ϕ includes both the types of
the coercion and expression arguments.)
The treatment of these six arguments shows up in the formation
rule for case expressions (T C ASE, from Figure 2), and the two
reduction rules for case expressions (S C ASE and S CP USH, from

Figure 8). These rules were already quite involved in System FC —adding kind polymorphism is a straightforward modification.
The rule T C ASE typechecks a case expression. In this rule, thelists κ and σ are the kind and type parameters to some datatype
T . These arguments replace the kind and type variables X and a,wherever they appear in the case expression. The rule then typechecks each branch of the case expression in a context extended
with the “existential” kind and type variables, as well as the coercion assumptions and constructor arguments of that branch.
The rule S C ASE describes the normal reduction of a case expression. If the scrutinee is a data constructor value, the appropriate branch is selected, after substitution of the last four arguments
carried by the data constructor value—the “existential” kinds andtypes, coercions, and expression arguments.
If there is a coercion around the data constructor value, rule
S CP USH pushes the coercion into the arguments of the data constructor. Again, the complexity of the semantics of this rule is inherited from System FC . The coercion γ 0 and expression arguments
e are each transformed by types “lifted” to coercions, using the operation [a7→nth γ]τ . This operation replaces each type variable ai
appearing in the type τ with a coercion nthi γ. We discuss thisoperation in more detail in §4. For more on the operation of thisrule, we refer readers to previous work [29, 33].
3.3

Promotion

We allow the “promotion” of certain type constructors into kinds,
and the promotion of certain data constructors to become types. But
exactly which type and data constructors are promoted, and whatkinds do the promoted data constructors have? The answers may
be found in Figure 5:• Type constructors. Rule KV L IFT states that T κ is a valid kind

only if T is a fully applied type constructor of kind ?n → ?.
• Data constructors. Rule K L IFT states that a data constructor

K may be treated as a type if K’s type τ can be promoted
to a kind κ, via the judgement ∅ ` τκ, whose rules
are given in Figure 9. The latter judgement merely replaces
type polymorphism in τ with kind polymorphism in κ, andchecks that type constructors mentioned in τ can themselves
be promoted.
The rule for promoting type constructors is deliberately restrictive.
There are many Haskell type constructors that do not have kinds ofthe form ?n → ?.
• We do not promote higher-order types of kind, say, (? → ?) →?. If we did so, we would need a richer classification of kinds
to ensure that such promoted higher-order types were applied
to appropriate arguments.
• We do not promote a type whose kind itself involves promoted

types, such as Vec : ? → Nat → ?. If we did so, the second
argument to Vec would have to be a kind classified by Nat.
In order to make this possible we would either have to allow“double promotion” (such as promoting a natural number value
all the way to the kind level), or make the type and kind levels
fully dependent. Either approach would complicate matters, so
we rule them out for now.
• We do not promote type constructors with polymorphic kinds.

If we did, we would need a system of polymorphic sorts toaccommodate the promoted kinds. At present, this seems likeextra complication for little benefit.
The guiding principle here is that kinds are not classified, or, to
put it another way, there is only one sort  in the kind validity
judgement Γ `k κ : .

Θ`τκType liftinga 7→ X ∈ Θ
L VAR
Θ`a
X
Θ ` τ1κ1 Θ ` τ2
κ2
L A RRΘ ` τ1 → τ 2
κ1 → κ2
Θ, a 7→ X ` τκΘ ` ∀ a: ? . τ∀X.κ
∅ `ty T : ?n → ? Θ ` τiΘ`TτTκ

L A BS
κin

L A PP

Figure 9. Type to kind translation

3.4

Design principle: no kind equalities!

There is one other major restriction on promoted types: we do notpromote GADTs. This limitation derives from an important designprinciple of F↑C : we do not allow equality constraints between kinds,
nor kind coercions. Since GADT data constructors take coercions
between types as arguments, their promotions would necessarily
require coercions between kinds. Disallowing kind equality constraints and coercions means that α-equivalence is the only meaningful equivalence for kinds, which dramatically simplifies the system.
The difficulty with kind constraints lies with type equivalence.
In F↑C , all nontrivial type conversions must be made explicit in thecode, through the use of coercions. Coercions simplify the metatheory of the FC language, by rendering type checking trivially decidable and separating the type soundness proof from the consistencyof the type equational theory. In the jargon of dependent type theory, FC has a trivial definitional equality (types are equal only when
α-equivalent) and an expressive propositional equality (coercions
are proofs of a much coarser equality between types.)
The presence of nontrivial kind equivalences muddies the definition of propositional equality between types. We would need togeneralize the coercion judgement to mention two types as well as
their kinds. But what should the interpretation of this judgement
be? That the types and their kinds are equal? Should we be able toextract a proof of kind equality from a proof of type equality? Sucha system would lead to bloated proofs and many additional rules.
We plan to address these issues in future work, using ideas
from Observational Type Theory [1]. But even if we are able todesign a sensible core language, there is still the issue of thecomplexity of the source language. Heterogeneous equality in Coq
and Agda is notoriously difficult for users to understand and use. By
only allowing one-level indexing, we have defined a simple, wellbehaved language for users to get started with dependently-typed
programming.

4.

Metatheory

We now turn to the formal properties of F↑C , and ultimately showthat the system enjoys subject reduction and progress under someconsistency requirements about the initial environment. We begin
with some scaffolding lemmas.
Lemma 4.1 (Kind substitution).
1. If ` Γ1 , (X: ), Γ2 and Γ1 `k κ :  then ` Γ1 , Γ2 [κ/X ].
2. If Γ1 , (X: ), Γ2 `ty τ : κ and Γ1 `k κ0 :  then Γ1 , Γ2 [κ0 /X ] `tyτ [κ0 /X ] : κ.
3. If Γ1 , (X: ), Γ2 `k η :  and Γ1 `k κ :  then Γ1 , Γ2 [κ/X ] `k
η[κ/X ] : .

The lemmas above are proved simultaneously by induction on
the height of the derivation. In each case, the induction hypothesis
asserts that all lemmas hold for derivations of smaller height. They
have to be proved simultaneously, as each of the three judgements
appeals to the other two.
Lemma 4.2 (Type substitution).
1. If ` Γ1 , (a: η), Γ2 and Γ1 `ty τ : η then ` Γ1 , Γ2 [τ /a].
2. If Γ1 , (a: η), Γ2 `ty σ : κ and Γ1 `ty τ : η then Γ1 , Γ2 [τ /a] `tyσ[τ /a] : κ.
3. If Γ1 , (a: η), Γ2 `k κ :  and Γ1 `ty τ : η then Γ1 , Γ2 [τ /a] `kκ : .
With these two lemmas, we can prove that the derived coercionsof our system are homogeneous.
Lemma 4.3 (Coercion homogeneity). If Γ `co γ : τ1 ∼ τ2 thenΓ ` τ1 , τ2 : κ for some kind κ.
As a corollary, if Γ `co γ : τ1 ∼ τ2 then Γ `ty τ1 ∼
τ2 : Constraint, since the two types have the same kind and theapplication of the (∼) constructor is possible by rule K E Q.
Moreover, coercion derivations (like type and kind derivations)are preserved by type and kind substitution.
Lemma 4.4 (Kind substitution in coercions). If Γ1 , (X: ), Γ2 `coγ : τ1 ∼ τ2 and Γ1 `k κ :  then Γ1 , Γ2 [κ/X ] `co γ[κ/X ] :τ1 [κ/X ] ∼ τ2 [κ/X ].
Lemma 4.5 (Type substitution in coercions). If Γ1 , (a: η), Γ2 `coγ : τ1 ∼ τ2 and Γ1 `ty τ : η then Γ1 , Γ2 [τ /a] `co γ[τ /a] :τ1 [τ /a] ∼ τ2 [τ /a].
We may also substitute coercions inside other coercions:Lemma 4.6 (Coercion substitution in coercion).
1. If Γ1 , (c: τ1 ∼ τ2 ), Γ2 `co γ : σ1 ∼ σ2 and Γ1 `co γ 0 : τ1 ∼
τ2 then Γ1 , Γ2 [γ 0 /c] `co γ[γ 0 /c] : σ1 ∼ σ2 .
2. If ` Γ1 , (c: τ1 ∼ τ2 ), Γ2 and Γ1 `co γ 0 : τ1 ∼ τ2 then` Γ1 , Γ2 [γ 0 /c].
3. If Γ1 , (c: τ1 ∼ τ2 ), Γ2 `ty τ : κ and Γ1 `co γ 0 : τ1 ∼ τ2 then
Γ1 , Γ2 [γ 0 /c] `ty τ : κ.
4. If Γ1 , (c: τ1 ∼ τ2 ), Γ2 `k κ :  and Γ1 , Γ2 [γ 0 /c] `k κ : .
4.1

Subject reduction

To show subject reduction, we first prove a substitution theorem forterms.
Theorem 4.7 (Substitution).
1. If Γ1 , (X: ), Γ2 `tm e:
τ and Γ1 `k κ :  then
Γ1 , Γ2 [κ/X ] `tm e[κ/X ] : τ [κ/X ].
2. If Γ1 , (a: η), Γ2 `tm e: τ and Γ1 `ty σ : η then
Γ1 , Γ2 [σ/a] `tm e[σ/a] : τ [σ/a].
3. If Γ1 , (c: σ1 ∼ σ2 ), Γ2 `tm e : τ and Γ1 `co γ : σ1 ∼ σ2then Γ1 , Γ2 [γ/c] `tm e[γ/c] : τ .
We also need a substitution lemma for terms:
Lemma 4.8 (Expression substitution). If Γ1 , (x: σ), Γ2 `tm e : τand Γ1 `tm u : σ then Γ1 , Γ2 `tm e[u/x ] : τ .
Finally, the crux of subject reduction is the so-called liftinglemma, which also has the same key role for proving subject reduction in previous work on FC . Recall the lifting operation from §3.2,
denoted [a7→γ]τ . Lifting provides a way to convert a type to a coercion by substituting its free type variables with coercions between
types of the appropriate kind. Its formal definition is straightforward.

Lemma 4.9 (Lifting). If Γ, (a: κ) `ty τ : η and Γ `co γ : τ1 ∼
τ2 with Γ ` τ1 , τ2 : κ then Γ `co [a7→γ]τ : τ [τ1 /a] ∼ τ [τ2 /a].
With all the scaffolding in place, we can show that evaluation
preserves types.
Theorem 4.10 (Subject reduction). Let Γ0 be the initial environment that does not contain any term, type, or kind variable bindings(we will refer to this as the top-level environment in what follows).
The following is true: if Γ0 `tm e1 : τ and e1 −→ e2 thenΓ0 `tm e2 : τ .
4.2

Progress

Despite the tedious scaffolding lemmas, subject reduction is not
hard conceptually, since each evaluation rule constructs proof terms
which justify the typeability of the reduct.
Progress, on the other hand, is more interesting: the formal operational semantics of F↑C involves coercions and pushing coercions
in terms, and we must make sure that these coercions do not stand in
the way of ordinary β-reductions. If coercions could prevent some
reductions, that would contradict our claim that coercions can besafely and entirely erased at runtime. The coercion erasure of a“safe” stuck F↑C term could lead to a crashing program.
Intuitively, for progress to hold we must impose the restrictionthat if a coercion coerces the type of a value to another value typethen the two value types have the same runtime representation. We
formalize this condition below.
Definition 4.11 (Value type). A type τ is a value type in an environment Γ if Γ `ty τ : ι and moreover it is of the form H κ σ, or∀ a: κ. σ, or ∀ X . σ.
To prevent unsound type equalities, the initial environment containing axioms and datatypes (but no term, type, and coercion variables) should be consistent, a notion that we directly adapt fromprevious work on FC [29, 33].
Definition 4.12 (Consistency). A context Γ is consistent iff• If Γ `co γ : H κ σ ∼ τ , and τ is a value type, then τ = H κ ϕ.
• If Γ `co γ : (∀ a: κ. σ) ∼ τ , and τ is a value type, thenτ = ∀ a: κ. ϕ.
:
τ = ∀ X . ϕ.

• If Γ `co γ(∀ X . σ) ∼ τ , and τ is a value type, thenUnder the assumption of consistency for the top-level definitions we can state and prove progress.
Theorem 4.13 (Progress). If Γ0 `tm e : τ and Γ0 is a top-levelconsistent environment, then either e is a value possibly wrappedin casts, or e −→ e 0 for some e 0 .
As defined above, consistency is a property not only of theinitial environment but also of the coercion formation judgement. It
is therefore not easy to check. For this reason, previous work [33]gives sufficient conditions exclusively on the top-level environment
which guarantee consistency (for a similar but simpler coercion
language). These conditions can be adapted in a straightforward
way here—the only interesting bit is that type family axioms now
involve type and kind arguments and both forms of arguments haveto be taken into account when checking the overlap of these axioms.
We finally remark that unsound equalities such as Int∼Bool
can be derived by terms, since Int∼Bool is just a type, so one
may wonder how type safety can possibly hold. For instance, thefollowing is valid F↑C code:
f :: (Int∼Bool)f =⊥Fortunately, such terms do not pose any danger to type safety,
because the syntax prevents us from injecting ordinary terms intothe universe of coercions and using them to erroneously cast thetypes of other expressions.

5.

Surface language and elaboration

When extending Haskell’s surface syntax to expose the new features to users, we found two major issues that needed to be addressed. First, a new mechanism for namespace resolution wasneeded; second, we had to decide when and to what degree kind
generalization should be performed.
5.1

Namespace resolution

As we saw in §2.2, type and data constructors have separate namespaces, so that type constructors and data constructors can be given
the same name. This practice is common in Haskell programs, starting with Prelude declarations such as (, ) and [ ]. However, whendata constructors can appear in types, it is no longer clear whatnamespace should be used to resolve type constants. SHE explored
one solution to this problem: it requires all promoted data constructors and kinds to be surrounded by curly braces.
data Vec :: ? → {Nat} → ? where
VNil :: Vec a {Z}VCons :: a → Vec a {n } → Vec a {S n }Note that curly braces can surround type expressions, not justdata constructors, as in {S n } above. Such notation is useful for
expressions with multiply lifted components. However, in SHE,
type variables with promoted kinds must also be lifted, meaningthat SHE is based on lifting values rather than just constructors.
In contrast, we separate the issue of namespace resolution fromthat of semantics by adopting the single quote mechanism. Each(ambiguous) data constructor must be marked. We find that thisnotation is easier to specify, as the treatment of type variables iscompletely standard. Furthermore, because quotes can often be
omitted, it is also visually lighter.
5.2

Kind generalization

The second issue that we needed to address in the source language
extension was the specification of where kind generalization should
occur, and how it should interact with type and kind annotations andlexically scoped type (and now kind) variables.
In general, our extension tries to be consistent with the existingtreatment of type polymorphism. Kind variables are generalized
at the same places that type variables are, and kind variables canbe brought into scope using annotations just like type variables.
Furthermore, kind variables that appear in type argument signaturesare quantified. For example, the declaration of T below is valid, andthe kind of T is inferred to be ∀X . (X → ?) → X → ?.
data T (a :: X → ?) b = K (a b)
In the same way, kind polymorphism can be explicitly specified
in class declarations. For example, the definition of IFunctor in§2.6 is accepted just as it appears there, but the programmer may
also write this more explicit definition:

are less fully tested. The changes required to the compiler, althoughwidespread, were surprisingly modest. We briefly summarize them
here. To understand this explanation it may help to recall that
GHC’s type inference engine elaborates input terms by filling in
implicit type and kind abstractions and applications, so that theterms can subsequently be desugared into F↑C .
6.1

We extended GHC’s Core language to support kind polymorphism,
which was mostly straightforward. The only awkward point wasthat we often abstract a term over a set of type variables whoseorder used to be immaterial. Now we need to abstract over typeand kind variables, and we must ensure that the kind variables comefirst, because they may appear in the kinds of the type variables.
6.2

6.

Implementation

We have a preliminary implementation of our system ready forrelease with GHC version 7.4. This initial release includes a solid
implementation of F↑C in the Core language; the source-language
features, and the kind inference that supports them, mostly work but

Type inference for terms

The type inference engine needed to be extended in two main ways:• When instantiating the type of a kind-polymorphic function, say

f :: ∀ X . ∀ a: X . τ we must instantiate a fresh unification kindvariable for X , and a fresh unification type variable for a, with
an appropriate kind.
• When unifying a type variable with a type we must unify its

kind with the kind of the type.
All kind unifications are solved on the fly by the usual sideeffecting unification algorithm, and do not generate evidence. In
contrast, type equalities are often gathered as constraints to besolved later, and are witnessed by evidence in the form of coercion
terms [26]. Not having to do this step for kind equalities rests on
the design principle discussed in §3.4.
6.3

Kind inference for types

GHC allows the user to write type signatures, such as
f :: Typeable a ⇒ [Proxy a ] → TypeRep
When elaborating this type signature, the inference engine performs kind generalization of the type, yielding the F↑C typef : ∀X . ∀a : X . Typeable X a → [Proxy X a ] → TypeRep
Type declarations themselves are a little more complex. Consider
data T f a = MkT (S a f ) | TL (f a)data S b g = MkS (T g b)
These two mutually recursive definitions must be kind checked
together. Indeed the situation is precisely analogous to the wellstudied problem of type inference for mutually recursive term definitions.
• We sort the type declarations into strongly connected compo-

nents, and kind check them in dependency order.
• A type constructor can be used only monomorphically within

its mutually recursive group.
• Type inference assigns each type constructor a kind variable,

then walks over the definitions, generating and solving kindconstraints.

class IFunctor (f :: (X1 → ?) → X2 → ?) whereimap :: ∀(s, t :: X1 → ?). (s :→ t) → (f s :→ f t)
The first line brings the kind variables X1 and X2 into scope, alongwith the type variable f ; all are then mentioned in the type of imap.

The Core language• Finally, the kind of each constructor in the group is generalized.

Class declarations are handled in the same way. There is nothing
new here—it all works in precisely the same way as for terms—so
we omit a precise account.

7.

Related work

Promoting data types The starting point for this work has been
Conor McBride’s Strathclyde Haskell Enhancement preproces-sor [19], which, among other features, allows users to promote
datatypes to be used in the type language. Throughout this paper,
we have already discussed several points of both similarity anddifference between our work and SHE.
The language extensions we describe here are most closely
related to the LX calculus [6] and the Ωmega language [27, 28].
These languages also allow the definition of datakinds and typelevel functions over datatypes. Like both of these systems, GHC
maintains a phase separation: terms can depend on types, but notvice versa. In terms of expressiveness, F↑C is very similar to LX:
F↑C includes kind polymorphism and does not require termination
proofs for type-level computation, but lacks anonymous functions
at the type-level. However, F↑C is less expressive than Ωmega, whichallows GADT programming at the type level. Because datakinds
may be indexed, Ωmega also allows the definition of datatypes in
the kind language. In fact, Ωmega has a hierarchy of levels (types,
kinds, superkinds, etc.) where each level includes datatypes that canbe indexed by elements from any of the higher levels. All datatypedefinitions are “level-polymorphic”, meaning that they can be used
at any level. On the other hand, Ωmega does not compile to an
explicitly typed language with evidence terms, and LX does notinclude explicit evidence for type equalities. This makes it harderin those languages to reason about type safety, robustness undertransformations, and the soundness of type and kind inference. In
F↑C many of the restrictions in our design (such as no evidencebased kind-equalities) are motivated by our desire to keep the
explicitly typed intermediate language simple.
Our extension does not add full-spectrum dependency to Haskell.
It merely makes the phase distinction less distinct. Full-spectrum
languages actually allow program expressions to invade the typesystem, but in the presence of nontermination or other effects, often limit those expressions to a subset with a trivial definition ofequality. For example, the Aura programming language [12] andLicata and Harper’s Positive Dependent Types [17] only allow dependency on values of positive types (such as datatypes formed
from strict products and sums). Alternatively, the F∗ language [30]allows dependency for all values, but mandates a trivial definitionof equality for functions. In contrast, promotion is more similar tothe duplication described above. Although Haskell datatypes are
nonstrict, we do not promote values, only the constructors used toform them.
Agda takes the promotion idea one step further with its experimental support for universe polymorphism5 . In Agda, all definitions(including datatypes) may be polymorphic over their level. Functions that work with such datatypes may also be level polymorphic,so the same function can be used both at runtime and for type-levelcomputation. This extension is much more sophisticated than thesimple form of promotion that we describe here, and its interactions with the rest of the type system are not yet well understood.
Kind polymorphism Kind polymorphism is an often requested
feature for Haskell in its own right. In fact, the Utrecht Haskell
Compiler (UHC)6 [7] already supports kind polymorphism. In particular, unknown kinds of type constructors do not default to kind?, but are instead generalized. The particular motivation for this addition to UHC seems to be the ability to define a kind-polymorphic
Leibniz equality datatype:
data Eq a b = Eq (∀f . f a → f b)
However, UHC does not compile to a typed intermediate language
like System F↑C .

Kind polymorphism has also been added to typed intermediate
languages, even when the source language did not include kindpolymorphism. Trifonov et al. [32] found that the addition of kindpolymorphism to the FLINT/ML compiler allowed it to be fullyreflexive. In other words, they were able to extend their typeanalyzing operations so that they are applicable to the type of any
runtime value in the language.
More formally, the properties of a polymorphic lambda calculus
with kind polymorphism were studied by Girard [8]. Girard showedthat this calculus can encode a variant of the Burali-Forti paradox
and is thus inappropriate for use as a constructive logic. This proofof “Girard’s paradox” is described in detail by Barendregt [2].
Hurkens later simplified this paradox [11]. It is not clear whether
this result holds for our system, since we do not directly allow
function abstraction at the type or kind levels. However, even if
it did, it would result in a non-normalizing term, which Haskell
already has in abundance.
Kind-indexed type families The idea of allowing type functions
to dispatch on kinds is a fairly novel component of this extension.
Work by Morrisett et al. on intensional type analysis [9] included
an operator that dispatched on types, but not kinds. Indeed, theextension of that work by Trifonov et al. [32] relied on the factthat kind polymorphism was parametric. In System FC , we haveseparated the soundness of the language from the decidability oftype checking [33].
Although we do not yet have many motivating examples of
the use of kind-indexed type families, we still believe that they
have great potential. For example, we can use them to define thepolykinded-types [10] found in Generic Haskell. System F↑C cannot
yet write the polytypic functions that inhabit such types, but weplan to further extend the language with such support (see §8.5).
Why not full-spectrum dependent types? One might well ask:
why not just use, say, Agda [23] or Coq [3]? What benefit is there in
adding dependent type features to Haskell without going all the way
to a full-spectrum dependently typed language? We see a numberof advantages of our evolutionary approach:• Type inference. Haskell enjoys robust type inference, even for

top-level terms. Adding full dependent types would severelycomplicate matters at best. Promotion, however, requires only
slight enhancements to existing inference mechanisms (§5).
• Phase distinction. Since Haskell types never actually dependon terms and vice versa, types can be safely erased before
runtime. This is still true for promoted values. Erasure analysis
for full-spectrum languages, on the other hand, is an active areaof research.
• Explicit, strongly typed evidence. This allows us to be cer-tain that type and kind inference is sound and does not accept
programs that may crash at runtime.
• Simple type checking. System FC , into which GHC desugars

Haskell source code, enjoys a simple, linear-time type checking
algorithm, guided by the presence of explicit coercion terms.
This remains true for our promoted variant. Type checking thecore language for a full-spectrum dependently typed intermediate language, on the other hand, must take into account a more
complex equivalence on types which includes β-equivalence.
• Optimization. Thanks again to the presence of explicit coer-cion terms, Haskell’s core language can be aggressively optimized while remaining statically typed.
• Familiarity. Many programmers are already familiar with

5 http://wiki.portal.chalmers.se/agda/agda.php?n=Main.

UniversePolymorphism
6 http://www.cs.uu.nl/wiki/UHC

Haskell, and it enjoys a large collection of existing libraries
and tools. Modest, backwards-compatible extensions will be
adopted in ways that major, breaking changes cannot.

8.

Future work

been simplicity. We wanted to make sure we have all the details
solidly in place before introducing any complications. There are,however, several further directions we would like to explore.

kinds, we now have type families which are “naturally” closed. For
example, given a type family Foo with two clauses, Foo Zero = ...
and Foo (Succ n) = ..., it is impossible to add any more wellkinded clauses without overlap. Could the compiler somehow takeadvantage of this knowledge?

8.1

8.5

One of the main driving forces behind the current design of F↑C has

Promoting functions

If we can promote (some) term-level data constructors to type
constructors, why not promote (some) term-level functions to typelevel functions? We have not done so yet because we already havea carefully-limited way to define type-level functions, and it seems
awkward to specify exactly which term-level functions should bepromoted. However, the resulting code duplication is irksome, andthere is no difficulty in principle, so we expect to revisit this topic
in the light of experience.
8.2

Generating singleton types

When using promoted types as indices, one quickly comes to desire
the ability to do case analysis on them. Of course, this is not directly
possible, since types are erased before runtime. A well-known technique for overcoming this limitation is the use of singleton types,
which allow doing case analysis on value-level representatives inlieu of types (the survey article on programming in Ωmega [28] offers an excellent introduction to this technique). We would like to
avoid this additional source of code duplication by automaticallygenerating singleton types from datatype declarations.
For instance, consider implementing a function replicate,
which creates a Vec of a certain (statically determined) length.
This can be accomplished with the help of singleton type SNat:
data SNat :: Nat → ? where
SZero :: SNat Zero
SSucc :: SNat n → SNat (Succ n)
replicate :: SNat n → a → Vec a n
replicate SZero= VNilreplicate (SSucc n) x = VCons x (replicate n x )Automatically generating singleton types is not hard [19, 22]. Moreinteresting would be the design of convenient surface syntax tocompletely hide their use, so users could just “pattern match on
types”.
8.3

Promoting primitive datatypes

Another useful extension would be the promotion of primitive
built-in datatypes, such as integers, characters, and strings. For
instance, having promoted string literals as types would allow us togo well beyond heterogeneous type-level lists to type-level records,
as in the Ur programming language [5].
There are no implementation or theoretical difficulties with simply promoting primitive datatypes. However, our implementation
does not yet promote primitive datatypes because, to make this feature truly usable, we would also like to promote primitive operations on these datatypes (such as integer addition or string concatenation) and integrate these operations with type inference andevidence generation. Some promising work in this direction is Diatchki’s recent addition of type-level naturals to GHC.7
8.4

Closed type families

Type families, as currently implemented in GHC, are open [25]: itis always possible to add more clauses to a type family definition at
any time, as long as they do not overlap with existing clauses. In aworld where the only base kind is ?, this makes sense, since ? itself
is open. However, with the ability to promote closed datatypes to
7 http://hackage.haskell.org/trac/ghc/wiki/TypeNats

Kind-indexed GADTs

Recall the definition of the Typeable class with a kind-polymorphic
type from §2.5:
class Typeable a where
typeOf :: Proxy a → TypeRep
Notice that typeOf ’s return type, TypeRep, does not mention a. It
would be nicer to have typed TypeReps by using GADTs whose
constructors refine types and kinds, for instance:data TypeRep (a :: κ) where
RepInt :: TypeRep Int
RepList :: (∀a. TypeRep a → TypeRep [a ]) → TypeRep [ ]Notice that RepInt must have type TypeRep ? Int in F↑C whereas
RepList returns TypeRep (? → ?) [ ]. However, supporting kindindexed GADTs is tricky. Just as GADTs currently introduce typeequalities, these kind-indexed GADTs could introduce kind equalities, an avenue that we are not prepared to take (see the discussionin §3.4).
On the other hand, there may be just enough machinery alreadyin F↑C to deal with kind-indexed GADTs in a more primitive fashion
than ordinary GADTs, by employing unifiers for kind equalities,
in the same way that GADTs used to be implemented in pre-FC
times [24]. We plan to explore this direction in the future.

Acknowledgments
Thanks to Conor McBride, Tim Sheard, the members of the Penn
PL Club, and the anonymous reviewers for many helpful and inspiring suggestions. This work was partially supported by the National
Science Foundation (NSF grants 0910500 and 1116620).

References[1] T. Altenkirch, C. McBride, and W. Swierstra. Observational equality,
now! In Proceedings of the 2007 workshop on Programming
languages meets program verification, PLPV ’07, pages 57–68, New
York, NY, USA, 2007. ACM.
[2] H. P. Barendregt. Lambda calculi with types, pages 117–309. Oxford
University Press, Inc., New York, NY, USA, 1992.
[3] Y. Bertot and P. Castéran. Interactive Theorem Proving and Program
Development. Coq’Art: The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. Springer-Verlag, 1 edition,
June 2004.
[4] M. Bolingbroke. Constraint Kinds for GHC.
http://blog.omega-prime.co.uk/?p=127.

2011.

URL

[5] A. Chlipala. Ur: statically-typed metaprogramming with type-level
record computation. SIGPLAN Not., 45:122–133, June 2010. ISSN
0362-1340.
[6] K. Crary and S. Weirich. Flexible type analysis. In Proceedings ofthe fourth ACM SIGPLAN International Conference on Functional
Programming (ICFP ’99), pages 233–248, 1999.
[7] A. Dijkstra, J. Fokker, and S. D. Swierstra. The architecture of the
Utrecht Haskell compiler. In Proceedings of the 2nd ACM SIGPLAN
symposium on Haskell, Haskell ’09, pages 93–104, New York, NY,
USA, 2009. ACM.
[8] J.-Y. Girard. Interprétation fonctionelle et élimination des coupuresde l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII,1972.

[9] R. Harper and G. Morrisett. Compiling polymorphism using
intensional type analysis. In Proceedings of the 22nd ACM SIGPLANSIGACT symposium on Principles of programming languages, POPL
’95, pages 130–141, New York, NY, USA, 1995. ACM.
[10] R. Hinze. Polytypic Values Possess Polykinded Types. In Proceedingsof the 5th International Conference on Mathematics of Program
Construction, MPC ’00, pages 2–27, London, UK, 2000. SpringerVerlag.
[11] A. J. C. Hurkens. A Simplification of Girard’s Paradox. In
Proceedings of the Second International Conference on Typed
Lambda Calculi and Applications, pages 266–278, London, UK,1995. Springer-Verlag.
[12] L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko, J. Schorr,
and S. Zdancewic. Aura: a programming language for authorization
and audit. In Proceeding of the 13th ACM SIGPLAN international
conference on Functional programming, ICFP 2008, Victoria, BC,
Canada, September 20-28, 2008, pages 27–38, 2008.
[13] O. Kiselyov, R. Lämmel, and K. Schupke. Strongly typed heterogeneous collections. In Haskell 04: Proceedings of the ACM SIGPLAN
workshop on Haskell, pages 96–107. ACM Press, 2004.
[14] R. Lämmel and S. Peyton Jones. Scrap your boilerplate: a practicaldesign pattern for generic programming. In Proceedings of the 2003
ACM SIGPLAN international workshop on Types in languages design
and implementation, TLDI ’03, pages 26–37, New York, NY, USA,2003. ACM.
[15] R. Lämmel and S. Peyton Jones. Scrap your boilerplate with class:extensible generic functions. In Proceedings of the tenth ACM
SIGPLAN international conference on Functional programming, ICFP
’05, pages 204–215, New York, NY, USA, 2005. ACM.
[16] D. Licata and R. Harper. Canonicity for 2-dimensional type theory. In
POPL ’12. To appear.
[17] D. R. Licata and R. Harper. Positively dependent types. In PLPV ’09:
Proceedings of the 3rd Workshop on Programming Languages Meets
Program Verification, pages 3–14, New York, NY, USA, 2009. ACM.
ISBN 978-1-60558-330-3.
[18] S. Marlow, editor. Haskell 2010 Language Report. 2010. URL
http://www.haskell.org/onlinereport/haskell2010/.
[19] C. McBride. The Strathclyde Haskell Enhancement. URL http://personal.cis.strath.ac.uk/~conor/pub/she/.
[20] C. McBride. Kleisli arrows of outrageous fortune. 2011. URL
http://personal.cis.strath.ac.uk/~conor/Kleisli.pdf.
[21] N. P. Mendler. Predicative type universes and primitive recursion. In
Proceedings, Sixth Annual IEEE Symposium on Logic in Computer
Science, 15-18 July, 1991, Amsterdam, The Netherlands, pages 173–
184. IEEE Computer Society, 1991.
[22] S. Monnier and D. Haguenauer. Singleton types here Singleton types
there Singleton Types Everywhere, 2009.
[23] U. Norell. Towards a practical programming language based on
dependent type theory. Chalmers University of Technology, 2007.
[24] S. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple
unification-based type inference for GADTs. In Proceedings of theeleventh ACM SIGPLAN international conference on Functional
programming, ICFP ’06, pages 50–61. ACM Press, 2006.
[25] T. Schrijvers, S. Peyton Jones, M. M. T. Chakravarty, and M. Sulzmann. Type checking with open type functions. In Proceedingof the 13th ACM SIGPLAN international conference on Functional
programming, ICFP ’08, pages 51–62. ACM Press, 2008.
[26] T. Schrijvers, S. Peyton Jones, M. Sulzmann, and D. Vytiniotis.
Complete and decidable type inference for GADTs. In Proceedingsof the 14th ACM SIGPLAN international conference on Functional
programming, ICFP ’09, pages 341–352, New York, NY, USA, 2009.
ACM.
[27] T. Sheard. Type-level Computation Using Narrowing in Omega.
Electr. Notes Theor. Comput. Sci., 174(7):105–128, 2007.
[28] T. Sheard and N. Linger. Programming in Omega. In CEFP, pages
158–227, 2007.

[29] M. Sulzmann, M. M. T. Chakravarty, S. Peyton Jones, and K. Donnelly. System F with type equality coercions. In Proceedings of the2007 ACM SIGPLAN international workshop on Types in languages
design and implementation, TLDI ’07, pages 53–66. ACM Press,
2007.
[30] N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang.
Secure distributed programming with value-dependent types. pages
266–278.
[31] The Coq Team. Coq. URL http://coq.inria.fr.
[32] V. Trifonov, B. Saha, and Z. Shao. Fully Reflexive Intensional Type
Analysis. In Fifth ACM SIGPLAN International Conference on
Functional Programming, pages 82–93. ACM Press, 2000.
[33] S. Weirich, D. Vytiniotis, S. Peyton Jones, and S. Zdancewic. Generative type abstraction and type-level computation. In Proceedings ofthe 38th annual ACM SIGPLAN-SIGACT Symposium on Principles ofprogramming languages, POPL ’11, pages 227–240, New York, NY,
USA, 2011. ACM.