WIXLIB

GADT meet subtyping6contravariant), and arrow types are not upward-closed as their domain should bedownward-closed. Only purely positive algebraic datatypes are upward-closed. Thesubset of GADT declarations that can be declared covariant today is small, yet, wethink, large enough to capture a lot of useful examples, such as α expr above.Giving back the freedom of subtypingIt is disturbing that the type system should rely on non-monotonic properties: ifwe adopt the correctness criterion above, we must be careful in the future not toenrich the subtyping relation too much.Consider private types for example: one could imagine a symmetric conceptof a type that would be strictly above a given type τ ; we will name those typesinvisible types (they can be constructed, but not observed). Invisible types andGADT covariance seem to be working against each other: if the designer adds one,adding the other later will be difficult.A solution to this tension is to allow the user to locally guarantee negativeproperties about subtyping (what is not a subtype), at the cost of selectively abandoning the corresponding flexibility. Just as object-oriented languages have finalclasses that cannot be extended any more, we would like to be able to define sometypes as public (respectively visible), that cannot later be made private (resp.invisible). Such declarations would be rejected if the defining type already hassubtypes (e.g. an object type), and would forbid further declarations of types below(resp. above) the defined type, effectively guaranteeing downward (resp. upward)closure. Finally, upward or downward closure is a semantic aspect of a type thatwe must have the freedom to publish through an interface: abstract types couldoptionally be declared public or visible.Another approach: subtyping constraintsGetting fine variance properties out of GADT is difficult because they correspondto type equalities which, to a first approximation, use their two operands bothpositively and negatively. One way to get an easy variance check is to encourageusers to change their definitions into different ones that are easier to check. Forexample, consider the following redefinition of α expr (in a speculative extensionof OCaml with subtyping constraints):type α expr Val : α.α α expr Int : α[α int].int α expr Thunk : β. β expr (β α) α expr Prod : αβγ[α β γ]. (β expr γ expr) α exprIt is now quite easy to check that this definition is covariant, since all type equalitiesα Ti [β] have been replaced by inequalities α Ti [β] which are preserved whenreplacing α by a subtype α0 α—we explain this more formally in §4.3. This variation on GADT, using subtyping instead of equality constraints, has been studiedby Emir et al [EKRY06] in the context of the C] programming language.But isn’t such a type definition less useful than the previous one, which had astronger constraint? We will discuss this choice in more detail in §4.3.a “closed world” and we can check, for example, that they are never used in a private typedefinition.

GADT meet subtyping7On the importance of variance annotationsBeing able to specify the variance of a parametrized datatype is important at abstraction boundaries: one may wish to define a program component relying on anabstract type, but still make certain subtyping assumptions on this type. Varianceassignments provide a framework to specify such a semantic interface with respectto subtyping. When this abstract type dependency is provided by an encapsulatedimplementation, the system must check that the provided implementation indeedmatches the claimed variance properties.Assume the user specifies an abstract typemodule typetype ( α)val emptyval app :endS sigcollection: unit - α collectionα collection - α collection - α collectionand then implements it with linked listsmodule C : S structtype α collection Nil of unit Cons of α α collectionlet empty () Nil ()endThe type-checker will accept this implementation, as it has the specified variance.On the contrary,type α collection (α list) reflet empty () ref []would be rejected, as ref is invariant. In the following definition:let nil C.empty ()the right hand-side is not a value, and is therefore not generalized in presence of thevalue restriction; we get a monomorphic type, ?α t, where ?α is a yet-undeterminedtype variable. The relaxed value restriction [Gar04] indicates that it is sound togeneralize ?α, as it only appears in covariant positions. Informally, one may unify?α with , add an innocuous quantification over α, and then generalize α. tinto α.α t by covariance—assuming a lifting of subtyping to polymorphic typeschemes.The definition of nil will therefore get generalized in presence of the relaxedvalue restriction, which would not be the case if the interface S had specified aninvariant type.Related workWhen we encountered the question of checking variance annotations on GADT, weexpected to find it already discussed in the literature. The work of Simonet andPottier [SP07] is the closest we could find. It was done in the context of findinggood specification for type inference of code using GADT, and in this context it isnatural to embed some form of constraint solving in the type inference problem.From there, Simonet and Pottier generalized to a rich notion of GADT defined overarbitrary constraints, in presence of a subtyping relation, justified in their settingby potential applications to information flow checking.They do not describe a particular type system, but a parametrized frameworkHMG(X), in the spirit of the inference framework HM(X). In this setting, they prove

GADT meet subtyping8a general soundness result, applicable to all type systems which satisfy their modelrequirements. We directly reuse this soundness result, by checking that we respectthese requirements and proving that their condition for soundness is met. Thisallows us to concentrate purely on the static semantics, without having to defineour own dynamic semantics to formulate subject reduction and progress results.Their soundness requirement is formulated in terms of a general constraint entailment problem involving arbitrary constraints. Specializing this to our setting issimple, but expressing it in a form that is amenable to mechanical verification is surprisingly harder—this is the main result of this paper. Furthermore, at their level ofgenerality, the design issues related to subtyping of GADT, in particular the notionof upward and downward-closed type constructors, were not apparent. Our articleis therefore not only a specialized, more practical instance of their framework, butalso raises new design issues.The other major related work, by Emir, Kennedy, Russo and Yu [EKRY06],studies the soundness of having subtyping constraints on classes and methods ofan object-oriented type system with generics (parametric polymorphism). Previouswork [KR05] had already established the relation between the GADT style of havingtype equality constraints on data constructors and the desirable object-orientedfeature of having type equality constraints on object methods. This work extendsit to general subtyping constraints and develops a syntactic soundness proof in thecontext of a core type system for an object-oriented languages with generics.The general duality between the “sums of data” prominent in functional programming and “record of operations” omnipresent in object-oriented programmingis now well-understood. Yet, it is surprisingly difficult to reason on the correspondence between GADT and generalized method constraints; an application that isusually considered to require GADT in a functional style (for example a stronglytyped eval α expr datatype and its associated eval function) is simply expressedin idiomatic object-oriented style without specific constraints6 , while the simpleflatten : α, α list list α list requires an equality or subtyping constraintwhen expressed in object-oriented style.These important differences of style and applications make it difficult to compareour present work with this one. Our understanding of this system is that a subtypingconstraint of the form X Y is considered to be a negative occurrence of X,and a positive occurrence of Y ; this means that equality constraints (which areconjunctions of a ( ) constraint and a ( ) constraints) always impose invarianceon their arguments. Checking correctness of constraints with this notion of varianceis simpler than with our upward and downward-closure criterion, but also not asexpressive. It corresponds, in our work, to the idea of GADT with subtypingconstraint mentioned in the introduction and that we detail in §4.3.The design trade-off in this related work is different from our setting; the reasonwhy we do not focus on this solution is that it requires explicit annotations at theGADT definition site, and more user annotations in pattern matching in our systemwhere subtyping is explicitly annotated, while convertibility is implicitly inferredby unification. On the contrary, in an OOP system with explicit constraints andimplicit subtyping, this solution has the advantage of user convenience.We can therefore see our present work as a different choice in the design space: wewant to allow a richer notion of variance assignment for type equalities, at the cost ahigher complexity for those checks. Note that the two directions are complementaryand are both expressed in our formal framework.6 There is a relation between this way of writing a strongly typed eval function and the “finallytagless” approach [Kis] that is known to require only simple ML types.

GADT meet subtypingσ σ9σ1 σ2σ2 σ3σ1 σ3σ σ0τ τ00σ τ σ τ0b6cb cσ σ0τ τ0σ τ σ0 τ 0 i, σi vi σi0type vα tσ t σ0 tFigure 1: Subtyping relation2A formal settingWe define a core language for Algebraic Datatypes (ADT) and, later, GeneralizedAlgebraic Datatypes (GADT), that is an instance of the parametrized HMG(X)system of Simonet and Pottier [SP07]. We refine their framework by using variancesto define subtyping, but rely on their formal description for most of the system,in particular the static and dynamic semantics. We ultimately rely on their typesoundness proof, by rigorously showing (in the next section) that their requirementson datatype definitions for this proof to hold are met in our extension with variances.2.1Atomic subtypingOur type system defines a subtyping relation between ground types, parametrizedby a reflexive transitive relation between base constant types (int, bool, etc.).Ground types consist of a set of base types b, function types τ1 τ2 , product typesτ1 τ2 , and a set of algebraic datatypes σ t. (We write σ for a sequence of types(σi )i I .) We use prefix notation for datatype parameters, as is the usage in ML.Datatypes may be user-defined by toplevel declarations of the form:type vα t K1 of τ 1 [α] . Kn of τ n [α]This is a disjoint sum: the constructors Kc represent all possible cases and eachtype τ c [α] is the domain of the constructor Kc . Applying it to an argument e of acorresponding ground type τ [σ] constructs a term of type σ t. Values of this typeare deconstructed using pattern matching clauses of the form Kc x e, one for eachconstructor.The sequence vα is a binding list of type variables αi along with their varianceannotation vi , which is a marker among the set { , , , on}. We may associate arelation a relation ( v ) between types to each variance v: is the covariant relation ( ); is the contravariant relation ( ), the symmetric of ( ); is the invariant relation ( ), defined as the intersection of ( ) and ( ); nn), the full relation such that σ on τ holds foro , is the irrelevant relation (oall types σ and τ .Given a reflexive transitive relation (6) on base types, the subtyping relation onground types ( ) is defined by the inference rules of Figure 1, which, in particular,give their meaning to the variance annotations vα. The judgment type vα t simplymeans that the type constructor t has been previously defined with the varianceannotation vα. Notice that the rules for arrow and product types can be subsumedby the rule for datatypes, if one consider them as special datatypes (with a specific

GADT meet subtyping10dynamic semantics) of variance ( , ) and ( , ), respectively. For this reason, thefollowing definitions will not explicitly detail the cases for arrows and products.Finally, it is routine to show that the rules for reflexivity and transitivity areadmissible, by pushing them up in the derivation until the base cases b 6 c, wherethey can be removed as (6) is assumed to be reflexive and transitive. Removingreflexivity and transitivity provides us with an equivalent syntax-directed judgmenthaving powerful inversion principles: if σ t σ 0 t and type vα t, then one candeduce that for each i, σi vi σi0 .We insist that our equality relation ( ) is here a derived concept, defined fromthe subtyping relation ( ) as the “equiconvertibility” relation ( ); in particular, it is not defined as the usual syntactic equality. If we have both b1 6 b2 andb1 6 b2 in our relation on base types, for two distinct base types b1 and b2 , we haveb1 b2 as types, even though they are syntactically distinct. This choice is inspiredby the previous work of Simonet and Pottier.On the restriction of atomic subtyping The subtyping system demonstratedabove is called “atomic”. If two head constructors are in the subtyping relation,they are either identical or constant (no parameters). Structure-changing subtypingoccurs only at the leaves of the subtyping derivations.While this simplifies the meta-theoretic study of the subtyping relation, this istoo simplifying for real-world type systems that use non-atomic subtyping relations.In our examples using the OCaml type system, private type were a source of nonatomic subtyping: if you define type α t2 private α t1 , the head constructorst1 and t2 are distinct yet in a subtyping relation. If we want to apply our formalresults to the design of such languages, we must be careful to isolate any assumptionon this atomic nature of our core formal calculus.The aspect of non-atomic subtype relations we are interested in is the notion ofv-closed constructor. We have used this notion informally in the first section (inOCaml, product types are -closed); we now defined it formally.Definition 1 (Constructor closure) A type constructor α t is v-closed if, forany type sequence σ and type τ such that σ t v τ hold, then τ is necessarily equalto σ 0 t for some σ 0 .In our core calculus, all type constructors are v-closed for any v 6 on, but we willstill mark this hypothesis explicitly when it appears in typing judgments; this letthe formal results be adapted more easily to a non-atomic type system.It would have been even more convincing to start from a non-atomic subtypingrelation. However, the formal system of Simonet and Pottier, whose soundnessproof we ultimately reuse, restricts subtyping relations between (G)ADT type toatomic subtyping. We are confident their proof (and then our formal setting) canbe extended to cover the non-atomic case, but we have left this extension to futurework.2.2The algebra of variancesIf we know that σ t σ 0 t, that is σ t σ 0 t, and the constructor t has variablevα, an inversion principle tells us that for each i, σi vi σi0 . But what if we onlyknow σ t u σ 0 t for some variance u different from ( )? If u is ( ), we get thereverse relation σi vi σi0 . If u is (on), we get σi on σi0 , that is, nothing. This outlinesa composition operation on variances u.vi , such that if σ t u σ 0 t then σi u.vi σi0

GADT meet subtyping11holds. It is defined by the following table:v.w onv on on ononononononwThis operation is associative and commutative. Such an operator, and the algebraicproperties of variances explained below, have already been used by other authors,for example [Abe06].There is a natural order relation between variances, which is the coarser-thanorder between the corresponding relations: v w if and only if ( v ) ( w ); i.e.if and only if, for all σ and τ , σ w τ implies σ v τ .7 This reflexive, partial orderis described by the following lattice diagram: onThat is, all variances are smaller than and bigger than on.From the order lattice on variances we can define join and meet of variances:v w is the biggest variance such that v w v and v w v; conversely, v wis the lowest variance such that v v w and w v w. Finally, the compositionoperation is monotonous: if v v 0 then w.v w.v 0 (and v.w v 0 .w).We will frequently manipulate vectors vα, of variable associated with variances,which correpond to the “context” Γ of a type declaration. We extend our operationpairwise on those contexts: Γ Γ0 and Γ Γ0 , and the ordering between contextsΓ Γ0 . We also extend the variance-dependent subtyping relation ( v ), whichbecomes an order ( Γ ) between vectors of type of the same length: σ vα σ 0 holdswhen for all i we have σi vi σi0 .2.3Variance assignment in ADTsA counter-example To have a sound type system, some datatype declarationsmust be rejected. Assume (only for this example) that we have two base typesint and bool such that bool 6 int and int 66 bool. Consider the following typedeclaration:type ( α, β) t Fun of α βIf it were accepted, we could build type the following program that deduces fromthe ( α) variance that (bool, bool) t (int, bool) t; that is, we could turn theidentity function of type bool bool into one of type int bool and then turnsan integer into a boolean:let three as bool : bool match (Fun (fun x - x) : (bool, bool) t : (int, bool) t) with Fun (danger : int bool) - danger 37 The reason for this order reversal is that the relations occur as hypotheses, in negative position,in definition of subtyping: if we have v w and type vα t, it is safe to assume type wα t: σ w σ 0implies σ v σ 0 , which implies σ t σ 0 t. One may also see it, as Abel notes, as an “informationorder”: knowing that σ τ “gives you more information” than knowing that σ no τ , thereforeno .

GADT meet subtyping12vc-Varwα Γw vΓ α:vvc-ConstrΓ type wα t i, Γ σi : v.wiΓ σt:vFigure 2: Variance assignmentA requirement for type soundness We say that the type type vα t definedby the constructors (Kc of τ c [α])c C is well-signed if c C, σ, σ 0 ,σ t σ 0 t τ c [σ] τ c [σ 0 ]The definition of ( α, β) t is not well-signed because we have ( , ) t (int, ) taccording to the variance declaration, but we do not have the corresponding conclusion (int ) ( ).This is a simplified version, specialized to simple algebraic datatypes, of thesoundness criterion of Simonet and Pottier. They proved that this condition issufficient 8 for soundness: if all datatype definitions accepted

GADT) sont maintenant bien compris, mais leur ajout a un langage equip e de sous-typage nous r eservait quelques surprises. Qu'est-ce qu' etre covariant pour un pa- . using the subtyping relation of the OCaml type system, the answer is \yes". But, surprisingly to us, in a type system with a top type , the answer would be \no". .