A reflection on types
Simon Peyton Jones1 , Stephanie Weirich2 , Richard A. Eisenberg2 , andDimitrios Vytiniotis1
1

2

Microsoft Research, Cambridge
Department of Computer and Information Science, University of Pennsylvania

Abstract. The ability to perform type tests at runtime blurs the line
between statically-typed and dynamically-checked languages. Recent developments in Haskell’s type system allow even programs that use reflection to themselves be statically typed, using a type-indexed runtime
representation of types called TypeRep. As a result we can build dynamic
types as an ordinary, statically-typed library, on top of TypeRep in an
open-world context.

1

Preface

If there is one topic that has been a consistent theme of Phil Wadler’s research
career, it would have to be types. Types are the heart of the Curry-Howard
isomorphism, occupying the intersection of logic and practical programming. Phil
has always been fascinated by this remarkable dual role, and many of his papers
explore that idea in more detail.
One of his most seminal ideas was that of type classes, which (with his student
Steve Blott) he proposed, fully-formed, to the Haskell committee in February
1988 [WB89]. At that time we were wrestling with the apparent compromises
necessary to support equality, numerics, serialisation, and similar functions thathave type-specific, rather than type-parametric, behaviour. Type classes completely solved that collection of issues, and we enthusiastically adopted them for
Haskell [HHPJW07]. What we did not know at the time is that, far from beinga niche solution, type classes would turn out to be a seed bed from which would
spring all manner of remarkable fruit: before long we had multi-parameter typeclasses; functional dependencies; type classes over type constructors (notably
the Monad and Functor classes, more recently joined by a menagerie of Foldable,
Traversable, Applicative and many more); implicit parameters, derivable classes,
and more besides.
One particular class that we did not anticipate, although it made an early
appearance in 1990 , was Typeable. The Typeable class gives Haskell a handle onreflection: the ability to examine types at runtime and take action based on thosetests. Many languages support reflection in some form, but Haskell is moving
steadily towards an unusually statically-typed form of reflection, contradictory
though that sounds, since reflection is all about dynamic type tests. That topic
is the subject of this paper, a reflection on types in homage to Phil.

2

2

Introduction

Static types are the world’s most successful formal method. They allow programmers to specify properties of functions that are proved on every compilation.
They provide a design language that programmers can use to express much of
the architecture of their programs before they write a single line of algorithmiccode. Moreover this design language is not divorced from the code but part of it,
so it cannot be out of date. Types dramatically ease refactoring and maintenanceof old code bases.
Type systems should let you say what you mean. Weak type systems get in
the way, which in turn give types a bad name. For example, no one wants to write
a function to reverse a list of integers, and then duplicate the code to reverse alist of characters: we need polymorphism! This pattern occurs again and again,
and is the motivating force behind languages that support sophisticated typesystems, of which Haskell is a leading example.
And yet, there comes a point in every language at which the static typesystem simply cannot say what you want. As Leroy and Mauny put it “there areprogramming situations that seem to require dynamic typing in an essential way”
[LM91]. How can we introduce dynamic typing into a statically typed language
without throwing the baby out with the bathwater? In this paper we describe
how to do so in Haskell, making the following contributions:– We motivate the need for dynamic typing (Section 3), and why it needs towork in an open world of types (Section 4). Supporting an open world is areal challenge, which we tackle head on in this paper. Many other approaches
are implicitly closed-world, as Section 9 discusses.
– Dynamic typing requires a runtime test of type equality, so some structurethat represents a type—a type representation—must exist at runtime, alongwith a way to get the type representation for a value. We describe a typeindexed form of type representation, TypeRep a (Sections 5.1 and 5.2), andexplain how to use it for a type-safe dynamic type test (Section 5.3).
– We show that simply comparing type representations is not enough; in some
applications we must also safely decompose them (Section 5.4).
– Rather unexpectedly, it turns out that supporting decomposition for type
representations requires GADT-style kind equalities, a feature that has only
just been added to GHC 8.0 (Section 5.5). Type-safe reflection requires avery sophisticated type system indeed!
Our key result is a way to build open-world dynamic typing as an ordinary
statically-typed library (i.e. not as part of the trusted code base), using a verysmall (trusted) reflection API for TypeRep. We also briefly discuss our implementation (Section 6), metatheory (Section 7), and other applications (Section 8),
before concluding with a review of related work (Section 9). This paper is literate
Haskell and our examples compile under GHC 8.0.

3

3

Dynamic types in a statically typed language

Haskell’s type system is so expressive that it is remarkably hard to find a compelling application for dynamic typing. But here is one. Suppose you want towrite a Haskell library to implement the following familiar state-monad API3,4 :data ST s a-- Abstract type for state monaddata STRef s a -- Abstract type for references (to value of type a)runST:: (∀ s. ST s a) → a
newSTRef :: a → ST s (STRef s a)
readSTRef :: STRef s a → ST s awriteSTRef :: STRef s a → a → ST s ()Papers about state monads usually assume that the implementation is built
in, but what if it were not? This is not a theoretical question: actively-used
Haskell libraries, such as vault 5 face exactly this challenge. To implement ST weneed some kind of “store” that maps a key (a STRef ) to its value. This Storeshould have the following API (ignore the Typeable constraints for now):
extendStore :: Typeable a ⇒ STRef s a → a → Store → Store
lookupStore :: Typeable a ⇒ STRef s a → Store → Maybe a
It makes sense to implement the Store by a finite map, keyed by Int or someother unique key, which itself is kept inside the STRef . For that purpose, we canuse the standard Haskell type Map k v , mapping keys k to values v . But what
type should v be? As the type of extendStore declares, we must be able to insert
any type of value into the Store. This is where type Dynamic is useful:type Key = Intdata STRef s a = STR Key
type Store = Map Key Dynamic
Dynamic suffices if we have the following operations available, used to create andtake apart Dynamic values:6
toDynamic :: Typeable a ⇒ a → Dynamic
fromDynamic :: Typeable a ⇒ Dynamic → Maybe a3

There is another connection with Phil’s work here: an API like this was first proposed in “Imperative functional programming” [PJW93], a collaboration between oneof the present authors and Phil, directly inspired by Phil’s ground-breaking paper“Comprehending monads” [Wad90].
4
For our present purposes you can safely ignore the “s” type parameter; the paper“State in Haskell” explains what is going on [LPJ95].
5
https://hackage.haskell.org/package/vault
6
These types also motivate the Typeable contraint above. We discuss that constraint
further in Section 5.2, but without looking that far ahead, Phil’s insight about“theorems for free” tells us that the type fromDynamic :: Dynamic → Maybe a is
a non-starter [Wad89]. Any function with that type must return Nothing , Just ⊥, ordiverge.

4

We can now implement the functions on Store, thus:
extendStore (STR k) v s = insert k (toDynamic v ) s
lookupStore (STR k) s = case lookup k s ofJust d → fromDynamic dNothing → Nothing
In lookupStore the dynamic type check made by fromDynamic will always succeed. (That is, when looking up a STRef s a, we should always find a value oftype a.) The runtime tests compensate where the static type system is inadequate.
In summary, there are a few occasions when even a type system as sophisticated as Haskell’s is not powerful enough to give the static guarantees we seek.
A Dynamic type, equipped with toDynamic and fromDynamic, can plug the gap.

4

The challenge of an open world

Where does type Dynamic come from? One classic approach is to make Dynamica tagged union of all the types we care about, like this:data Dynamic = DInt Int| DBool Bool
| DChar Char| DPair Dynamic Dynamic...
toDynInt :: Int → Dynamic
toDynInt = DInt
fromDynInt :: Dynamic → Maybe Int
fromDynInt (DInt n) = Just n= Nothing
fromDynInt
toDynPair :: Dynamic → Dynamic → Dynamic
toDynPair = DPairdynFst :: Dynamic → Maybe Dynamic
dynFst (DPair x1 x2 ) = Just x1= NothingdynFstFor each type constructor (Int, Bool , pairs, lists, etc) we define a data constructor(e.g. DPair ) in the Dynamic type, plus a constructor function (e.g. toDynPair )and one or more destructors (e.g. dynFst, dynSnd ).
This approach has a fundamental shortcoming: it is not extensible. Concretely, what is the “...” above? The data type declaration for Dynamic can enumerate only a fixed set of type constructors (integers, booleans, pairs, etc)7 . We
call this the closed-world assumption. Sometimes a closed world is acceptable.
7

Although the set of type constructors is fixed, you can use them to build an infinite
number of types; e.g. (Int, Bool ), (Int, (Bool , Int)), etc.

5For example, if we were writing an evaluator for a small language we would need
Dynamic to have only enough data constructors to represent the types of theobject language.
But in general the world is simply not closed; it is unreasonable to extend
Dynamic, whenever the user defines a new data type! In the ST example, it isfundamental that the monad be able to store values of user-declared types.
So in this paper we focus exclusively on the challenge of open-world extensibility. Before moving on, it is worth noting that a surprisingly large fraction of theacademic literature on dynamics in a statically typed language makes a closedworld assumption (see Section 9). Moreover, even if we accept a closed world,
the approach sketched above has other difficulties, discussed in Section 9.2.

TypeRep: runtime reflection in an open world

5

We can implement an open-world Dynamic as an ordinary, type-safe Haskell library, on top of a new abstraction, that of type-indexed type representations or
TypeRep. In fact, Haskell has supported (un-type-indexed) type representations
and an open-world Dynamic for years, but in a rather unsatisfactory way (the“old design”). However, recent developments in Haskell’s type system—notably
GADTs [XCC03, PJVWW06], kind polymorphism [YWC+ 12], and kind equalities [WHE13]—have opened up new opportunities (the “new design”). A major
purpose of this paper is to motivate and describe this new design. For readersfamiliar with the old design, we compare it with the new one in Section 9.1.
5.1

Introducing TypeRep

The key to our approach is our type-indexed type representation TypeRep. But
what is a type-indexed type representation? It is best understood by example:– The representation of Int is the value of type TypeRep Int.
– The representation of Bool is the value of type TypeRep Bool .
– And so on.
That is, the index in a type-indexed type representation is itself the represented
type. TypeRep is abstract, and thus we don’t write the TypeRep value in theexamples above. Note, however, that we have said the value, not a value—there
is precisely one value of type TypeRep Int 8 . TypeRep thus defines a family of
singleton types [EW12]; indeed, TypeRep is the singleton family associated withthe kind ? of types.
As we build out the API for TypeRep, we will consider how to build an
efficient, type-safe, and open-world implementation of Dynamic. Converting toand from Dynamic should not touch the value itself; instead we represent a
dynamic value as a pair of a value and a runtime-inspectable representation of
its type. Thus:
8

Recall that ⊥ is not a value.

6

data Dynamic where
Dyn :: TypeRep a → a → Dynamic
Here we are using GADT-style syntax to declare the constructor Dyn, whose
payload includes a runtime representation of a type a and a value of type a. The
type a is existentially bound; that is, it does not appear in the result type of thedata constructor.
Now we have two challenges: where do we get the TypeRep from when creatinga Dynamic in toDynamic (Section 5.2); and what do we do with it when unpacking
it in fromDynamic (Section 5.3)?
5.2

The Typeable class

Because each type has its own TypeRep, the obvious approach is to use a typeclass, thus:class Typeable a where
typeRep :: TypeRep aThis class has only one operation, a nullary function (or simple value) that is
the type representation for the type. Now we can write toDynamic:
toDynamic :: Typeable a ⇒ a → Dynamic
toDynamic x = Dyn typeRep x
The type of the data constructor Dyn ensures that that the call of typeRep
produces a type representation for the type a. Easy!
But where do instances of Typeable come from? The magic of type classes
gives us a simple way to solve the open-world challenge, by using a single pieceof built-in compiler support: every data type declaration gives rise to a Typeable
instance for that type (Section 6). Furthermore, because Typeable and its instances are built in, we can be sure that these representations uniquely define
types; for example, the user cannot write bogus instances of Typeable that use
the same TypeRep for two different types.
5.3

Type-aware equality for TypeReps

The second challenge is to unpack dynamics. We need a function with this signature:
fromDynamic :: Typeable a ⇒ Dynamic → Maybe a
The function fromDynamic takes a Dynamic and tests whether it wraps a valueof the desired type; if so, it returns the value wrapped in Just; if not, it returns
Nothing . The Typeable constraint allows fromDynamic to know what the “desiredtype” is.

7

But how is fromDynamic implemented? Patently it must compare type representations, so we might try this:
fromDynamic :: ∀ d . Typeable d ⇒ Dynamic → Maybe d
fromDynamic (Dyn (ra :: TypeRep a) (x :: a))| rd == ra = Just x -- Eeek! Type error!
| otherwise = Nothingwhererd = typeRep :: TypeRep d
The type signatures for ra and x could be omitted, but we have put them in to remind ourselves that the types of ra and x are connected through the existentiallybound type a. The value rd is (the runtime representation of) the “desired type”,
disambiguated by a type signature. We compare rd with ra, (the representationof) x’s type, and return Just x if they match. The operational behaviour is justwhat we want, but the type checker will reject it. It has no reason to believethat x actually has type d : the type-checker surely does not understand that wehave just compared TypeReps linking up x’s type with d .
Fortunately, we have a fine tool to use whenever a runtime operation needs toinform us about types: generalised algebraic data types, or GADTs. We need anequality on TypeRep that returns a GADT; pattern-matching on the return value
gives the type-checker just the information it needs. Here are the definitions9 :eqT :: TypeRep a → TypeRep b → Maybe (a :≈: b)-- Primitive; implemented by compiler
data a :≈: b where
Refl :: a :≈: a
Here eqT returns Nothing if the two TypeReps are different, and (Just Refl ) if
they are the same. The data constructor Refl is the sole, nullary data constructorof the GADT (a :≈: b). Pattern matching on Refl tells the type checker that thetwo types are the same. In short, when the argument types are equal, eqT returns
a proof of this equality, in a form that the type checker can use.
To be concrete, here is the definition of fromDynamic:
fromDynamic :: ∀ d . Typeable d ⇒ Dynamic → Maybe d
fromDynamic (Dyn (ra :: TypeRep a) (x :: a))= case eqT ra (typeRep :: TypeRep d ) of
Nothing → Nothing
Just Refl → Just x
We use eqT to compare the two TypeReps, and pattern-match on Refl , so thatin the second case alternative we know that a and d are equal, so we can return
Just x where a value of type Maybe d is needed.
Since Maybe is a monad, we can use do notation for this code, and instead
write it like this:9

Here we are using GHC’s ability to define infix type constructors.

8

fromDynamic (Dyn ra x)= do Refl ← eqT ra (typeRep :: TypeRep d )return x
When we make multiple matches this style is more convenient, so we use it fromnow on.
More generally, eqT allows to implement type-safe cast, a useful operationin its own right [Wei04, LPJ03, LPJ05].
cast :: ∀ a b. (Typeable a, Typeable b) ⇒ a → Maybe bcast x = do Refl ← eqT (typeRep :: TypeRep a)(typeRep :: TypeRep b)
return x

5.4

Decomposing type representations

So far, the only operation we have provided over TypeRep is eqT , which compares two type representations for equality. But that is not enough to implement
dynFst:dynFst :: Dynamic → Maybe Dynamic
dynFst (Dyn pab x)= -- Check that pab represents a pair type-- Take (fst x) and wrap it in Dyn
How can we decompose the type representation pab, to check that it indeed
represents a pair, and extract its first component? Since types in Haskell arebuilt via a sequence of type applications (much like how an expression applying
a function to multiple arguments is built with several nested term applications),
the natural dual is to provide a way to decompose type applications:splitApp :: TypeRep a → Maybe (AppResult a)-- Primitive; implemented by compiler
data AppResult t where
App :: TypeRep a → TypeRep b → AppResult (a b)
The primitive operation splitApp allows us to observe the structure of types.
If splitApp is applied to a type constructor, such as Int, it returns Nothing ;otherwise, for a type application, it decomposes one layer of the application,and returns (Just (App ra rb)) where ra and rb are representations of the subcomponents. Like eqT , it returns a GADT, AppResult, to expose the type equalities it has discovered to the type checker.
Now we can implement dynFst:
dynFst :: Dynamic → Maybe Dynamic
dynFst (Dyn rpab x)

9= do App rpa rb ← splitApp rpab
App rp ra ← splitApp rpa
Refl← eqT rp (typeRep :: TypeRep (, ))return (Dyn ra (fst x))
We check that the type of x, whose TypeRep, rpab, is of form (, ) a b, by decomposing it twice with splitApp. Then we must check that rp, the TypeRep of thefunction part of this application, is indeed the pair type constructor (, ); we cando that using eqT . These three GADT pattern matches combine to tell the typechecker that the type of x, which began life in the (Dyn rpab x) pattern matchas an existentially-quantified type variable, is indeed a pair type (a, b). So we
can safely apply fst to x, to get a result whose type representation ra we have inhand.
In the same way we can use splitApp to implement dynApply , which applies
a function Dynamic to an argument Dynamic, provided the types line up:
dynApply :: Dynamic → Dynamic → Maybe Dynamic
dynApply (Dyn rf f ) (Dyn rx x) = do
App ra rt2 ← splitApp rf
App rtc rt1 ← splitApp ra
Refl← eqT rtc (typeRep :: TypeRep (→))
Refl
← eqT rt1 rx
return (Dyn rt2 (f x))
In both cases, the code is simple enough, but the type checker has to work
remarkably hard behind the scenes to prove that it is sound. Let us take a closer
look.
5.5

Kind polymorphism and kind equalities

There is something suspicious about our use of typeRep :: TypeRep (, ). So far
we have discused type representations for only types of kind ?. But (, ) has
kind (? → ? → ?); does it too have a TypeRep? Of course it must, to allow
TypeRep Int, TypeRep Maybe, and TypeRep (, ). So the type constructor TypeRepmust be polymorphic in the kind of its type argument, or poly-kinded, and somust be its accompanying class Typeable, thus:
data TypeRep (a :: k) -- primitive, indexed by type and kindclass Typeable (a :: k) where
typeRep :: TypeRep a
Fortunately, GHC has offered kind polymorphism for some years [YWC+ 12].
Similarly, the result GADT AppResult must be kind-polymorphic. Here is its
definition with kind signatures added10 :10

The kind signatures are optional. With PolyKinds enabled, GHC infers them, but weoften add them for clarity.

10

data AppResult (t :: k) where
App :: ∀ k 1 k (a :: k 1 → k) (b :: k 1 ).
TypeRep a → TypeRep b → AppResult (a b)
In AppResult, note that k 1 , the kind of b, is existentially bound in this data
structure, meaning that it does not appear in the kind of the result type (a b).
We know the result kind of the type application but there is no way to know thekinds of the subcomponents.
With kind polymorphism in mind, let’s add some type annotations to see
what existential variables are introduced by the two calls to splitApp in dynFst:
dynFst :: Dynamic → Maybe Dynamic
dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))= do App (rpa :: TypeRep pa) (rb :: TypeRep b) ← splitApp rpab-- introduces kind k 2 , and types pa :: k 2 → ?, b :: k 2
App (rp :: TypeRep p) (ra :: TypeRep a) ← splitApp rpa-- introduces kind k 1 , and types p :: k 1 → k 2 → ?, a :: k 1
Refl ← eqT rp (typeRep :: TypeRep (, ))-- introduces p ∼ (, ) and (k 1 → k 2 → ?) ∼ (? → ? → ?)return (Dyn ra (fst x))
Focus on the arguments to the call to eqT in the third line. We know that:––rp:: TypeRep p and p :: k 1 → k 2 → ?
typeRep :: TypeRep (, ) and (, ) :: ? → ? → ?

So eqT must compare the TypeReps for two types of different kinds; if the runtime test succeeds, we know not only that p ∼ (, ), but also that k 1 ∼ ? andk 2 ∼ ?. That is, the pattern match on Refl GADT constructor brings local kindequalities into scope, as well as type equalities.
We can make this more explicit by writing out kind-annotated definitions for(:≈:) and eqT , thus:
eqT :: ∀ k 1 k 2 (a :: k 1 ) (b :: k 2 ). TypeRep a → TypeRep b → Maybe (a :≈: b)data (a :: k 1 ) :≈: (b :: k 2 ) where
Refl :: ∀ k (a :: k). a :≈: a
If the two types are the same, then eqT returns a proof that the types are equaland simultaneously a proof that the kinds are equal: a heterogeneous (often
referred to as “John Major”) equality [McB02].
In the case of dynFst, if eqT succeeds, the type checker can conclude (k 1 →k 2 → ?) ∼ (? → ? → ?) and p ∼ (, ). The GHC constraint solver uses theseequalties to conclude that the type of x is (a, b), validating the projection fst x.
The addition of first-class kind equalities, to accompany first-class type equalities, is the most recent innovation in GHC 8.0. Indeed, they motivate a systemicchange, namely collapsing types and kinds into a single layer, so that we have11

? :: ?. This change is described and motivated in a recent paper [WHE13]. Typesafe decomposition of type representations is a compelling motivation for kindequalities.
5.6

Visible vs. invisible type representations

Here are two functions with practically identical functionality:
cast :: (Typeable a, Typeable b) ⇒ a → Maybe b
castR :: TypeRep a → TypeRep b → a → Maybe b
A Typeable class constraint is represented at runtime by a value argument, aTypeable “dictionary” in the jargon of type classes [WB89]. A dictionary is justa record of the methods of the class. Since Typeable a has only one method, aTypeable a dictionary is represented simply by a TypeRep a value. So, in implementation terms the function cast actually takes two TypeRep arguments exactly
like castR. It’s just that castR takes visible TypeRep arguments, while cast takes
invisible (compiler-generated) Typeable arguments. So which is “better”?
The answer is primarily stylistic. Sometimes, in library code that manipulates
many different TypeRep values, it is much clearer to name them explicitly, as wehave done in the earlier examples in this section. But in other places (usuallyclient code) it is vastly more convenient to take advantage of type classes toconstruct relevant Typeable evidence.
The two are, of course, equally expressive, since the implementation is thesame in either case. Going from an implicit type representation (Typeable) to an
explicit one (TypeRep) is easy, if inscrutable: just use the method typeRep. For
example, here is how to define cast using castR:
cast :: (Typeable a, Typeable b) ⇒ a → Maybe bcast = castR typeRep typeRep
The two calls to typeRep are at different types, but that is not very visible inthe code. That is why it is often clearer to pass TypeRep values explicitly. But
for the caller of cast is it much easier to pass invisible arguments; for example,
in the call:(cast x) :: Maybe Boolthe compiler will construct a TypeRep for x’s type and one for Bool , bothwrapped as Typeable dictionaries, and pass them to cast.
However, going from explicit to implicit is not as easy. Suppose we have a
TypeRep a and we wish to call a function with a Typeable a constraint. We essentially need to invent an instance Typeable a on the spot. Haskell provides nofacility for local instances, chiefly because doing so would imperil class coherence.11 In the context of type representations, though, incoherence is impossible:
11

Though, some Haskellers have hacked around this restriction with abandon. See Kiselyov and Shan [KS04] and Edward Kmett’s reflection package (at http://hackage.
haskell.org/package/reflection).

12

there really is only one TypeRep a in existence, and so one Typeable a instanceis surely the same as any other. Our API thus provides the following additional
function withTypeable, which we can use to close the loop by writing castR in
terms of cast:withTypeable :: TypeRep a → (Typeable a ⇒ r ) → r
castR :: TypeRep a → TypeRep b → a → Maybe b
castR ta tb = withTypeable ta (withTypeable tb cast)We cannot implement withTypeable in Haskell source. But we can implement it
in GHC’s statically-typed intermediate language, System FC [SCPJD07]. The
definition is simple, roughly like this:
withTypeable tr k = k tr-- Not quite rightIts second argument k expects a Typeable dictionary as its value argument. But
since a Typeable dictionary is represented by a TypeRep, we can simply pass tr
to k. When written in System FC there is a type-safe coercion to move from
TypeRep a to Typeable a, but that coercion is erased at runtime. Since thedefinition can be statically type checked, withTypeable does not form part of thetrusted code base.
5.7

Comparing TypeReps

It is sometimes necessary to use type representations in the key of a map. For
example, Shake [Mit12] uses a map keyed on type representations to look up classinstances (dictionaries) at runtime; these instances define class operations for thetypes of data stored in a collection of Dynamics. Storing the class operations once
per type, instead of with each Dynamic package, is much more efficient.12
More specifically, we would like to implement the following interface:data TyMap
empty :: TyMap
insert :: Typeable a ⇒ a → TyMap → TyMap
lookup :: Typeable a ⇒ TyMap → Maybe a
But how should we implement these type-indexed maps? One option is to
use the standard Haskell library Data.Map. We can define the typed-map as a
map between the type representation and a dynamic value.
data TypeRepX where
TypeRepX :: TypeRep a → TypeRepX
type TyMap = Map TypeRepX Dynamic
12

See also http://stackoverflow.com/q/32576018/791604 for another use case for amap keyed on type representations.

13

Notice that we must wrap the TypeRep key in an existential TypeRepX , otherwise
all the keys would be for the same type, which would rather defeat the purpose!
The insert and lookup functions can then use toDynamic and fromDynamic toensure that the right type of value is stored with each key.
insert :: ∀ a. Typeable a ⇒ a → TyMap → TyMap
insert x = Map.insert (TypeRepX (typeRep :: TypeRep a)) (toDynamic x)
lookup :: ∀ a. Typeable a ⇒ TyMap → Maybe alookup = fromDynamic <=< Map.lookup (TypeRepX (typeRep :: TypeRep a))
Because Data.Map uses balanced binary trees, TypeRepX must be an instance ofOrd :instance Ord TypeRepX wherecompare (TypeRepX tr1 ) (TypeRepX tr2 ) = compareTypeRep tr1 tr2
compareTypeRep :: TypeRep a → TypeRep b → Ordering -- primitive
The TypeRep API includes a comparison function compareTypeRep that compares two TypeReps, indexed by possibly-different types a and b. Notice that wecannot make an instance for Ord (TypeRep a): if we compare two values bothof type TypeRep t, following the signature of compare, they should always beequal!
Alternatively, we could use a more strongly typed data structure that internally keeps track of the dependency between the key and the element type. A
simple example might be the following binary search tree:
data TyMap = Empty | Node Dynamic TyMap TyMap
Of course, much more general structures are also possible.13
Looking up values in this tree requires comparing the ordering of type representations. We could implement this comparison using the ordering for TypeRepX ,but that implementation is clumsy. Once we have found the value, we must do
an extra cast to show that it has the correct type.
lookup :: TypeRep a → TyMap → Maybe alookup tr1 (Node (Dyn tr2 v ) left right) =case compareTypeRep tr1 tr2 of
LT → lookup tr1 left
EQ → castR tr2 tr1 v -- know this cast will succeed
GT → lookup tr1 rightlookup tr1 Empty = Nothing
However, we can improve this implementation using the following more informative comparison function, thereby avoiding this redundant check. In particular, when the two type representations are equal, this function will returnan equality proof, just like eqT .
13

The dependent-map library is an example of such a data structure. See
https://hackage.haskell.org/package/dependent-map-0.1.1.3/docs/
Data-Dependent-Map.html.

14

cmpT :: TypeRep a → TypeRep b → OrderingT a b-- definition is primitive

data OrderingT a b where
LTT :: OrderingT a b
EQT :: OrderingT t t
GTT :: OrderingT a b
It is, of course, trivial to define compareTypeRep in terms of cmpT .

5.8

Representing polymorphic and kind-polymorphic types

Our interface does not support representations of polymorphic types, such as
TypeRep (∀ a. a → a). Although plausible, supporting those in our setting brings
in a whole new range of design decisions that are as of yet unexplored (e.g.
higher-order representations vs. de-Bruijn?). Furthermore, it requires the language to support impredicative polymorphism (the ability to instantiate quantified variables with polymorphic types, for instance the a variable in TypeRep a or
Typeable a), which GHC currently does not. Finally, representations of polymorphic types have implications on semantics and possibly parametricity, an issue
that we discuss in the next section.
Similarly, constructors with polymorphic kinds would require impredicative
kind polymorphism. A representation of type TypeRep (Proxy :: ∀ kp. kp → ?)would require the kind parameter k of TypeRep (a :: k) to be instantiated tothe polymorphic kind ∀ kp. kp → ?. Type inference for impredicative kindpolymorphism is no easier than for impredicative type polymorphism and wehave thus excluded this possibility.

5.9

Summary

It is time to draw breath. We used the ST example to motivate a Dynamic type
(Section 3); then we used Dynamic to motivate type-indexed type representations(Section 5.1); and in the rest of Section 5 we have discussed the various operations
we need over those representations. Our final API for TypeRep is summarised in
Figure 1.
Why do we make TypeRep primitive rather than Dynamic? When we design
a primitive, built-in feature for a language, we seek the smallest, most sharplyfocused feature that serves the need. We need built-in support for something like
TypeRep and the Typeable class to implement Dynamic. If the Dynamic library
becomes just an ordinary library, with no uses of unsafeCoerce, that usefully
shrinks the trusted code base. Moreover, TypeRep is independently useful tosupport other abstractions (not just Dynamic), as we describe in Section 8.

15-- Related definitions ——————————————————–-- Informative propositional equality
data (a :: k 1 ) :≈: (b :: k 2 ) where
Refl :: ∀ k (a :: k). a :≈: a-- An informative ordering type, asserting type equality in the EQ casedata OrderingT a b where
LTT :: OrderingT a b
EQT :: OrderingT t t
GTT :: OrderingT a b-- Data.Typeable ————————————————————
data TypeRep (a :: k)-- primitive, indexed by type and kindinstance Show (TypeRep a)class Typeable (a :: k) where
typeRep :: TypeRep a-- Typeable instances automatically generated for all type constructors-- class accesswithTypeable :: TypeRep a → (Typeable a ⇒ r ) → r-- existential version
data TypeRepX where
TypeRepX :: TypeRep a → TypeRepX
instance Eq
TypeRepX
instance Ord TypeRepX
instance Show TypeRepX-- comparison
eqT :: TypeRep a → TypeRep b → Maybe (a :≈: b)
cmpT :: TypeRep a → TypeRep b → OrderingT a b-- construction
mkTyApp :: TypeRep a → TypeRep b → TypeRep (a b)-- pattern matching
splitApp :: TypeRep a → Maybe (AppResult a)data AppResult (t :: k) where
App :: TypeRep a → TypeRep b → AppResult (a b)-- information about the “head” type constructor
tyConPackage :: TypeRep a → String
tyConModule :: TypeRep a → String
tyConName :: TypeRep a → String
Fig. 1. New Typeable interface

16

6

Implementation

How do we implement type representations? We use a GADT like this:data TypeRep (a :: k) where
TrApp :: TypeRep a → TypeRep b → TypeRep (a b)
TrTyCon :: TyCon → TypeRep k → TypeRep (a :: k)data TyCon = TyCon {tc_module :: Module, tc_name :: String }data Module = Module {mod_pkg :: String , mod_name :: String }The TyCon type is a runtime representation of the “identity” of a type constructor. For every datatype declaration, GHC silently generates a binding for asuitable TyCon. For example, for Maybe GHC will generate:$tcMaybe :: TyCon$tcMaybe = TyCon {tc_module = Module {mod_pkg = "base", mod_name = "Data.Maybe"}, tc_name = "Maybe"}
The name $tcMaybe is not directly available to the programmer. Instead (this is
the second piece of built-in support), GHC’s type-constraint solver has special
behaviour for Typeable constraints, as follows.
To solve Typeable (t 1 t 2 ), GHC simply solves Typeable t 1 and Typeable t 2 ,and combines the results with TrApp. To solve Typeable T where T is a type
constructor, the solver uses TrTyCon. The first argument of TrTyCon is straightforward: it is the (runtime representation of the) type constructor itself, e.g.
$tcMaybe.
But TrTyCon also stores the representation of the kind of this very constructor, of type TypeRep k. Recording the kind representations is important, otherwise we would not be able to distinguish, say, Proxy :: ? → ? from Proxy :: (? →?) → ?, where Proxy has a polymorphic kind (Proxy :: ∀ k. k → ?). We do
not support direct representations of kind-polymorphic constructors like Proxy ,for reasons outlined in Section 5.8; rather TrTyCon encodes the instantiationof a kind-polymorphic constructor (such as Proxy ). There is a limitation here:
the kind of the instantiated type constructor must be monomorphic (again, forreasons outlined in Section 5.8), so (a) the type constructor must have a rank-1
prenex-polymorphic kind, and (b) it can be instantiated only with monomorphic
kinds (i.e. predicatively).
Notice that TrTyCon is fundamentally insecure: you could use it to build a
TypeRep t for any t whatsoever. That is why we do not expose the representationof TypeRep to the programmer. Instead the part of GHC’s Typeable solver thatbuilds TrTyCon applications is part of GHC’s trusted code base.
Another reason for keeping TypeRep abstract is that it allows us to varydetails of the representation. For example, the SYB pattern (Section 8.2) makes
many equality tests for TypeRep. If we stored a fingerprint, or even a hash-value,in every node, we could make comparisons work in constant time. Another aspectthat we might want to vary is how much meta-data we make available in a TyCon.

17

7

Properties of a language with reflection

The addition of features such as Dynamic and TypeRep has implications to thesemantics and metatheory of a programming language.
Strong normalization. The addition of type Dynamic (whether implemented with
TypeRep or not) creates the possibility for loops without explicitly using recursion (nor recursive data types):delta :: Dynamic → Dynamic
delta dn = case fromDynamic dn ofJust f → f dn
Nothing → dnloop = delta (toDynamic delta)
Effectively Dynamic behaves like a negative recursive datatype, a feature thatbreaks strong normalization.
A similar example can be encoded with the more primitive TypeRep, adapting
an example from previous work [VW10] (Section 5.3):
data Rid = MkT (∀ a. TypeRep a → a → a)
rt :: TypeRep Rid
rt = typeRepdelta :: ∀ a. TypeRep a → a → adelta ra x = case (eqT ra rt) of
Just Refl → case x of MkT y → y rt x
Nothing → x
loop = delta rt (MkT delta)
These examples demonstrate that primitives like TypeRep or Dynamic cannot
be incorporated in languages where logical consistency is required, such as Coq
or Agda, without further restrictions (e.g. predicative polymorphism, or weakerelimination forms). Fortunately Haskell is not one of those.
Parametricity Now that we have added TypeRep, Typeable and automaticallygenerated type representations as built-in features, the alert reader might wonder
whether we have perhaps accidentally weakened parametricity, and thereby lostPhil’s free theorems.
Fortunately, the type system makes it explicit when run-time reflection isused, and must do so even though every type is Typeable. Phil’s free theorems
would go out of the window if we allowed cast to have the type cast :: a →Maybe b! That is the principled reason for requiring explicit Typeable constraints.
There is an operational reason too: the Typeable constraint is implemented asa runtime argument; if there was no explicit Typeable constraint we would beforced to pass a Typeable dictionary to every polymorphic function, just in caseit needed it, which would be disgusting.

18

Thanks to those explicit type representation arguments, techniques that haveappeared in previous work [VW10] for a closed world of representations can beused to deduce “free theorems” from the types of all polymorphic functions. When
those functions include TypeRep arguments (or Typeable constraints) then suchtheorems can still be derived but are often not very informative.
We conjecture that these results will carry over to (a) an open world of type
representations, and (b) representations of types that hide polymorphic types
in their defining equations (such as Rid above; see Section 5.3 of [VW10]), butboth directions are open problems – perhaps new puzzles for Phil to solve!

8

Other applications of TypeRep and dynamic

One of the advantages of building Dynamic on top of TypeRep is that the latteris independently useful to build other abstractions. We briefly describe some ofthese applications in this section.
8.1

Variants of Dynamic

In ML, the extensible exception type is built-in, but not so in Haskell: it is programmed as a library using Typeable, using a design described by “An extensible
dynamically-typed hierarchy of exceptions” [MPJMR01]. Here are the key definitions:
throw # :: SomeException → adata SomeException where
SomeException :: Exception e ⇒ e → SomeException
class (Typeable e, Show e) ⇒ Exception e where {...}The primitive exception-raising operation is throw #. Its argument is the fixed
type SomeException, whose definition is an existential rather like Dynamic; thedifference is that as well as having a Typeable superclass (which makes it like
Dynamic), Exception also has Show superclass, and some methods of its own.
The fundamental data structure of the Shake build system [Mit12] is a directed acyclic graph (DAG) in which each node contains a value, a recipe forrecomputing that value, and the dependencies of the node. If the values of anyof the dependent nodes changes, the node’s own value should be recomputed.
The value in a node may be of any type, including types defined by the client of
the Shake library, so again we have a fundamentally open-world problem. Shakesolves this by ubiquitous use of dynamically typed values, both as keys and asvalues of its finite mappings [Mit12, Section 4.1]. For example, the Shake typeAny is just like Dynamic, except that it includes Binary , Eq, Hashable, Show ,and NFData constraints.

19

8.2

Supporting generic programming

Here is the opening example from “Scrap Your Boilerplate” [LPJ03]:
increase :: Float → Company → Company
increase k = everywhere (mkT (incS k))
A Company is a tree-shaped data structure describing a company; the function
increase is supposed to find every employee in the data structure and increase hisor her salary by k, using incS ::Float → Salary → Salary . The function everywhereapplies its argument function to every node in the data structure; we will notconsider it further here. Our focus is the function mkT , which depends criticallyon Typeable:
mkT :: (Typeable a, Typeable b) ⇒ (b → b) → a → a
mkT f x = case (cast f ) of
Just g → g x
Nothing → x
That is, mkT takes a type-specific function (such as incS) and lifts it to work on
values of any type, as follows: if types match use g , otherwise use the identity
function. (cast was described in Section 5.7.)
So the SYB approach to generic programming depends crucially on dynamic
type tests. The popular Uniplate library for generic programming also makes
essential use of comparison of TypeReps, for a similar purpose as SYB [MR07].
Note, however, that TypeRep alone is not enough to support generic programming (see Section 9.5).
8.3

Distributed programming and persistence

Cloud Haskell is an Erlang-style library for programming a distributed system
in Haskell [EBPJ11]. A key component of the implementation, described in thepaper, is the ability to serialise a code pointer and send it from one node toanother in the distributed system. This code pointer could be implemented ina variety of ways, such as: a machine address, a small integer, a long string, a
URL.
But regardless of how it is implemented, the receiving node must deserialise
the code pointer to some code. To guarantee that the code is then applied toappropriately typed values, the receiving node must perform a dynamic type
test. That way, even if the code pointer was corrupted in transit, by accident
or malice, the receiving node will be type-sound. A simple way to do this is toserialise a code pointer as a key into a static pointer table containing Dynamic
values. When receiving code pointer with key k, the recipient can lookup up
entry k in the table, find a Dynamic, and check that it has the expected type.
The key can be an integer, a string, or whatever; regardless, if it is corrupted,
the recipient might access the wrong entry in the table, but the type test will
ensure soundness.

20

In other variants of this idea, one might want to serialise and deserialisevalues of type Dynamic, and hence of type TypeRep. It turns out that this raises
some quite interesting issues that are beyond the scope of this paper14 .
8.4

Meta programming

It is perhaps unsurprising that meta programming for a statically typed target
language often involves type reflection. For example, it is popular to define a
type-indexed version of the syntax tree of expressions, so that a value of type
Expr t is a syntax tree for an expression of type t. But then what is the type ofa front end for the language, which takes a String , parses it (presumably to an
un-typed syntax tree), and then typechecks it to reject type-incorrect programs.
The front end cannot have this type
frontEnd :: String → Maybe (Expr a) -- No!
because that is too polymorphic. The type a has to depend on the contents ofthe string! So we need something more like this:data DynExp where
DE :: TypeRep a → Expr a → DynExp
frontEnd :: String → DynExp
Here frontEnd returns an existential pair of a Expr a, and a TypeRep that describes the type of the expression. The earliest paper we have found that clearly
embodies this idea is “Tagless staged interpreters for typed languages” [PTS02],
but it has become more widespread since Haskell has supported this programming style [GM08, MCGN15].

9

Related work

9.1

The old implementation of Typeable and Dynamic

GHC has supported Dynamic and a non-indexed version of TypeRep for sometime. Here is the essence of the implementation in GHC 7.10:
data TypeRep -- Abstractclass Typeable a where
typeRep :: proxy a → TypeRepdata Dynamic where
Dyn :: TypeRep → a → Dynamic
data Proxy a = Proxy14

See the tree of wiki pages rooted at https://ghc.haskell.org/trac/ghc/wiki/
DistributedHaskell for lots more information.

21

Typeable had built-in support, so that newly declared data types would automatically get Typeable instances. But TypeRep was not indexed, so there wasno connection between the TypeRep stored in a Dynamic and the corresponding
value. Indeed, accessing the typeRep required a proxy argument to specify thetype that should be represented.
Because there is no connection between types and their representations, this
implementation of Dynamic requires unsafeCoerce. For example, here is the old
fromDynamic:
fromDynamic :: ∀ d . Typeable d ⇒ Dynamic → Maybe d
fromDynamic (Dyn trx x)| typeRep (Proxy :: Proxy d ) == trx = Just (unsafeCoerce x)| otherwise= Nothing
Likewise, unsafeCoerce was used in the definition of dynApply :dynApply :: Dynamic → Dynamic → Maybe Dynamic
dynApply (Dyn trf f ) (Dyn trx x) =case splitTyConApp trf of(tc, [t 1 , t 2 ]) | tc == funTc && t 1 == trx →Just (Dyn t 2 ((unsafeCoerce f ) x))→ Nothing
Here splitTyConApp, a special definition from Data.Typeable that decomposes
type representations, and funTc is the function type constructor. There is nothing
special about function types. Other forms of data also need their own unsafe
elimination functions to be defined. For example, the implementations of dynFst
and dynSnd are similar, and also require unsafeCoerce.
Furthermore, the library designer cannot hide all such uses of unsafeCoerce
from the user. If they want to use their own parameterized type with Dynamic,
then they too must use unsafeCoerce. In short, the old interface to this libraryis not expressive enough to work with type representations and dynamics safely.
9.2

Dynamics in a closed world

We have focused entirely on an open-world setting (Section 4). If, however, yourapplication can work with a closed world, with a predetermined set of type
constructors, then simpler designs are available.
Universal datatype implementation of Dynamic. The most obvious way
to implement closed-world dynamics is to use a universal datatype to represent
dynamic values (see Section 4). But even in a closed-world setting this approachis unsatisfactory. Most prominently it suffers from a serious efficiency problem,
because converting a value to or from Dynamic traverses the value itself. For
example, to convert an (Int, Bool ) pair to a Dynamic, we would have to deepcopy the value, and then do the reverse when we get it out. This is silly: in the

22

ST example of Section 3 we only want to store the value in the Store, and readit back out later; we shouldn’t need to process the value in any way whatsoever!
Processing the value has a semantic problem too: a dynamic type test forces
evaluation of a term, so it will fail on diverging terms; in our ST example, we
could not store bottom in the Store.
GADT-based type representations. In a closed-world setting, TypeRep canbe implemented as an ordinary library without built-in support, thus:
data TypeRep (a :: ?) where
TBool :: TypeRep Bool
TFun :: TypeRep a → TypeRep b → TypeRep (a → b)
TProd :: TypeRep a → TypeRep b → TypeRep (a, b)...
With this representation for TypeRep, the functions eqT , dynApply , dynFst, etc.,
are all easily written, using pattern-matching on the TypeRep GADT. The trouble with this approach is simply that it is not extensible: the set of representabletypes is limited those with data constructors in TypeRep.
History of encoding type representations. In concurrent work, Cheney and Hinze[CH02] and Baars and Swierstra [BS02] showed how to implement type Dynamic
by first encoding indexed type representations, similar to the GADT shown
above. (GADTs were not a part of GHC at that time). These type representation encodings were based on earlier work by Yang [Yan98] and Weirich [Wei04].
In particular, Yang showed how to encode the TypeRep type above using higherorder polymorphism (available in the ML module system). And Weirich used
type classes to encode a version of type Dynamic that supported type-safe
cast (i.e. toDynamic and fromDynamic) but could not destruct types (i.e. no
dynApply ).
9.3

Dynamic typing in other statically-typed languages

Several statically typed languages include a Dynamic type as a language primitive. Abadi et al. [ACPP91, ACPR95] laid the groundwork for such extensions,by incorporating a special type Dynamic to contain values of unknown type. Values of this type could be refined using a typecase operator that allowed patternmatching on the actual type of the value.
Clean. The Clean language includes a dynamic type as well as a class constraint
similar to Typeable, called TC , for types that support “type codes” [Pil99]. Unlike
Haskell, where Dynamic is defined in terms of Typeable, both of these structures
are language primitives in Clean. Pil [Pil99] makes the case that type Dynamic
is not enough on its own; languages should also include something like Typeable.
Making Dynamic a language primitive is powerful. For example, Clean can support polymorphic values embedded into dynamics. In other words, types such as∀ a. a → a are Typeable, unlike in Haskell (Section 5.8).

23

Clean’s interface to runtime types is also different from a user perspective.
Clean includes runtime type unification using type-pattern variables. This features subsumes both runtime type equality (as in our eqT ) as type patterns may
be nonlinear, and type destruction (as in our splitApp). We conjecture that thisdifference is cosmetic.
OCaml. Leroy and Mauny [LM91] used similar mechanism to Abadi et al. inorder to extend the ML language with a dynamic type. However, more recent
extensions in support of dynamic typing in OCaml have been proposed in workshop talks [Fri11, HG13]. Like the design presented here, these extensions include
a type for type representations ’a ty, and a comparison operation that returns
a GADT-based witness for type equality.
These extensions also include a mechanism to decompose type representations. In this case, every type constructor needs its own a decomposition GADTand function. For example (using Haskell syntax), the pair type constructor
would be accompanied by the following:
data IsPair a where
TypePair :: TypeRep a → TypeRep b → IsPair (a, b)
isPair :: TypeRep a → Maybe (IsPair a) -- Primitive implementation
These definitions could then be used to implement dynFst.
dynFst :: Dynamic → Maybe Dynamic
dynFst (Dyn tab x) = case isPair tab of
Just (TypePair ta tb) → Just (fst x)
Nothing → Nothing
Our AppResult GADT and splitApp function uses GHC’s kind-polymorphism togeneralize these definitions for any type constructor.
9.4

Reflection in JavaIn a language with subtyping and down-casting, a maximal supertype acts like a
dynamic type. For example, in Java, a reference type, like String , can be coerced
to Object (the maximal supertype) without runtime overhead. Furthermore, Javaalso supports a simple equivalent of fromDynamic using a runtime cast.
Here is another connection to Phil, who introduced generics to Java [BOSW98].
Java’s generics are limited in two (related) ways: Java has no notion of higherkinded types, and type parameters to generic clases (such as ListhT i) and methods are erased, disallowing dynamic checks involving those parameters.
Generics have enhanced Java’s reflection feature, which has remarkable parallels to Haskell’s. From its first versions, Java had the Class type, which was
useful for queries about a type, but not for casting. Phil’s generics then allowed
Class to be type-indexed [NW06], just like we are doing with TypeRep. For any
reference type T in modern Java, the expression T .class is a runtime type representation, of type ClasshT i. With a ClasshT i in hand, we can cast an arbitraryvalue to T , even if T is a type parameter.

24

9.5

Generic programming and type representations

The type representations described in this paper are not designed for full-blown
datatype generic programming [Gib07]. TypeRep allows one to compare and explore just the shape of a type including names of type constructors and type arguments. But generic programming requires the additional capability to generically
explore the structure of the values inhabiting a type; for instance by allowing
one to iterate over the data constructors of some unknown type without having
the actual type definition in scope.
There are many ways to support generic programming; from isomorphisms oftypes to sums and products (for example the Generic class in Haskell [MDJL10]),
to providing built-in generic instances for iterators (for example the Data classin Haskell [LPJ03]), to advanced variants of TypeRep that additionally include
type-indexed data structures for describing data constructors and introducing/eliminating values generically [Wei06].

10

Conclusions and further work

In this paper, we have designed a powerful API for type reflection and shownthat it can be used to implement a flexible and extensible dynamic type. The
next major challenge is to provide a better story for polymorphic dynamic values(Section 5.8).

Acknowledgements
Thanks to Neil Mitchell both for help in understanding Shake and for a rapid
review. Kenneth Foner also provided feedback on a draft. Ben Price’s internshipat Microsoft Research was helpful in bringing some of the key issues to thesurface. This paper was typeset with lhs2TeX 15 .
Finally, thanks to Phil, who has spent much of his professional life reflecting
on types. Increasingly, Haskell can too. Happy birthday Phil!

References[ACPP91][ACPR95][BOSW98]

15

Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin.
Dynamic typing in a statically-typed language. ACM Transactions on
Programming Languages and Systems, 13(2):237–268, April 1991.
Martín Abadi, Luca Cardelli, Benjamin Pierce, and Didier Rémy. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5(1):111–130, January 1995.
Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler.
Making the future safe for the past: Adding genericity to the Java programming language. In Conference on Object-oriented Programming,
Systems, Languages, and Applications, pages 183–200. ACM, 1998.

http://www.andres-loeh.de/lhs2tex/

25[BS02][CH02][EBPJ11][EW12][Fri11][Gib07][GM08][HG13][HHPJW07][KS04][LM91][LPJ95][LPJ03][LPJ05][McB02][MCGN15][MDJL10][Mit12][MPJMR01]

Arthur I. Baars and Doaitse Swierstra. Typing dynamic typing. In
International Conference on Functional Programming, pages 157–166.
ACM, 2002.
James Cheney and Ralf Hinze. A lightweight implementation of generics
and dynamics. In Workshop on Haskell, pages 90–104. ACM, 2002.
Jeff Epstein, Andrew P. Black, and Simon Peyton Jones. Towards
Haskell in the cloud. In Haskell Symposium. ACM, 2011.
Richard A. Eisenberg and Stephanie Weirich. Dependently typed programming with singletons. In Haskell Symposium. ACM, 2012.
Alain Frisch. Runtime types in OCaml. Presentation at Meeting of theCaml Consortium, November 2011.
Jeremy Gibbons. Datatype-generic programming. In Roland Backhouse,
Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, DatatypeGeneric Programming, volume 4719 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2007.
Louis-Julien Guillemettte and Stefan Monnier. A type-preserving compiler in Haskell. In International Conference on Functional Programming. ACM, 2008.
Grégoire Henry and Jacques Garrique. Dynamic typing in OCaml. Presentation at Nagoya University, 2013.
Paul Hudak, John Hughes, Simon Peyton Jones, and Philip Wadler. A
history of Haskell: being lazy with class. In Conference on History ofProgramming Languages, 2007.
Oleg Kiselyov and Chung-chieh Shan. Functional pearl: Implicit
configurations–or, type classes reflect the values of types. In Workshop
on Haskell, pages 33–44. ACM, 2004.
Xavier Leroy and Michel Mauny. Dynamics in ML. In J. Hughes, editor,
Functional Programming Languages and Computer Architecture, volume523, pages 406–426. Springer-Verlag, 1991.
John Launchbury and Simon Peyton Jones. State in Haskell. Lisp Symb.
Comput., 8(4), December 1995.
Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate: a practical design pattern for generic programming. In Workshop on Types in
Languages Design and Implementation. ACM, 2003.
Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate with class:
Extensible generic functions. In International Conference on Functional
Programming. ACM, 2005.
Conor McBride. Elimination with a motive. In Workshop on Typesfor Proofs and Programs, TYPES ’00, pages 197–216. Springer-Verlag,
2002.
Trevor McDonell, Manuel Chakravarty, Vinod Grover, and Ryan Newton. Type-safe runtime code generation. In Haskell Symposium, pages
201–212. ACM, 2015.
Jose Pedro Magalhaes, Atze Dijkstra, Johan Jeuring, and Andres Loeh.
A generic deriving mechanism for Haskell. In Haskell Symposium, pages
37–48. ACM, 2010.
Neil Mitchell. Shake before building: Replacing Make with Haskell. In
International Conference on Functional Programming. ACM, 2012.
Simon Marlow, Simon Peyton Jones, Andrew Moran, and John Reppy.
Asynchronous exceptions in Haskell. In Programming Language Design
and Implementation. ACM, 2001.

26[MR07][NW06][Pil99][PJVWW06][PJW93][PTS02][SCPJD07][VW10][Wad89][Wad90][WB89][Wei04][Wei06][WHE13][XCC03][Yan98][YWC+ 12]

Neil Mitchell and Colin Runciman. Uniform boilerplate and list processing. In Workshop on Haskell. ACM, 2007.
Maurice Naftalin and Phil Wadler. Java Generics and Collections.
O’Reilly Media, 2006.
Marco Pil. Dynamic types and type dependent functions. In K. Hammand, T. Davie, and C. Clack, editors, Workshop on the Implementationof Functional Languages, LNCS, pages 169–185. Springer Verlag, 1999.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs.
In International Conference on Functional Programming, pages 50–61.
ACM, 2006.
Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Principles of Programming Languages. ACM, 1993.
Emir Pasalic, Walid Taha, and Tim Sheard. Tagless staged interpreters
for typed languages. In International Conference on Functional Programming. ACM, 2002.
Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, andKevin Donnelly. System F with type equality coercions. In Workshop
on Types in Languages Design and Implementation. ACM, 2007.
Dimitrios Vytiniotis and Stephanie Weirich. Parametricity, type equality, and higher-order polymorphism. Journal of Functional Programming, 20:175–210, 2010.
Philip Wadler. Theorems for free! In International Conference on Functional Programming Languages and Computer Architecture. ACM, 1989.
Philip Wadler. Comprehending monads. In Conference on LISP and
Functional Programming. ACM, 1990.
Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism
less ad-hoc. In Principles of Programming Languages, pages 60–76.
ACM, 1989.
Stephanie Weirich. Type-safe cast. Journal of Functional Programming,
14(6):681–695, November 2004.
Stephanie Weirich. Replib: A library for derivable type classes. In
Workshop on Haskell. ACM, 2006.
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. System FC
with explicit kind equality. In International Conference on Functional
Programming, pages 275–286. ACM, 2013.
Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatypeconstructors. In Principles of Programming Languages. ACM, 2003.
Zhe Yang. Encoding types in ML-like languages. In International Conference on Functional Programming, pages 289–300. ACM, 1998.
Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
Dimitrios Vytiniotis, and José Pedro Magalhaẽs. Giving Haskell a promotion. In Workshop on Types in Language Design and Implementation.
ACM, 2012.