Equality Proofs
Equality Proofs
Equality Proofs
A Compiler Pearl
Dimitrios Vytiniotis
Utrecht University
jpm@cs.uu.nl
Abstract
The Glasgow Haskell Compiler is an optimizing compiler that expresses and manipulates first-class equality proofs in its intermediate language. We describe a simple, elegant technique that exploits
these equality proofs to support deferred type errors. The technique
requires us to treat equality proofs as possibly-divergent terms; we
show how to do so without losing either soundness or the zerooverhead cost model that the programmer expects.
Categories and Subject Descriptors D.3.3 [Language Constructs
and Features]: Abstract data types; F.3.3 [Studies of Program
Constructs]: Type structure
General Terms Design, Languages
Keywords Type equalities, Deferred type errors, System FC
1.
Introduction
based on a simple observation: System FC , with the recent addition of kind polymorphism (Yorgey et al. 2012), already allows
us to define within the system an ordinary first-class type for
type equality (Section 4). As such, we can have ordinary values of that type, that are passed to or returned from arbitrary
(even partial or divergent) terms. Moreover, deferring type errors aside, there are other compelling advantages of proofs-asvalues in an evidence-passing compiler, as we outline in Section 6.
Most functional programmers think of types as static objects,
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. To copy otherwise, to republish, to post on servers or to redistribute
to lists, requires prior specific permission and/or a fee.
ICFP12, September 915, 2012, Copenhagen, Denmark.
Copyright 2012 ACM 978-1-4503-1054-3/12/09. . . $10.00
with zero run-time overhead, and they expect the same of proofs
about types. Treating type equality proofs as values seriously
undermines this expectation. In Section 7 we address this challenge and show how the optimizer of GHC, with no changes
whatsoever, can already eliminate the cost of equality proofs
except in corner cases where it would be wrong to do so.
2.
Suppose you type this Haskell term into the interactive read-evalprint prompt in GHCi:
ghci> fst (True, a && False)
This term does not go wrong when evaluated: you might expect
to just get back the result True from projecting the first component
of the pair. But in a statically typed language like Haskell you get
the type error:
Couldnt match Bool with Char
In the first argument of (&&), namely a
This behaviour is fine for programs that are (allegedly) finished, but
some programmers would much prefer the term to evaluate to True
when doing exploratory programming. After all, if the error is in
a bit of the program that is not executed, it is doing no harm! In
particular, when refactoring a large program it is often useful to be
able to run parts of the completed program, but type errors prevent
that. What we want is to defer type errors until they matter. We have
more to say about motivation and related work in Section 8.
As we shall see, System FC allows us to offer precisely this behaviour, without giving up type safety. Here is an interactive session
with ghci -fdefer-type-errors:
ghci> let foo = (True, a && False)
Warning: Couldnt match Bool with Char
ghci> :type foo
(Bool, Bool)
ghci> fst foo
True
ghci> snd foo
Runtime error: Couldnt match Bool with Char
Notice that:
The definition of foo produced a warning (rather than an error),
True.
The term snd foo also typechecks fine, and runs; however the
GHCs type inference algorithm works in two stages: first we generate type constraints, and then we solve them (Vytiniotis et al.
2011). In addition, inference elaborates the Haskell source term to
an explicitly typed FC term, that includes the types and proofs (evidence in GHC jargon) computed by the constraint solver.
3.
The FC language
Terms
e, u ::=
|
|
|
|
|
p
::=
Types
, , ,
x | l | x: .e | e u
a:.e | e | .e | e
c:.e | e
K | case e of p u
let x: = e in u
e.
K c: x:
`tm e :
Type/kind polymorphism
Coercion abs/app
` x:
, (x: ) `tm e :
`ty : ?
Cast
Patterns
`tm x: .e :
::=
|
|
|
|
|
|
a
H
F
1 2
a:.
.
Variables
Constants
Type functions
Application
Kind application
Polymorphic types
Kind-polymorphic types
T
()
(# )
Datatypes
Arrow
Primitive equality type
|?|
.
Constraint#
Polymorphic kinds
Kind of static proofs
Coercion values
,
::=
|
|
|
|
|
c
1 2
hi
1 ; 2
sym
...
Variables
Application
Reflexivity
Transitivity
Symmetry
Other coercion forms
Environments
,
::=
bnd
::=
|
|
|
|
|
|
Notation
T
| , bnd
a:
c : #
x:
T : . ?
K : (a:a ). T a
...
T 1 . . . m 1 . . . n
1 . . . n
for either or
The syntax of coercions themselves ( in Figure 1) includes coercion variables, constructors for reflexivity, transitivity, and symmetry, as well as other constructors (such as lifting type equalities over
data constructors) that we do not need to discuss in this paper.
The well-formedness judgement for terms appears in Figure 2
and is mostly conventional. In particular, the rules for coercion
abstraction and application (ECA BS and ECA PP) mirror those for
terms (EA BS and EA PP). The rule for case expressions (EC ASE) is
also standard but notice that it allows us to bind coercion variables,
as well as term variables, in a pattern.
`tm K :
EA BS
ECA BS
`tm e : (1 # 2 )
`co : 1 # 2
`k
, (a:) `tm e :
`tm a:.e : a:.
, `tm e :
`tm .e : .
ETABS
EK ABS
, (x: ) `tm u :
, (x: ) `tm e :
`tm let x: = u in e :
EL ET
EA PP
`tm e u :
`tm c: .e :
`tm e :
EC ON
`tm e :
`tm u :
, (c: ) `tm e :
`ty : Constraint#
ECA PP
`tm e : a:.
`ty :
`tm e : [/a]
`tm e : .
`k
`tm e : [/]
`tm e :
`co : #
`tm e . :
`tm e : T
For each branch K x: u
(K: (a:a ).1 # 2 T a) 0
i = i [/][ /a]
1i = 1i [/][ /a]
2i = 2i [/][ /a] , c:1 2 x: `tm u :
Kind variable
Type variable
Coercion variable
Term variable
Data type
Data constructor
Type families etc.
3.1
EVAR
tm
Type constants
H
::=
|
|
Kinds
,
::=
|
|
(K: ) 0
(x:)
ETA PP
EKA PP
EC AST
EC ASE
The cast converts the type of the result from [Int ] to [a]2 . The
coercion sym [c] is evidence for (or a proof of) the equality of these
types, lifting c (of type a # Int) over lists ([c], of type [a] # [Int ]),
before applying symmetry. We urge the reader to consult Sulzmann
et al. (2007) and Weirich et al. (2011) for more examples and
intuition.
`ty :
(a : )
(T : )
TVAR
ty
`ty T :
` a:
`ty 1 : 1 `ty 2 : ?
1 {?,Constraint# }
`ty 1 2 : ?
`ty 1 : 1 2
`ty 2 : 1
`ty 1 2 : 2
, (a:) `ty : ?
`k
ty
TA PP
TDATA
TA RR
`ty : .
`k
`ty : [/]
TKA PP
4.
TA LL
` a:. : ?
`ty . : ?
TKA LL
`co : 1 # 2
...
`k
...
, `ty : ?
In
coercions can appear as arguments to data constructors,
a feature that is particularly useful for representing generalized
algebraic datatypes (GADTs) (Peyton Jones et al. 2006). Consider
this source Haskell program which defines and uses a GADT:
data T a where
T1 :: Int T Int
T2 :: a T a
f :: T a [a]
f (T1 x) = [x + 1]
f (T2 v) = [ ]
main = f (T1 4)
In FC , we regard the GADT data constructor T1 as having the type:
T1 : a . (a # Int) Int T a
So T1 takes three arguments: a type argument to instantiate a, a
coercion witnessing the equality between a and Int, and a value of
type Int. Here is the FC version of main:
main = f Int (T1 Int hInti 4)
The coercion argument has kind Int # Int, for which the evidence
is just hInti (reflexivity). Similarly, pattern-matching on T1 binds
two variables: a coercion variable, and a term variable. Here is the
FC elaboration of function f :
f = (a : ?) . (x : T a) .
case x of
T1 (c : a # Int) (n : Int)
(Cons (n + 1) Nil) . sym [c]
T2 v Nil
In Section 2 we sketched how to use type-equality evidence to support deferred type errors, using as the type of equality evidence. Then in Section 3 we introduced our intermediate language,
System FC , in which explicit coercions of type # represent evidence for the equality of two types. The distinction between ()
and (# ) is crucial: it allows us to to marry a sound, erasable language of proofs with the potentially-unsound ability to have terms
that compute proofs, as we discuss in this section.
4.1
The tension
erasable, and
informally use Haskells notation [ ] for the type list of , and Cons
and Nil as its constructors.
5.
cast : (a b : ?) . a (a b) b
cast = (a b : ?) . (x : a) . (eq : a b) .
case eq of Eq# (c : a # b) x . c
Each use of cast forces evaluation of the coercion, via the case
expression and, in the case of a deferred type error, that is what
triggers the runtime failure.
Just as cast is a lifted version of ., we can lift all the coercion
combinators from the (# ) type to (). For example:
mkRefl :: . (a : ) . a a
mkRefl = . (a : ) . Eq# a a hai
mkSym :: . (a b : ) . (a b) (b a)
mkSym = . (a b : ) . (c : a b) .
case c of Eq# c Eq# b a (sym c)
The relationship between () and (# ) is closely analogous to that
between Int and Int# , described twenty years ago in our implementation of arithmetic in GHC (Peyton Jones and Launchbury 1991).
Concretely, here is GHCs implementation of addition on Int:
data Int = I# Int#
plusInt :: Int Int Int
plusInt x y = case x of I# x0
case y of I# y0 I# (x0 +# y0 )
An Int is an ordinary algebraic data type with a single constructor
I# (the # is not special; it is just part of the constructor name). This
constructor has a single argument, of type Int# , which is the type
of unboxed integers, a honest-to-goodness 32-bit integer value just
like Cs int. Finally (+# ) is the machine 32-bit addition instruction.
We may summarise the relationships thus:
A value of type Int, or , is always heap-allocated; it is
Step 1: traverse the syntax tree of the input Haskell term, gen-
For example, consider the term show xs, where xs : [Int ], and
show : a . Show a a String. In Step 1 we generate:
Elaborated term:
Constraint:
Equality constraints
show [Int ] d6 xs
d6 : Show [Int ]
The elaborated term looks much like the original except that show
is now applied to a type argument [Int ] (corresponding to the a
in shows type) and an evidence argument d6 (corresponding to the
Show a in its type). The constraint is given a fresh name,
d6 in this example, which is mentioned in the elaborated term.
Afficionados of Haskells type-class system will recognise d6 as
shows dictionary argument: it is simply a tuple of functions, the
methods of the Show class.
show d6 (cast xs c5 )
d6 : Show
c5 : [Int ]
In Step 2, the constraint solver has a little extra work to do: as well
as solving the constraints and giving bindings for the evidence variables, it must also produce bindings for the unification variables. In
our running example, the solution to the constraints looks like this:
c5 : [Int ]
d6 : Show [Int ]
=
=
=
[Int ]
mkRefl [Int ]
$dShowList Int $dShowInt
cast = (a b : ?) . (x : a) . (eq : a b) .
case eq of
Eq# (c : a # b) x . c
Error s error s
The technique works uniformly for all type constraints, not
FC
The type Int Int simply does not make sense applying Int to
Int is a kind error, and we do not have a convenient way to defer
kind errors, only type errors.
5.4
uses the (known) type of upper to type-check its argument, expecting the result to be of type [Char ]. This idea of pushing down the
expected type into an expression, sometimes called bidirectional
or local type inference (Pierce and Turner 2000), is already implemented in GHC to improve the quality of error messages; see
Peyton Jones et al. (2007, Section 5.4) for details. Although it is a
heuristic, and not a formal guarantee, the mechanism localises the
casts very nicely in practice.
Nevertheless, the bottom line is that the dynamic semantics of a
type-incorrect program depends on hard-to-specify implementation
details of the type inference algorithm. That sounds bad! But we
feel quite relaxed about it:
The issue arises only for programs that contain errors. Type
are treated uniformly with type-class constraints and implicitparameter constraints; anywhere a class constraint can appear,
an equality constraint can appear, and vice versa. Class constraints
and implicit-parameter constraints definitely cannot be erased: by
design their evidence carries a runtime value. Treating some constraints as non-erasable values and others (the equalities) as typelike, erasable constructs, led to many annoying special cases in the
type inference and source-to-FC elaboration of Haskell programs.
The most troublesome example of this non-uniformity arises when
treating Haskells superclasses. Consider the declaration
class (a F b, Eq a) C a b where . . .
Here Eq a is a superclass of C a b, meaning that from evidence for
C a b one can extract evidence for Eq a. Concretely this extraction
is witnessed by a field selector:
sc2 : C a b Eq a
Summary
There are many reasons why evidence-based type elaboration, using constraint generation and subsequent constraint solving, is desirable (Vytiniotis et al. 2011):
sc1 = ab . (d : C a b) .
case d of
MkC (c : a # F b) (eq : Eq a) . . . Eq# c
6.
Discussion
Evidence uniformity
We have mentioned that both equalities (# ) and () are kindpolymorphic, but we have not yet said why. Right from the beginning Haskell has featured kinds other than ?, such as ? ?. During
type inference, when unifying, say, Maybe Int, the inference
engine or, more precisely, the constraint solver must decompose the equality to give Maybe and Int. The former equality is at kind ? ?, so it follows that the () type constructor itself
must be either (a) magically built in or (b) poly-kinded. And similarly (# ).
Solution (a) is entirely possible: we could add and # to
the syntax of types, and give them their own kinding rules. But there
are unpleasant knock-on effects. The optimizer would need to be
taught how to optimize terms involving (). Worse, it turns out that
we need equalities between equalities, thus (1 1 ) (2 2 ),
which in turn leads to the need for new coercion combinators to
decompose such types.
Happily there are many other reasons for wanting kind polymorphism in FC (Yorgey et al. 2012), and once we have kind polymorphism we can readily make the equality type constructors kindpolymorphic.
6.3
f :: (Num b, a F b) a b b
then given a source-language call (f e1 e2 ), the type inference will
generate the elaborated call (f d c e1 e2 ), where and are the
types that instantiate a and b, and d and c are evidence terms that
witness that Num holds and that F , respectively.
One might wonder whether one can (in Haskell) also write
g :: (a # F b) a b b
7.2
7.
Optimizing equalities
T1 :: a . (a Int) Int T a
It would be perfectly sound to adopt the latter type for T1 in
the elaborated program; for example, function f from Section 3.2
would be elaborated thus:
f = a . (x : T a) .
case x of
T1 (c : a Int) (n : Int)
cast (Cons (n + 1) Nil) (mkSym [c])
T2 v Nil
Since an argument of type a Int has a lifted type with a boxed
representation, it would take up a whole word in every T1 object.
Moreover, since c is bound by the pattern match, the case expression in mkSym will not cancel with an Eq# box in the binding for c.
This is not good! What has become of our zero-overhead solution?
The solution is simple: we desugar GADTs to contain unlifted,
rather than lifted, equalities. We can do this in such a way that
the Haskell programmer still sees only the nice well-behaved ()
types, as follows. First, in the elaborated program the type of T1 is:
T1 : a . (a # Int) Int T a
However, the elaborator replaces every source-language call of T1
with a call of a constructor wrapper function, T1wrap, defined like
this:
T1wrap : a . (a Int) Int T a
T1wrap = (a : ?) . (c : a Int) . (n : Int) .
case c of Eq# c1 T1 c1 n
The wrapper deconstructs the evidence and puts the payload into
T1 where, since it is erasable, it takes no space.
Dually, a source-program pattern match is elaborated into a FC
pattern match together with code to re-box the coercion. So our
function f is elaborated thus:
f = a . (x : T a) .
case x of
T1 (c1 : a # Int) (n : Int)
f : a . F a Int [F a] Int
f = a . (c : F a Int) . (x : [F a]) .
case c of Eq# c0 fwrk c0 x
fwrk : a . F a # Int [F a] Int
fwrk = a . (c0 : F a # Int) . (x : [F a]) .
let c = Eq# c0 in head (cast x c) + 1
Now in fwrk the boxing and unboxing cancels; and dually we are
free to inline the wrapper function f at its call sites, where the
unboxing will cancel with the construction. This worker/wrapper
mechanism is precisely what GHC already implements to eliminate
boxing overheads on strict function arguments (Peyton Jones and
Santos 1998), so it too comes for free. There is a small price to pay,
however: the transformation makes the function strict in its equality
evidence, and that in turn might trigger a deferred error message
slightly earlier than strictly necessary. In our view this is a trade-off
worth making. In our current implementation the worker/wrapper
transform on equalities is only applied when the function really
is strict in the equality; we have not yet added the refinement of
making it strict in all equalities.
7.4
Summary
8.
Related work
8.1
Hybrid type checking (Flanagan 2006) refers to the idea of deferring statically unproved goals as runtime checks. Achieving similar effects, but arriving from the opposite end of the spectrum soft
typing tries to elimiminate statically as many runtime checks as
possible (Wright and Cartwright 1997). There are two differences
compared to our approach: First, in hybrid type checking typically
only unsolved goals will be deferred whereas insoluble ones will be
reported statically. In our case, insoluble and unsolved goals will be
deferred. Second, unsolved goals will be deferred as checks in hybrid type systems, whereas they will remain errors in our system:
Our treatment of coercions does not replace static type errors by
runtime checks, but rather delays triggering a static error until the
offending part of the program is evaluated, at runtime. For instance,
consider the following program, which contains a static error but is
compiled with -fdefer-type-errors:
f :: a . a a a
f x y = x && y
There is a static error in this program because f is supposed to
be polymorphic in the type of its arguments x and y, which are
nevertheless treated as having type Bool. At runtime, even if we
evaluate the application of f on arguments of type Bool, such as
f True False we will get a type error Couldnt match type a with
Bool, despite the fact that the arguments of f are of type Bool at
runtime. In contrast, a truly dynamic type-check would not trigger
a runtime error.
In the context of GHC, there is no straightforward way to incorporate runtime checks instead of error triggers at runtime, unless
dynamic type information is passed along with polymorphic types.
Though systems with dynamic types and coercions have been studied in the literature (Henglein 1994), we have not examined this
possibility.
There is a large body of work on interoperating statically and dynamically typed parts of a program, often referred to as gradual
typing (Ahmed et al. 2011; Siek and Taha 2006; Siek and Vachharajani 2008; Tobin-Hochstadt and Felleisen 2006). Typically, statically insoluble goals will be reported statically (Siek and Taha
2006), whereas insoluble goals which perhaps arise from the potential interoperation of dynamic and static parts of the program
will be wrapped with runtime checks. The main problem in gradual typing is to identify how to assign blame in case of a contract
violation (or a dynamic type error). We have seen in Section 5.3
that non-determinism in the dynamic placement of the type error
may well exist. Consequently it might be an interesting avenue to
explore if ideas from gradual typing could help us specify a more
predictable blame assignment for these deferred type errors. Note
finally that previous work on type error slicing (Haack and Wells
2004) has focused on identifying parts of a program that contribute
to a type error and would be potentially useful for reducing this
non-determinism both for static error messages and for better specifying the dynamic behaviour of an erroneous program.
8.2
Proof erasure
Coq (The Coq Team) uses a sort-based erasure process by introducing a special universe for propositions, Prop, which is analogous to
our Constraint# kind. Terms whose type lives in Prop are erased
even when they are applications of functions (lemmas) to computational terms. This is sound in Coq, since the computation language
is also strongly normalizing. Extending the computation language
of FC proofs or finding a way to restrict the ordinary computation
language of FC using kinds in order to allow it to construct primitive equalities is an interesting direction towards true dependent
types for Haskell.
Irrelevance-based erasure is another methodology proposed in the
context of pure type systems and type theory. In the context of Epigram, Brady et al. (2003) presented an erasure technique where
term-level indices of inductive types can be erased even when they
are deconstructed inside the body of a function, since values of the
indexed inductive datatype will be simultaneously deconstructed
and hence the indices are irrelevant for the computation. In the
Agda language (Norell 2007) there exist plans to adopt a similar
irrelevance-based erasure strategy. Other related work (Abel 2011;
Mishra-Linger and Sheard 2008) proposes erasure in the context
of PTSs guided with lightweight programmer annotations. There
also exist approaches that lie in between sort-based erasure and
irrelevance-based erasure: for instance, in implicit calculus of constructions (Miquel 2001) explicitly marked static information (not
necessarily Prop-bound) does not affect computation and can be
erased (Barras and Bernardo 2008). In FC the result of a computation cannot depend on the structure of an equality proof, by construction: there is no mechanism to decompose the structure of a
coercion at all at the term-level. Hence a coercion value needs no
structure (since it cannot be decomposed), which allows us to perform full erasure without any form of irrelevance analysis.
This idea of separating the computational part of a proof-like
object, which always has to run before we get to a zero-cost logical part is reminiscent of a similar separation that A-normal
forms introduce in refinement type systems, for instance (Bengtson et al. 2008) or the more recent work on value-dependent
types (Borgstrom et al. 2011; Swamy et al. 2011). This line of work
seems the closest in spirit to ours, with similar erasure concerns,
and there is rapidly growing evidence of the real-world potential
of these ideas see for instance the discussion and applications
reported by Swamy et al. (2011).
9.
Error coercion placement This paper has been about an implementation technique that uses first-class proof-like objects to al-
low for deferred type errors with very low overhead. A natural next
step would be towards a declarative specification of the elaboration process from source to a target language which specifies the
placement of the deferred error messages on potentially erroneous
sub-terms. Recent related work on coercion placement in the context of coercive subtyping is the work of Luo (2008) and Swamy
et al. (2009); these would certainly be good starting points for investigations on a declarative specification of deferring type errors.
The canonical reference for coercion placement in a calculus with
type-dynamic is the work of Henglein (1994), but it seems somewhat disconnected from our problem as we do not have currently
any way of dynamically passing type information or executing programs that contain static errors but are safe dynamically.
In general, this problem seems very hard to tackle without exposing some of the operation of the underlying constraint solver.
In the other direction, a principled approach to deferring type errors might actually provide guidance on the order in which constraints should be solved. For instance, when solving the constraints
C1 C2 C3 arising from the expressions e1 , e2 , and e3 in the term
if e1 then e2 else e3 , we might want to prioritise solving the constraint C1 . In this way, if an error is caused by the interaction of the
expressions e2 or e3 with e1 , we would still be able to execute the
condition of the branch e1 before we emit a deferred type error for
e2 or e3 . Otherwise we run the danger of the term e2 or e3 forcing
some unification that makes constraint C1 insoluble, giving rise to
an earlier error message (during evaluation of the condition term
e1 ). However, it is not clear what should happen when C2 and C3
have a common unification variable, and there is freedom in deferring either one, for instance. Therefore this problem is certainly
worth further investigation.
Conclusions In this paper we have proposed a simple and lightweight mechanism for deferring type errors, in a type-safe way that
requires no program rewriting, and preserves the semantics of the
program until execution reaches the part that contains a type error.
We have shown that this can be done in an entirely safe way in the
context of a typed intermediate language, and in fact without requiring any modifications to System FC or the compiler optimizer.
This work is fully implemented in GHC, where it has in addition
greatly simplified the implementation of type inference and elaboration of Haskell to FC .
Acknowledgments
Particular thanks are due to Etienne Laurin, who suggested to us
the idea of deferring type errors (GHC Trac ticket 5624), although
his implementation was very different to the one described here.
We thank Stephanie Weirich and Brent Yorgey for their detailed
comments and suggestions, and the ICFP reviewers for the helpful
feedback.
This work has been partially funded by the Portuguese Foundation
for Science and Technology (FCT) via the SFRH/BD/35999/2007
grant, and by EPSRC grant number EP/J010995/1.
References
Andreas Abel. Irrelevance in type theory with a heterogeneous equality
judgement. In Foundations of Software Science and Computational
Structures, 14th International Conference, FOSSACS 2011, pages 57
71. Springer, 2011.
Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler.
Blame for all. In Proceedings of the 38th annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL
11, pages 201214, New York, NY, USA, 2011. ACM. ISBN 978-14503-0490-0. doi: 10.1145/1926385.1926409.
Bruno Barras and Bruno Bernardo. The implicit calculus of constructions
as a programming language with dependent types. In Foundations of
Software Science and Computation Structure, pages 365379, 2008. doi:
10.1007/978-3-540-78499-9 26.
Michael Bayne, Richard Cook, and Michael Ernst. Always-available static
and dynamic feedback. In Proceedings of 33rd International Conference
on Software Engineering (ICSE11), pages 521530, Hawaii, 2011.
Jesper Bengtson, Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, and Sergio Maffeis. Refinement types for secure implementations.
In Proceedings of the 2008 21st IEEE Computer Security Foundations
Symposium, pages 1732, Washington, DC, USA, 2008. IEEE Computer
Society. ISBN 978-0-7695-3182-3.
Johannes Borgstrom, Juan Chen, and Nikhil Swamy. Verifying stateful
programs with substructural state and Hoare types. In Proceedings of
the 5th ACM Workshop on Programming Languages meets Program
Verification, PLPV 11, pages 1526, New York, NY, USA, 2011. ACM.
ISBN 978-1-4503-0487-0.
Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda a
functional language with dependent types. In TPHOLs 09: Proceedings
of the 22nd International Conference on Theorem Proving in Higher
Order Logics, pages 7378, Berlin, Heidelberg, 2009. Springer-Verlag.
Edwin Brady, Conor McBride, and James McKinna. Inductive families
need not store their indices. In Stefano Berardi, Mario Coppo, and
Ferruccio Damiani, editors, TYPES, volume 3085 of Lecture Notes in
Computer Science, pages 115129. Springer, 2003.
Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. Associated type synonyms. In ICFP 05: Proceedings of the Tenth ACM
SIGPLAN International Conference on Functional Programming, pages
241253, New York, NY, USA, 2005. ACM.
James Cheney and Ralf Hinze. First-class phantom types. CUCIS TR20031901, Cornell University, 2003.
Cormac Flanagan. Hybrid type checking. In Proceedings of the 33rd
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 06, pages 245256, New York, NY, USA, 2006.
ACM. doi: 10.1145/1111037.1111059.
Matthew Gertz. Scaling up: The very busy background compiler. MSDN
Magazine, 6 2005. URL http://msdn.microsoft.com/en-us/
magazine/cc163781.aspx.
Christian Haack and J. B. Wells. Type error slicing in implicitly typed
higher-order languages. Science of Computer Programming, 50:189
224, March 2004. ISSN 0167-6423.
Fritz Henglein. Dynamic typing: syntax and proof theory. Science of
Computer Programming, 22:197230, June 1994. ISSN 0167-6423.
Oleg Kiselyov, Simon Peyton Jones, and Chung-chieh Shan. Fun with
type functions. In A.W. Roscoe, Cliff B. Jones, and Kenneth R.
Wood, editors, Reflections on the Work of C.A.R. Hoare, History of
Computing, pages 301331. Springer London, 2010. doi: 10.1007/
978-1-84882-912-1 14.
Ralf Lammel and Simon Peyton Jones. Scrap your boilerplate with class:
extensible generic functions. In Proceedings of the 10th ACM SIGPLAN
International Conference on Functional Programming, ICFP 05, pages
204215, New York, NY, USA, 2005. ACM. doi: 10.1145/1086365.
1086391.
Daniel R. Licata and Robert Harper. A formulation of dependent ML with
explicit equality proofs. Technical Report CMU-CS-05-178, Carnegie
Mellon University Department of Computer Science, 2005.
Daniel R. Licata and Robert Harper. Canonicity for 2-dimensional type
theory. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 12, pages
337348, New York, NY, USA, 2012. ACM. doi: 10.1145/2103656.
2103697.
Zhaohui Luo. Coercions in a polymorphic type system. Mathematical
Structures in Computer Science, 18(4):729751, August 2008. ISSN
0960-1295. doi: 10.1017/S0960129508006804.
Alexandre Miquel. The implicit calculus of constructions: extending pure
type systems with an intersection type binder and subtyping. In Proceedings of the 5th International Conference on Typed Lambda Calculi
and Applications, TLCA01, pages 344359, Berlin, Heidelberg, 2001.
Springer-Verlag. ISBN 3-540-41960-8.
Nathan Mishra-Linger and Tim Sheard. Erasure and polymorphism in
pure type systems. In Roberto Amadio, editor, Foundations of Software
Science and Computational Structures, volume 4962 of Lecture Notes in
Computer Science, pages 350364. Springer Berlin / Heidelberg, 2008.
Ulf Norell. Towards a practical programming language based on dependent
type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007.
Simon Peyton Jones and John Launchbury. Unboxed values as first class
citizens in a non-strict functional programming language. In FPCA91:
Conference on Functional Programming Languages and Computer Architecture, pages 636666, New York, NY, August 1991. ACM Press.
Simon Peyton Jones and Andre Santos. A transformation-based optimiser
for Haskell. Science of Computer Programming, 32(1-3):347, September 1998.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey
Washburn. Simple unification-based type inference for GADTs. In
Proceedings of the 11th ACM SIGPLAN International Conference on
Functional Programming, pages 5061, New York, NY, USA, 2006.
ACM Press. ISBN 1-59593-309-3.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields. Practical type inference for arbitrary-rank types. Journal of Functional Programming, 17(01):182, 2007. doi: 10.1017/
S0956796806006034.
Benjamin C. Pierce and David N. Turner. Local type inference. ACM Transactions on Programming Languages and Systems, 22(1):144, January