System F with Type Equality Coercions
Martin Sulzmann
School of Computing National University of Singapore sulzmann@comp.nus.edu.sg Manuel M.T.Chakravarty
人才培养计划Computer Science&Engineering
University of New South Wales
chak@c.unsw.edu.au
Simon Peyton Jones Kevin Donnelly
Microsoft Rearch Ltd
Cambridge,England
{simonpj,t-kevind}@
Abstract
We introduce System F C,which extends System F with support for non-syntactic type equality.There are two main extensions:(i) explicit witness for type equalities,and(ii)open,non-parametric type functions,given meaning by top-level equality axioms.Unlike System F,F C is expressive enough to rve as a target for veral different source-language features,including Haskell’s newtype, generalid algebraic data types,associated types,functional de-pendencies,and perhaps more besides.
Categories and Subject Descriptors D.3.1[Programming Lan-guages]:Formal Definitions and Theory—Semantics; F.3.3[Log-ics and Meanings of Programs]:Studies of Program Constructs—Type structure
General Terms Languages,Theory
Keywords Typed intermediate language,advanced type features
xxx699
1.Introduction
The polymorphic lambda calculus,System F,is popular as a highly-expressive typed intermediate language in compilers for functional languages.However,language designers have begun to experim
ent with a variety of type systems that are difficult or impossible to translate into System F,such as functional dependencies[21],gen-eralid algebraic data types(GADTs)[43,31],and associated types[6,5].For example,when we added GADTs to GHC,we extended GHC’s intermediate language with GADTs as well,even though GADTs are arguably an over-sophisticated addition to a typed intermediate language.But when it came to associated types, even with this richer intermediate language,the translation became extremely clumsy or in places impossible.
In this paper we resolve this problem by prenting System F C(X), a super-t of F that is both more foundational and more powerful than adding ad hoc extensions to System F such as GADTs or as-sociated types.F C(X)us explicit type-equality coercions as wit-ness to justify explicit type-cast operations.Like types,coercions are erad before running the program,so they are guaranteed to have no run-time cost.苟同
This single mechanism allows a very direct encoding of associ-ated types and GADTs,and allows us to deal with some exotic functional-dependency programs that GHC currently rejects on the grounds that they have no System-F translation(§2).Our specific contributions are the:
Permission to make digital or hard copies of all or part of this work for personal or classroom u is g
ranted 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 thefirst page.To copy otherwi,to republish,to post on rvers or to redistribute to lists,requires prior specific permission and/or a fee.
TLDI’07January16,2007,Nice,France.
Copyright c 2007ACM1-59593-393-X/$5.00.
•We give a formal description of System F C,our new intermedi-ate language,including its type system,operational mantics, soundness result,and erasure properties(§3).There are two dis-tinct extensions.Thefirst,explicit equality witness,gives a system equivalent in power to System F+GADTs(§3.2);the cond introduces non-parametric type functions,and adds sub-stantial new power,well beyond System F+GADTs(§3.3).•A distinctive property of F C’s type functions is that they are open(§3.4).Here we u“open”in the same n that Haskell type class are open:just as a newly defined type can be made an instance of an existing class,so in F C we can extend an existing type function with a ca for the new type.This property is crucial to the translation of associated types.•The system is very general,and its soundness requires that the axioms stated as part of the program text are consistent(§3.5).
That is why we call the system F C(X):the“X”indicates that it is parametrid over a decision procedure for checking con-sistency,rather than baking in a particular decision procedure.
(We often omit the“(X)”for brevity.)Conditions identified in earlier work on GADTs,associated types,and functional de-pendencies,already define such decision procedures.
•A major goal is that F C should be a practical compiler inter-mediate language.We have paid particular attention to ensuring that F C programs are robust to program transformation(§3.8).•It must obviously be possible to translate the source language into the intermediate language;but it is also highly desirable that it be straightforward.We demonstrate that F C has this property,by sketching a type-prerving translation of two source language idioms,namely GADTs(Section4)and as-sociated types(Section5).The latter,and the corresponding translation for functional dependencies,are more general than all previous type-prerving translations for the features.
System F C has no new foundational content:rather,it is an intrigu-ing and practically-uful application of techniques that have been well studied in the type-theory community.Several other calculi exist that might in principle be ud for our purpo,but they gen-erally do not handle open type functions,are less robust to trans-formation,and are significantly more complicated.We defer a com-parison with related work until§6.
To substantiate our claim that F C is practical,we have implemented it in GHC,a state-of-the-art compiler for Haskell,including both GADTs and associated(data)types.This is not just a prototype;
F C now is GHC’s intermediate language.
F C does not strive to do everything;rather we hope that it strikes an elegant balance between expressiveness and complexity.While our motivating examples were GADTs and associated types,we believe that F C may have much wider application as a typed target for sophisticated HOT(higher-order typed)source languages.
2.The key ideas
No compiler us pure System F as an intermediate language, becau some source-language constructs can only be desugared into pure System F by very heavy encodings.A good example is the algebraic data types of Haskell or ML,which are made more complicated in Haskell becau algebraic data types can capture existential type variables.To avoid heavy encoding,most compilers invariably extend System F by adding algebraic data types,data constructors,and ca expressions.We will u F A to describe System F extended in this way,where the data constructors are allowed to have existential components[24],type variables can be of higher kind,and type constru
ctor applications can be partial. Over the last few years,source languages(notably Haskell)have started to explore language features that embody non-syntactic or definitional type equality.The features include functional depen-dencies[16],generalid algebraic data types(GADTs)[43,36], and associated types[6,5].All three are difficult or impossible to translate into System F—and yet the alternative of simply ex-tending System F by adding functional dependencies,GADTs,and associated types,ems wildly unattractive.Where would one stop? In the rest of this ction we informally prent System F C,an extension of System F that resolves the dilemma.We show how it can rve as a target for each of the three examples.The formal details are prented in§3.Throughout we u typewriter font for source-code,and italics for F C.
2.1GADTs
Consider the following simple type-safe evaluator,often ud as the poster child of GADTs,written in the GADT extension of Haskell supported by GHC:
data Exp a where
Zero::Exp Int
Succ::Exp Int->Exp Int
Pair::Exp b->Exp c->Exp(b,c)
eval::Exp a->a
eval Zero=0
eval(Succ e)=eval e+1
eval(Pair x y)=(eval x,eval y)
main=eval(Pair(Succ Zero)Zero)
The key point about this program,and the aspect that is hard to express in System F,is that in the Zero branch of eval,the type variable a is the same as Int,even though the two are syntactically quite different.That is why the0in the Zero branch is well-typed in a context expecting a result of type a.
Rather than extend the intermediate language with GADTs them-lves—GHC’s pre-F C“solution”—we instead propo a gen-eral mechanism of parameterising functions with type equalities, writtenσ1∼σ2,witnesd by coercions.Coercion types are pasd around using System F’s existing type passing facilities and enable reprenting GADTs by ordinary algebraic data types encapsulat-ing such type equality coercions.
Specifically,we translate the GADT Exp to an ordinary algebraic data type,where each variant is parametrid by a coercion: data Exp:⋆→⋆where
Zero:∀a.(a∼Int)⇒Exp a
Succ:∀a.(a∼Int)⇒Exp Int→Exp a
Pair:∀abc.(a∼(b,c))⇒Exp b→Exp c→Exp a So far,this is quite standard;indeed,veral authors prent GADTs in the source language using a syntax involving explicit equality constraints,similar to that above[43,10].However,for us the equality constraints are extra type arguments to the constructor,which must be given when the constructor is applied,and which are brought into scope by pattern matching.The“⇒”is syntac-tic sugar,and we sloppily omitted the kind of the quantified type variables,so the type of Zero is really this:
Zero:∀a:⋆.∀(co:a∼Int).Exp a
Here a ranges over types,of kind⋆,while co ranges over coercions, of kind a∼Int.An important property of our approach is that coercions are types,and hence,equalitiesτ1∼τ2are kinds.An equality kindτ1∼τ2categoris all coercion types that witness
the interchangeability of the two typesτ1andτ2.So,our slogan is propositions as kinds,and proofs as(coercion)types.
Coercion types may be formed from a t of elementary coer-cions that correspond to the rules of equational logic;for example, Int:(Int∼Int)is an instance of the reflexivity of equality and sym co:(Int∼a),with co:(a∼Int),is an instance of symme-try.A call of the constructor Zero must be given a type(to instan-tiate a)and a coercion(to instantiate co),thus for example: Zero Int Int:Exp Int
As indicated above,regular types like Int,when interpreted as coercions,witness reflexivity.
Just like value arguments,the coercions pasd to a constructor when it is built are made available again by pattern matching.Here, then,is the code of eval in F C:
eval=Λa:⋆.λe:Exp a.
ca e of
Zero(co:a∼Int)→
0◮sym co
Succ(co:a∼Int)(e′:Exp Int)→
(eval Int e′+1)◮sym co
Pair(b:⋆)(c:⋆)(co:a∼(b,c))
(e1:Exp b)(e2:Exp c)→
(eval b e1,eval c e2)◮sym co
The formΛa:⋆.e abstracts over types,as usual.In thefirst al-ternative of the ca expression,the pattern binds the coercion type argument of Zero to co.We u the symmetry of equality in(sym co)to get a coercion from Int to a and u that to cast the type of0to a,using the cast expression0◮sym co.Cast expres-sions have no operational effect,but they rve to explain to the type system when a value of one type(here Int)should be treated as another(here a),and provide evidence for this equivalence.In general,the form e◮g has type t2if e:t1and g:(t1∼t2). So,eval Int(Zero Int Int))is of type Int as required by eval’s signature.We shall discuss coercion types and their kinds in more detail in§3.2.
In a similar manner,the recently-propod extended algebraic data types[40],which add equality and
predicate constraints to GADTs, can be translated to F C.
2.2Associated types
Associated types are a recently-propod extension to Haskell’s type-class mechanism[6,5].They offer open,type-indexed types that are associated with a type class.Here is a standard example: class Collects c where
type Elem c--associated type synonym
empty::c
inrt::Elem c->c->c
礼仪主持人The class Collects abstracts over a family of containers,where the reprentation type of the container,c,defines(or constrains) the type of its elements Elem c.That is,Elem is a type-level func-tion that transforms the collection type to the element type.Just as inrt is non-parametric–its implementation varies depend-ing on c–so is Elem.For example,a list container can contain
elements of any type supporting equality,and a bit-t container might reprent a collection of characters:
instance Eq e=>Collects[e]where
{type Elem[e]=e;...}
instance Collects BitSet where
{type Elem BitSet=Char;...}
Generally,type class are translated into System F[17]by(1)turn-ing each class into a record type,called a dictionary,contain-ing the class methods,(2)converting each instance into a dic-tionary value,and(3)passing such dictionaries to whichever function mentions a class in its signature.For example,a func-tion of type negate::Num a=>a->a will translate to negate:NumDict a→a→a,where NumDict is the record generated from the class Num.
A record only encapsulates values,so what to do about associ-ated types,such as Elem in the example?The system given in [6]translates each associated type into an additional type param-eter of the class’s dictionary type,provided the class and instance declarations abide by some moderate constraints[6].For example, the class Collects translates to dictionary type CollectsDict c e, where e reprents Elem c and where all occurrences of Elem c of the method signatures have been replace
d by the new type parameter e.So,the(System F)type for inrt would now be CollectDict c e→e→c→c.The required type transforma-tions become more complex when associated types occur in data types;the data types have to be rewritten substantially during trans-lation,which can be a considerable burden in a compiler.
给我希望Type equality coercions enable a far more direct translation.Here is the translation of Collects into F C:
type Elem:⋆→⋆
data CollectsDict c=
Collects{empty:c;inrt:Elem c→c→c} The dictionary type is as in a translation without associated types. The type declaration in F C introduces a new type function.An instance declaration for Collects is translated to(a)a dictionary transformer for the values and(b)an equality axiom that describes (part)of the interpretation for the type function Elem.For example, here is the translation into F C of the Collects Bitt instance: axiom elemBS:Elem BitSet∼Char
dCollectsBS:CollectsDict Bitt
dCollectsBS=...
The axiom definition introduces a new,named coercion constant, elemBS,which rves as a witness of the equality asrted by the axiom;here,that we can convert between types of the form Elem BitSet and Char.Using this coercion,we can inrt the character’b’into a BitSet by applying the coercion elemBS backwards to’b’,thus:
(’b’◮(sym elemBS)):Elem BitSet
This argumentfits the signature of inrt.
In short,System F C supports a very direct translation of associated types,in contrast to the clumsy one described in[6].What is more, there are veral obvious extensions to the latter paper that cannot be translated into System F at all,even clumsily,and F C supports them too,as we sketch in Section5.
2.3Functional dependencies
Functional dependencies are another popular extension of Haskell’s type-class mechanism[21].With functional dependencies,we can encode a function over types F as a relation,thus
class F a b|a->b
instance F Int Bool However,some programs involving functional dependencies are impossible to translate into System F.For example,a uful idiom in type-level programming is to abstract over the co-domain of a type function by way of an existential type,the b in this example: data T a=forall b.F a b=>MkT(b->b)
In this Haskell declaration,MkT is the constructor of type T,captur-ing an existential type variable b.One might hope that the following function would type-check:
combine::T a->T a->T a
combine(MkT f)(MkT f’)=MkT(f.f’)
After all,since the type a functionally determines b,f and f’must have the same type.Yet GHC rejects this program,becau it cannot be translated into System F A,becau f and f’each have distinct,existentially-quantified types,and there is no way to express their(non-syntactic)identity in F A.
It is easy to translate this example into F C,however:
type F1:⋆→⋆
data FDict:⋆→⋆→⋆where
F:∀a b.(b∼F1a)⇒FDict a b
axiom fIntBool:F1Int∼Bool
data T:⋆→⋆where
MkT:∀a b.FDict a b→(b→b)→T a
combine:T a→T a→T a
combine(MkT b(F(co:b∼F1a))f)
(MkT b′(F(co′:b′∼F1a))f′)
=MkT a b(F a b co)(f.(f′◮d2))
where
d1:(b′∼b)=co′◦sym co
d2:(b′→b′∼b→b)=d1→d1
The functional dependency is expresd as a type function F1,with one equality axiom per instance.(In general there might be many functional dependencies for a single class.)The dictionary for class F includes a witness that indeed b is equal to F1a,as you can e from the declaration of constructor F.When pattern matching in combine,we gain access to the witness,and can u them to cast f′so that it has the same type as f.(To construct the witness d1we u the coercion combinators sym·and·◦·,which reprent symmetry and transitivity;and from d1we build the witness d2.) Even in the abnce of existential types,there are reasonable source programs involving functional dependencies that have no System F translation,and hence are rejected by GHC.We have encountered this problem in real programs,but here is a boiled-down example, using the same class F as before:
class D a where{op::F a b=>a->b}
instance D Int where{op_=True}
The crucial point is that the context F a b of the signature of op constrains the parameter of the enclosing type class D.This be-comes a problem when typing the definition of op in the instance D Int.In D’s dictionary DDict,we have op:∀b.C a b→a→b with b universally quantified,but in the instance declaration,we would need to instantiate b with Bool.The instance declaration for D cannot be translated into System F.Using F C,this problem is easily solved:the coercion in the dictionary for F enables the result of op to be cast to type b as required.
To summari,a compiler that us translation into System F(or F A)must reject some reasonable(albeit slightly exotic)programs involving functional dependencies,and also similar programs in-volving associated types.The extra expressiveness of System F C solves the problem neatly.
2.4Translating newtype
F C is extremely expressive,and can support language features be-yond tho we have discusd so far.Another example are Haskell 98’s newtype declarations:
newtype T=MkT(T->T)
In Haskell,this declares T to be isomorphic to T->T,but there is no good way to express that in System F.In the past,GHC has handled this with an ad hoc hack,but F C allows it to be handled directly,
by introducing a new axiom
axiom CoT:(T→T)∼T
2.5Summary
In this ction we have shown that System F is inadequate as a typed intermediate language for source languages that embody non-syntactic type equality—and Haskell has developed veral such extensions.We have sketchily introduced System F C as a solution to the difficulties.We will formali it in the next ction.
3.System F C(X)
The main idea in F C(X)is that we pass around explicit evidence for type equalities,in just the same way that System F pass types explicitly.Indeed,in F C the evidenceγfor a type equality is a type;we u type abstraction for evidence abstraction,and type application for evidence application.Ultimately,
we era all types before running the program,and thereby era all type-equality evidence as well,so the evidence passing has no run-time cost. However,that is not the only reason that it is better to reprent evidence as a type rather than as a term,as we discuss in§3.10. Figure1defines the syntax of System F C,while Figures2and3 give its static mantics.The notation
a n,a n+1
decl;e
decl→data T:
K:∀b:ι.a
|type S n:
ϕn|∀a:κ.ϕ
|symγ|γ1◦γ2|γ@ϕ|leftγ|rightγ
|γ∼γ|rightcγ|leftcγ|γ◮γ
We uρ,σ,τ,andυfor regular types,γfor coercions,andϕfor both. Syntactic sugar
Typesκ⇒σ≡∀
p→e2
|e◮γCast
p→K x:σPattern
Environments
Γ→ǫ|Γ,u:σ|Γ,d:κ|Γ,g:κ|Γ,S n:κ
A top-level environment binds only type constructors,
T,S n,data constructors K,and coercion constants C.
Figure1:Syntax of System F C(X)
sometimes u the following syntactic sugar:
αn.ϕ≡∀α1···∀αn.ϕ
An algebraic data type T is introduced by a top-level data dec-laration,which also introduces its data constructors.The type of a data constructor K takes the form
K:∀b:ι.a n
Thefirst n quantified type variables
a.The remaining quantified type variables bind either existentially quantified type variables,or(as we shall e) coercions.
Types are classified by kindsκ,using the⊢TY judgement in Fig-ure2.Temporarily ignoring the kindσ1∼σ2,the structure of kinds
Γ⊢TYσ:κ
(TyVar)d:κ∈ΓΓ⊢kκ:TY
Γ⊢TYσ1σ2:κ2
(TySCon)(S n:σ:κn
σn:ι
(TyAll)
Γ,a:κ⊢TYσ:⋆Γ⊢kκ:δa∈fv(Γ)Γ⊢CO a:a∼a
(CoVar)
g:σ∼τ∈Γ
Γ⊢CO∀a:κ.γ:∀a:κ.σ∼∀a:κ.τ
(CoInstT)
Γ⊢COγ:∀a:κ.σ∼∀b:κ.τ
Γ⊢TYυ:κ
γ:σ∼τnΓ⊢TY S n
Γ⊢CO S nσn∼S nΓ⊢CO symγ:τ∼σ(Trans)
Γ⊢COγ1:σ1∼σ2
Γ⊢COγ2:σ2∼σ3
Γ⊢COγ1γ2:σ1σ2∼τ1τ2(Left)
Γ⊢COγ:σ1σ2∼τ1τ2
Γ⊢CO rightγ:σ2∼τ2
(CompC)Γ⊢COγ:κ1∼κ2Γ⊢COγ′:σ1∼σ2
Γ⊢kκ1:CO
Γ⊢CO leftcγ:κ1∼κ2
(RightC)
Γ⊢COγ:
κ1⇒σ1
∼
κ2⇒σ2Γ⊢COγ1∼γ2:(σ1∼σ2)∼(τ1∼τ2)遥控飞机怎么玩
(CastC)
Γ⊢COγ1:κΓ⊢COγ2:κ∼κ′
Γ⊢e u:σ
(Ca)
Γ⊢e e:σ
Γ⊢e ca e ofΓ⊢e let x:σ1=e1in e2:σ2
(Cast)
Γ⊢e e:σΓ⊢COγ:σ∼τ
Γ⊢eλx:σx.e:σx→σ(App)
Γ⊢e e1:σ2→σ1
Γ⊢e e2:σ2
Γ⊢eΛa:κ.e:∀a:κ.σ(AppT)
Γ⊢e e:∀a:κ.σΓ⊢kκ:δΓ⊢δϕ:κ
经常出差a:κ.∀σ→Tυ/a]Γ,x:θ(σ)⊢e e:τ
b:θ(ι)υ→τ
Γ⊢decl:Γ′
(Data)
Γ⊢(data T:κwhere K:σ)
(Type)Γ⊢kκ:TY
Γ⊢(axiom C:κ):(C:κ)
Γ⊢pgm:σ
(Pgm)
Γd
Γ⊢e:σ
decl;e:σ
Figure2:Typing rules for System F C(X)
Γ⊢kκ:δ
(Star)
Γ⊢kκ1→κ2:TY
(EqTy)
Γ⊢TYσ1:κΓ⊢TYσ2:κ
Γ⊢kγ1∼γ2:CO
Figure3:Kinding rules for System F C(X)
is conventional:⋆is the kind of proper types(that is,the types that a term can have),while higher kinds take the formκ1→κ2.Kinds guide type application by way of Rule(TyApp).Finally,the rules for judgements of the formΓ⊢kκ:δ,given in Figure3,ensure the well-formedness of kinds.Hereδis either TY for kinds formed from arrows and⋆,or CO for coercion kinds of formσ1∼σ2.The conclusions of Rule(EqTy)and(EqCo)appear to overlap,but an actual implementation can deterministically decide which rule to apply,choosing(EqCo)iffγ1has the formϕ1∼ϕ2.
The syntax of terms is largely conventional,as are their type rules which take the formΓ⊢e e:σ.As in F,every binder has an explicit type annotation,and type abstraction and application are also explicit.There is a ca expression to take apart values built with data constructors.The patterns of a ca expression areflat—there are no nested patterns—and bind existential type variables, coercion variables,and value variables.For example,suppo K:∀a:⋆.∀b:⋆.a→b→(b→Int)→T a
一般的床垫多少钱Then a ca expression that deconstructs K would have the form ca e of K(b:⋆)(v:a)(x:b)(f:b→Int)→e′
Note that only the existential type variable b is bound in the pattern. To e why,one need only reali that K’s type is isomorphic to: K:∀a:⋆.(∃b:⋆.(a,b,(b→Int)))→T a
3.2Type equality coercions
We now describe the unconventional features of our system.To begin with,consider the fragment of System F C that omits type ,type and axiom declarations).This fragment is sufficient to rve as a target for translating GADTs,and so is of interest in its own right.We return to type functions in§3.3.
The esntial addition to plain F(beyond algebraic data types and higher kinds)is an infrastructure to construct,pass,and apply type-equality coercions.In F C,a coercion,γ,is a special sort of type who kind takes the unusual formσ1∼σ2.We can u such a coercion to cast an expression e:σ1to typeσ2using the cast expression(e◮γ);e Rule(Cast)in Figure2.Our intuition for equality coercions is an extensional one:
γ:σ1∼σ2is evidence that a value of typeσ1can be ud
in any context that expects a value of typeσ2,and vice
versa.
By“can be ud”,we mean that running the program after type erasure will not go wrong.We stress that this is only an intuition; the soundness of our system is proved without appealing to any mantic notion of whatσ1∼σ2“means”.We u the symbol “∼”rather than“=”,to avoid suggesting that the two types are intensionally equal.
Coercions are types–some would call them“constructors”[25,12] since they certainly do not have kind⋆—and hence the term-level syntax for type abstraction and application(Λa.e and eϕ)also rves for coercion abstraction and application.However,coercions have their own kinding judgement⊢CO,given in Figure2.The type of a term often has the form∀co:(σ1∼σ2).ϕ,whereϕdoes not mention co.We allow the standard syntactic sugar for this ca, writing it thus:(σ1∼σ2)⇒ϕ(e Figure1).Incidentally,note
that although coercions are types,they do not classify values.This is standard in Fω;for example,there are no values who type has kind⋆→⋆.
More complex coercions can be built by combining or transform-ing other coercions,such that every syntactic form corresponds to an inference rule of equational logic.We have the reflexivity of equality for a given typeσ(witnesd by the type itlf),symme-try‘symγ’,transitivity‘γ1◦γ2’,type composition‘γ1γ2’,and decomposition‘leftγ’and‘rightγ’.The typing rules for the coercion expressions are given in Figure2.
Here is an example,taken from§2.Suppo a GADT Expr has a constructor Succ with type
Succ:∀a:⋆.(a∼Int)⇒Exp Int→Exp a
(notice the u of the syntactic sugarκ⇒σ).Then we can con-struct a value of type Exp Int thus:Succ Int Int e.The c-ond argument Int is a regular type ud as a coercion witness-ing reflexivity—i.e.,we have Int:(Int∼Int)by Rule(CoRefl). Rule(CoRefl)itlf only covers type variables and constructors, but in combination with Rule(Comp),the reflexivity of complex types is also covered.More interestingly,here is a function that decompos a value of type Exp a:
foo:∀a:⋆.Exp a→a→a
=Λa:⋆.λe:Exp a.λx:a.
ca e of
Succ(co:a∼Int)(e′:Exp Int)→
(foo Int e′0+(x◮co))◮sym co
The ca pattern binds the coercion co,which provides evidence that a and Int are the same type.This evidence is needed twice, once to cast x:a to Int,and once to coerce the Int result back to a,via the coercion(sym co).
Coercion composition allows us to“lift”coercions through arbi-trary types,in the style of logical relations[1].For example,if we have a coercionγ:(σ1∼σ2)then the coercion Treeγis ev-idence that Treeσ1∼Treeσ2,using rules(Comp)and(CoRefl) and(CoVar).More generally,our system has the following theo-rem.
T HEOREM1(Lifting).IfΓ′⊢COγ:σ1∼σ2andΓ⊢TYϕ:κ, thenΓ′⊢CO[γ/a]ϕ:[σ1/a]ϕ∼[σ2/a]ϕ,for any typeϕ,including polytypes,whereΓ=Γ′,a:κ′such that a does not appear inΓ′. For example,ifγ:σ1∼σ2then
∀b.γ→Int:(∀b.σ1→Int)∼(∀b.σ2→Int) Dually decomposition enables us to take evidence apart.For ex-
ample,assumeγ:Treeσ1∼Treeσ2;then,(rightγ)is evidence thatσ1∼σ2,by rule(Right).Decomposition is necessary for the translation of GADT programs to F C,but is problematic in ear-lier approaches[3,9].The soundness of decomposition relies,of cour,on algebraic types being ,Treeσ1=Treeσ2 iffσ1=σ2.Notice,too,that Tree by itlf is a coercion relating two types of higher kind.
Similarly,one can compo and decompo equalities over poly-types,using rules(CoAllT)and(CoInstT).For example,
