Ambivalent Types for Principal Type Inference with - Gallium
Contents
1. 14 15 16 A I Baars and S D Swierstra Typing dynamic typing In ICFP 02 Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming pages 157 166 ACM Press 2002 J Cheney and R Hinze First class phantom types Computer and Information Science Technical Report TR2003 1901 Cornell University 2003 J Garrigue A certified implementation of ML with structural polymorphism In Proc Asian Symposium on Programming Languages and Systems volume 6461 of Springer Verlag LNCS pages 360 375 Shanghai Nov 2010 J Garrigue Monomophic let in OCaml Blog article at Sept 2013 J Garrigue and D R my Semi explicit first class polymorphism for ML Information and Computation 155 134 171 Dec 1999 J Garrigue and D R my Ambivalent types for principal type inference with GADTs Avail able electronically at http gallium inria fr remy gadts June 2013 D Le Botlan and D R my Recasting MLF nformation and Computation 207 6 726 785 2009 X Leroy D Doligez A Frisch J Garrigue D R my and J Vouillon The OCaml system release 4 00 Documentation and user s manual Projet Gallium INRIA July 2012 C k Lin and T Sheard Pointwise generalized algebraic data types In Proceedings of the 5th ACM SIGPLAN workshop on Types in Language Design and Implementation TLDI 10 pages 51 62 New York NY USA 2010 ACM R Milner A theory of type polymorphism in programming2. Journal of Computer and System Sciences 17 348 375 1978 F Pottier and Y R gis Gianas Stratified type inference for generalized algebraic data types In Proceedings of the 33rd ACM Symposium on Principles of Programming Languages POPL 06 pages 232 244 Charleston South Carolina Jan 2006 T Schrijvers S Peyton Jones M Sulzmann and D Vytiniotis Complete and decidable type inference for gadts In Proceedings of the 14th ACM SIGPLAN international conference on Functional programming ICFP 09 pages 341 352 New York NY USA 2009 ACM T Sheard and N Linger Programming in Omega In Z Horv th R Plasmeijer A So s and V Zs k editors Central European Functional Programming School volume 5161 of Lecture Notes in Computer Science pages 158 227 Springer 2007 V Simonet and F Pottier A constraint based approach to guarded algebraic data types ACM Transactions on Programming Languages and Systems 29 1 Jan 2007 D Vytiniotis S Peyton Jones T Schrijvers and M Sulzmann OutsideIn X Modular type inference with local assumptions Journal of Functional Programming 21 4 5 333 412 Sept 2011 H Xi C Chen and G Chen Guarded recursive datatype constructors In Proceedings of the 30th ACM SIGPLAN SIGACT symposium on Principles of programming languages POPL 03 pages 224 235 New York NY USA 2003 ACM
3. Rule M Bivr is used for variables y and in A that are no longer used we omitted the other premisses while Rule M GEN is used for variables amp and y in A Notice that neither I M V a a y int a gt int xa nor I H M V amp y nt int are derivable It is a key feature of our system that sharing and ambivalence can only be increased implicitly Still it is sound to decrease them explicitly using a type annotation as in I F a gt int M v a a y a int This is obtained by applying the coercion a int of type a gt int gt a gt int f i e V 0t 00 0r 03 Y Y 0 a int a gt int to M The expression Mp equal to use x eq a int in a gt int M is not ambiguous thanks to the annotation around M Hence we have T t eq a int x I a intk a int M a 5 int M UsE Bons A a A x eq a int 2 Mo la int M FUN A a a aF A x Mo leq a int a intf M NEW A v a A x Mo V a lea aG int amp intl A Egq F v a A x Mo Eq lint gt int for some well chosen A A and I where Rx means R preceded and followed by a sequence of and M GEN The rigid variable a is turned into the poly morphic variable which is then instantiated to int before the application to Eq M APP 4 Properties By lack of space we omit formal statements and their proofs as well as
4. do not address this problem here Ambivalent Types for Principal Type Inference with GADTs 9 v 8 i a 0 a y 8 v6 Y int 0 int pj 8 p 8 amp amp 60 00 v a 0 V a 8 a eq 1 62 0 eq 6 0 20 Fig 2 Application of substitution 0 equal to a lt that the current program point cannot be reached Therefore any ambivalent type is admissible in an inconsistent context The semantic judgment I y means by definition that any ground instance of I that satisfies the equations in I makes all types in the semantics of y equal Formally Definition 1 Entailment Let I be a typing environment A ground substitution 0 from rigid variables to simple types models I if 0 11 and 0 T2 are equal for each equation 1 T in T We say that I entails y and write T y if 0 w is a singleton for any ground substitution 0 that models I This gives a simple algorithm to check for entailment compute the most general unifier 0 of I then T l y holds if and only if 0 w is a singleton or 0 does not exist 3 4 Substitution In our setting substitutions operate on ambivalent types where type variables are used to label inner nodes of types and not just their leaves They allow the replacement of an ambivalent node y by a more ambivalent one y y using the substitution a yz y or merging two ambivalent nodes yj and y using the substitution 0 05 Wi yo To cap
5. labeling of the type of its argument without changing its behavior The types of the argument and the result need not be exactly T but consistent instances of 7 see the definition of 17 above Annotations are typically meant to be used in expressions such as T M which forces M to have a type that is an instance of t While this is the only effect it would have in ML here it also duplicates the polymorphic skeleton of M which allows different labeling of inner nodes in the type of M passed to the annotation and its type after the annotation By contrast free type variables of tT remain shared between both types The example below illustrates how type annotations can be used to remove ambivalence Rule M WrtnEss says that the Eq type constructor can be used to witness an equal ity between equal types as eq for any type Conversely an equality type eq 1 62 can only have been built from the Eq type constructor Rule w Usz uses this fact to learn and add the equation 7 7 in the typing context while typechecking the body of M2 the witness M must be typable as an instance of the type eq 1 T2 up to sharing of inner nodes Since the equation is only available while typechecking Mh it is not present in the typing context of the conclusion Hence the type 6 amp 5 must be well formed in I But this is a direct consequence of the second premise it implies I t T2 F Co which in turn requires that all labels of 5 whic
6. view e g yi may be large and a potential source of ambiguities the outer view e g V may contain fewer types and remain coherent this way the ambivalence of the inner view does not leak outside and does not create ambiguities Consider for example the program let g type a x a int eq y match x with Eq gt if y a gt O then y a else 0 a Type annotations on y and the conditional let them have unique outer types which are thus unambiguous when leaving the scope of the equation More precisely Cy a and 0 can be both assigned type a int which is also that of the conditional if else 0 while the annotation if else O a and variable y both have the singleton type a Note that the type of the annotated expression is the inner view for y but the outer view for the conditional Of course it would be quite verbose to write annotations everywhere so in a real language we shall let annotations on parameters propagate to their uses and annotations on results propagate inside pattern matching branches The function g may be written more concisely as follows but we will ignore this aspect in this work let go type a x a int eq y a a match x with Eq gt if y gt O then y else 0 A natural question at this point is why not just require that the type of the result of pattern matching a GADT be fully known from annotations This would avoid the need for this new notion of ambiguity This is pe
7. 61 U ffy 62 The definition is analogous for free rigid variables except that frv w is equal to frv w and frv a is equal to a We write ftv the subset of ffv of variables that appear as leaves i e labeling empty nodes and fnv C the subset of ffv that are labeling nonempty nodes In well formed types these two sets are disjoint i e ffv C is the disjoint union of ftv and fnv C Rigid type variables lie between flexible type variables and type constructors A rigid variable a stands for explicit polymorphism it behaves like a nullary type con structor and clashes by default with any type constructor and any other rigid variable but itself However pattern matching a GADT may introduce type equations in the typ ing context while type checking the body of the corresponding branch which may allow a rigid type variable to be compatible with another type Type equations are used to ver ify that all ambivalent types occurring in the type derivation are well formed which requires in particular that all types of a same node can be proved equal Interpretation of types Ambivalent types may be interpreted as sets of simple types by unfolding ambivalent nodes as follows e a int int Cer v Upepe we 6 gt Sol t1 gt 1 Or E l la a llea Si 2 I tea 1 m 61 o The interpretation ignores labels of inner nodes It is used below for checking coherence of ambivalent type
8. Ambivalent Types for Principal Type Inference with GADTs Jacques Garrigue and Didier R my Nagoya University Graduate School of Mathematics INRIA Rocquencourt Abstract GADTs short for Generalized Algebraic DataTypes which allow con structors of algebraic datatypes to be non surjective have many useful applica tions However pattern matching on GADTs introduces local type equality as sumptions which are a source of ambiguities that may destroy principal types and must be resolved by type annotations We introduce ambivalent types to tighten the definition of ambiguities and better confine them so that type inference has principal types remains monotonic and requires fewer type annotations 1 Introduction GADTS short for Generalized Algebraic DataTypes extend usual algebraic datatypes with a form of dependent typing by enabling type refinements in pattern matching branches 2 I4 I They can express many useful invariants of data structures provide safer typing and allow for more polymorphism 11 They have already been available in some Haskell implementations in particular GHC for many years and now appear as a natural addition to strongly typed functional programming languages However this addition is by no means trivial In their presence full type infer ence seems undecidable in general even in the restricted setting of ML style polymor phism 10 Moreover many well typed programs lack a most general ty
9. M APP I x C9 M L Mi C mw LDF rM 6 LIF AQ M V y o gt 6 THM M M LET M ANN Ir M oi T x 0 M3 62 I Fv ftv c T letx M in M2 62 T t V ftv t ttj M WITNESS M USE Fr DF eqn 5 Mi G D 9 M o T H Eq V a y eq a I F use M eq 1 7 in M3 Cp Fig 3 Typing rules also carry type equations 7 7 in typing contexts that are used to show the coherence of ambivalent types via direct or indirect uses of well formedness judgments All axioms require well formedness of I so that whenever a judgement M 6 holds we have I Rule M INsT instantiates the outermost variable of a type scheme It is unusual in two ways First we write o lt y rather than just o in the quantified type This trick ensures that all nodes labeled with were indeed yj and overcomes the absence of y in the binder Intuitively the instantiated type should be ofa yo w but this happens to be equal to o a lt yw Second we require yo C v to ensure preservation of ambivalence as explained in the previous subsection Finally the premise I y ensures that the resulting type is well formed Rule M GEN introduces polymorphism implicitly as in ML variables that do not appear in the context can be generalized The following rule is derivable from w GrN and and can be used as a shortcut when variable does not appear in y M BIND Tra yF M y oazy CEM wy Rule enables explicit polymorp
10. Mo Types occurring in the source program are simple types T G a tT t ea 7 7 int Type variables are split into two different syntactic classes flexible type variables writ ten amp and rigid type variables written a As usual flexible type variable are meant to be instantiated by any type either during type inference or after their generalization Conversely rigid variables stand for some unknown type and thus are not meant to be instantiated by an arbitrary type They behave like skolem constants We write V F and 7 for the set of variables flexible variables and rigid variables Terms are expressions of the A calculus with constants written c the datatype Eq pattern matching use M T in Mp the introduction of a rigid variable v a M or a type annotation T i e the usual annotation M T is seen as the application T M M x c Mi M A x M let x Mi in M2 Eq use M tin M2 v a M T Although type annotations in source programs are simple types their flexible type vari ables are interpreted as universally quantified in the type of the annotation see q 5 Besides we use and infer ambivalent types internally to keep track of the use of typing equations and detect ambiguities more accurately 3 1 Ambivalent types Intuitively ambivalent types are sets of types Technically they refine simple types to express certain type equivalences within the structure of types Every node becomes
11. a set of type expressions instead of a single type expression and is labeled with a flexible type variable More precisely ambivalent types written are recursively defined as pr alC gt Cleq int wz elpew GC w o v a 6 6 Jacques Garrigue and Didier R my A raw type p is a rigid type variable a an arrow type C an equality type eq 6 C or the base type int A proper raw type is one that is not a rigid type variable An ambivalent type is a pair y of a set y of raw types p labeled with a flexible type variable ot We use to separate the elements of sets of raw types it is associative commutative has the empty set for neutral element and satisfies the idempotence axiom V y y An ambivalent type is always of the form y and we write for y When y is empty is a leaf of the form which corresponds to a type variable in simple types hence we may just write instead of as in the examples above Type schemes o are defined as usual by generalizing zero or more flexible type variables Rigid type variables may only be used free and cannot be quantified over We introduce them in the typing environment but turn them into flexible type variables before quantifying over them so they never appear as bound variables in type schemes In our representation every node is labeled by a flexible type variable This is es sential to make type inference modular as it is needed for increme
12. a description of type inference and we refer the reader to the accompanying technical report 5 Type soundness Type soundness is established by seeing our system as a subset of HMG X 12 Formally we exhibit a translation from our language to HMG X that preserves typing judgments The key is that well formed ambivalent types are such that all simple types in their interpretation are provably equal in the current context i e under the equations introduced by use expressions Ambivalent types are only used for type inference and are dropped during the translation Monotonicity Let I o lt o be the instantiation relation which says that any monomor phic instance of o well formed in T is also a monomorphic instance of o This relation is extended point wise to typing contexts I I if for any term variable x in dom T DI FI x I x all other components of I and I being identical We may now state monotonicity in our system if I M and I lt I then I M C Existence of principal solutions to type inference problems This is our main result A typing problem is a typing judgment skeleton gt M where I omits all node descriptions y hence I is usually not well formed but can be extended into a well formed environment by interleaving the appropriate node descriptions with bind ings in I A solution to a typing problem is a pair of a substitution 0 that preserves Ambivalent Types for Principal Typ
13. be performed in the body of the case analysis By allowing information to flow only from the outside to the inside principality is preserved when inference succeeds Yet as for stratified type inference 9 it lacks monotonicity While previous approaches have mostly attempted to propagate types to GADT case analyses we aim in the opposite direction at reducing the need for type information in case analysis This aspect is orthogonal to propagation and improving either one improves type inference as a whole Actually OutsideIn already goes one step in that direction by allowing type information to flow out of a pattern matching case when no type equation was added But it stops there because if type equations were added they could have been used and consequently the type of the branch is flagged ambiguous This led us to focus our attention on the definition of ambiguity Type equations are introduced inside a pattern matching branch but with a local scope the equation is not valid outside of the branch This becomes a source of ambiguities Indeed a type equation allows implicit type conversions i e there are several inter convertible forms for types that we need not distinguish while in the scope of the equation but they become nonconvertible hence ambiguous when leaving its scope as the equation can no longer be used Ambiguity depends both on the equations available and on the types that leak outside of the branch if removing the
14. ction a with the effect of replacing all occurrences of a and of int by intza Thus the function has type int a int a and the result of the application has type int a 1the correct one We now obtain the same result whatever the scenario This result type may still be unified with some other rigid variable a as long as this is allowed by having some equation a int or a a in the context and refine its type to int za a Since we cannot tell in advance which type constructors will eventually be mixed with other ones all nodes must keep their label when substituted Replaying the example with full label annotations choice has type V a y y a a Y Y and its partial application to x has type V a y a a9 af ter generalization Observe that this is less general than V a o y a a but more general than V a y int xa intza Type variables Type variables are either rigid variables a or flexible variables We write frv for the set of rigid variables that are free in and ffv C for the set of Ambivalent Types for Principal Type Inference with GADTs 7 flexible variables that are free in These definitions are standard For example free flexible variables are defined as ffv y for Uffv y ffv a 0 ffv 2 0 ffv int 2 0 flv p z y fiv p Uffv v ff Ei 62 ffy E1 U ffy 62 ffv V a o ffv o a ffv eq amp 1 62 ffy
15. e 9 is another interesting approach to type inference for GADTs that uses several sophisticated passes to propagate local typing constraints and not just type annotations progressively to the rest of the program 14 Jacques Garrigue and Didier R my The following table summarizes the typability of the programs given in the overview for our approach including simple syntactic propagation of type annotations Out sidelif and stratified type inference 9 Program f fi f2 g gi E2 P Pi Ambivalent VI VIVI vV v vl OutsideIn Viviv Stratified V v The results for f are unsurprising this example is not even principal in the naive type system without an internal notion of ambivalence a type system is unable to tell that the equality between two types is only accidental and should not be considered as a source of ambiguity The results for f and f2 are more interesting While OutsideIn requires an external type annotation in both cases stratified type inference accepts to infer the type of the branch from its body More precisely the propagation algorithm operates in a bi directional way and is able to extract non ambiguous information from GADT pattern matching branches The exported information is pruned so that it re mains compatible with any interpretation of the internal information even in a context with fewer type equations Thus the type of the result is pruned i
16. e Inference with GADTs 13 ambivalence for the types in I and together with a context A that contains only node descriptions such that I0 and A can be interleaved to produce a well formed typing context written I 0 A and the judgment I O A M 0 holds For any typing problem the set of solutions is stable by substitution and is either empty or has a principal solution A 0 i e one such that any other solution A 0 is of the form 0 0 o 0 for some substitution 0 that preserves well formedness in I 0 A i e for any type C such that TO At C we have rO A H C 0 Sound and complete type inference Principality of type inference is proved as usual by exhibiting a concrete type inference algorithm This algorithm presented in the extended version relies on a variant of the standard unification algorithm that works on ambivalent types and preserves their sharing It uses a typing constraint approach which converts typing problems to unification problems while also ensuring that in ferred types are well formed i e coherent properly scoped and acyclic The use of constraints here is however just a convenience since the ambivalence information is contained in types themselves constraints can always be solved prior to type general ization so that we do not need constrained type schemes That is constraints are just a way to describe the algorithmic steps without getting into implementation details OCaml it
17. e type inference is also tackling type inference a ML but restricting the expressiveness of the system some uses of GADT will be rejected so that more aggressive type propagation can be done in a principal way Point wise type inference is hard to compare to our approach as many programs have to be modified For instance it rejects all our examples because equality witnesses can only be matched on if they relate two rigid type variables To be accepted we could replace eq by a specialized version type _ t Int int t Ambivalent types borrow ideas from earlier works The use of sharing to track known type information was already present in our work on semi explicit first class polymorphism 4 There we only tracked sharing on a special category of nodes con taining explicitly polymorphic types Here we need to track sharing on all nodes as any type can become ambivalent In our type inference algorithm we also reuse the same definition style describing type inference as a constraint resolution process but introducing some points where constraints have to be solved before continuing The formalization itself borrows a lot from previous work on structural polymor phism for polymorphic variant and record types 3 In particular unification of am bivalent types which merges sets of rigid variables and requires checking coherence constraints can be seen as an instance of the unification of structurally polymorphic nodes The diff
18. equation does not impair convertibility for a type either because it was not convertible to start with or because other equations are available it need not be seen as ambiguous Since ambiguities must generally be solved by adding type annotations a more precise definition and better detection of ambiguities become essential to reduce the need for explicit type information By defining ambiguity inside the type system we are able to restrict the set of valid typings In this paper we present a type system such that among the valid typings there is always a principal one i e subsuming all of them and we provide a type inference algorithm that returns the principal solution when it exists Ambivalent Types for Principal Type Inference with GADTs 3 Moreover our type system keeps the usual properties of ML including monotonicity This detection of ambiguity is now part of OCaml 7 Since propagating type information and reducing the amount of type information needed by case analysis are orthogonal issues our handling of ambiguity could be combined with existing type inference algorithms to further reduce the need for type annotations As less type information is needed it becomes possible to use a weaker propagation algorithm that preserves monotonicity This is achieved in OCaml by rely ing on the approach previously developed for first class polymorphism 4 The rest of this paper is organized as follows We give an overview of our solut
19. erence is again that all nodes are potentially ambivalent in our case while structural polymorphism only cares about variant and record types 6 Conclusion Ambivalent types are a refinement of ML types which represents within types them selves ambiguities resulting from the use of local equations They permit a more accu rate definition of ambiguity which in turn reduces the need for type annotations while preserving both the principal type property and monotonicity This approach has been implemented in OCaml We have not addressed propagation of type information in this work although this is quite useful in practice A simple propagation mechanism based on polymorphism similar to that used for semi explicit first class polymorphism as already in use in OCaml seems sufficient to alleviate the need for most local type annotations while preserving principality of type inference The notion of ambivalence is orthogonal to previous techniques used for GADT type inference Therefore it should also benefit other approaches such as OutsideIn or stratified type inference Hopefully ambivalent types might be transferable to MLF 16 Jacques Garrigue and Didier R my 6 as the techniques underlying both ambivalent types and semi explicit first class polymorphism have many similarities Acknowledgements We thank Gabriel Scherer and the anonymous reviewers for de tailed comments on this paper References 1 10 11 12 13
20. f ambiguity The idea is to track whether such mixed types are escaping from their scope Intuitiveley we may do so by disallow ing the expression to have either type and instead viewing it with an ambivalent type a7 int which we just see syntactically as a set of types An ambivalent type must still be coherent i e all the types it contains must be provably equal under the equations available in the current scope Hence although a int can be interpreted as an intersection type it is not more expressive than choosing either representation since by equations this would be convertible to the other type but more precise it retains the information that the equivalence of a and int has been assumed to give the expression the type a or int Since coherence depends on the typing context a coherent ambivalent type may suddenly become incoherent when leaving the scope of an equation This is where ambiguity appears Hence while an ambivalent type is a set of types that have been assumed interchangeable an ambiguity arises only when an ambivalent type becomes incoherent by escaping the scope of an equation it depends on Ambiguous programs are to be rejected Fortunately ambiguities can be eliminated by using type annotations Intuitively in an expression e 7 the expressions e and e T have sets of types y and yo that may differ but such that 7 is included in both ensuring soundness of the change of view In particular while the inner
21. h contain no quantifiers have node descriptions in I so that they cannot depend on T 75 Typically ambivalent types needed for the typing of M are introduced using rule w Bir which means that they cannot remain inside 5 so that there is no way to keep an ambiguous type Notice that the well formedness of I t t implies that 7 and 7 contain no flexible type variables rules wF TyPE EQUAL and wF CTXx EQUAL We now illustrate the typing rules on an example Assume that if _ then _else _ is given as a primitive with type scheme V 75 35 1 Yo V bool gt a gt a gt a n Let I be I5 A Ay int za where I is a a int and A is Q int 5 A Q yi a gt a and A is y bool yy a gt A gt a r Using M Var for premises we have T if then else _ boo1 a gt a gt T F true y i Ib if true then else _ gt a gt a We also have D 1 int zza and I y int za by w INsT and w VaR Hence we have I F if true then 1 else y int a by This leads to M AP Ib if true then 1 else y int a M FUN Ij A A F A y if true then 1 else y V y int za int zza M INST z z Ij A A M int xa gt int za 9 M BIND Ty AEM ntzza gt int a M GEN I M V a y int za gt int xa 12 Jacques Garrigue and Didier R my where M is A y if true then 1 else y
22. hism and explicit type equations using wit nesses For that purpose it introduces a rigid type variable a in the typing context that may be used inside M typically for introducing type annotations However poly morphism becomes implicit in the conclusion by turning the rigid type variable a into a quantified flexible type variable when exiting the scope of the v form Polymorphism can then be eliminated implicitly gt las regular polymorphism in ML The second premise ensures that the rigid type variable a does not appear anywhere else but in a Our version of Rule generalizes the type y introduced for annotating the arrow type which avoids introducing y o 6 in the premise Rule M AP differs from the standard application rule in two ways a minor difference is that the arrow 5 This is why we write this v a M rather than Aa M Ambivalent Types for Principal Type Inference with GADTs 11 type has a label as in Rule a major difference is that the type of M may be ambivalent as long as it contains an arrow raw type of the form 5 6 In particular the premise I M 2 y does not in general imply C M 62 gt as this could lose sharing Hence we have to read the arrow structure directly from the ambivalent type Rule w Lrr is as usual Rule M ANnJallows explicit loss of sharing via type annotations It is presented as a retyping function of type scheme 7 i e a function that changes the
23. ion in 2 We present our system formally and state its soundness in 93 We state principality and monotonicity in by lack of space we leave out some technical developments all proofs and the description of the type inference algorithm which can all be found in the accompanying technical report 5 Finally we compare with related works in 2 Anoverview of our solution The standard notion of ambiguity is so general that it may just encompass too many cases Consider the following program type _ _ eq Eq 0 0 eq let f type a x a int eq match x with Eq gt 1 Type eq is the classical equality witness It is a GADT with two index parameters denoted by the two underscores and a single case Eq for which the indices are the same type variable Thus a value of type a b eq can be seen as a witness of the equality between types a and b In the definition of we first introduce an explicit universal variable a called a rigid variable treated in a special way in OCaml as it can be refined by GADT pattern matching By constraining the type of x to be a int eq we are able to refine a when pattern matching x against the constructor Eq the equation a int becomes available in the corresponding branch i e when typechecking the expression 1 which can be assigned either type a or int As a result f can be given either type int eq gt int or OG int eq a This fulfills the standard definition of ambiguity and s
24. n the external type system a program may be typable but have no principal type but it does hold if we restrict ourselves to those programs whose elaboration in the internal language is typable However since elaboration extracts information from the typing context monotonicity is lost strengthening the type of a free variable by making it more general before elaboration can reduce the amount of type information available on the elaborated program and make it ill typed Monotonicity is a property that has often been underestimated because it usually but not always holds in languages with principal types However losing monotonicity can be worse for the programmer than losing principal types It reveals a lack of modularity in the language since some simple program transformations such as simplifying the body of a function may end up infer ring more general types which may subsequently break type inference Propagating only type annotations would preserve monotonicity but it is much weaker GHC 7 follows a similar strategy called OutsideIn 13 using constraint solving rather than elaboration to extract all typing information from the outer context As a re sult propagation and inference are interleaved That is the typing information obtained by solving constraints on the outer context enclosing a GADT case analysis is directly used to determine the types of both the scrutinee and the result in this case analysis Type inference can then
25. n function f but it can be propagated for f and f2 This corresponds exactly to the naive notion of ambiguity Typing of g fails in all three systems as it is fundamentally ambiguous whichever definition is chosen The results for g may look surprising while it contains many type annotations both OutsideIn and stratified type inference still fail on it The reason is that type annotations are inside the branch in both systems only type annotations outside of a branch can disambiguate types for which an equation has been introduced We find this behavior counter intuitive The freedom of where to add type annotations stands as a clear advantage of ambivalent types By contrast g2 provides full type annotations in a standard style so that all systems succeed although ambivalent types need some simple propagation mechanism to push annotations inside Programs p and p demonstrate the power of OutsideIn The program pi is the following variant of p which we deem ambiguous Indeed the match expression in p would have to be given the ambivalent type a int which is not allowed outside the scope of the equation a int Both p and p are ac cepted by OutsideIn since type information can be propagated upward even for local let definitions This comes at a cost though local let definitions are monomorphic by default but can be made polymorphic by adding a type annotation While local poly morphic definitions are relatively rare
26. ntal instantiation To see this consider a context that contains a rigid type variable a an equation a int and a variable x of type a under which we apply a function choice of type a 0t a to x and 1 We first reason in the absence of labels on inner nodes The partial application choice x has type a a To further apply it to 1 we must use the equation to convert both 1 of type int and the domain of the partial application to the ambivalent type int a The type of the full application is then a However if we inverted the order of arguments it would be int Something must be wrong In fact if we notice in advance that both types a and int will eventually have to be converted to int a we may see both x and 1 with type int a before performing the applications In this case we get yet another result int a which happens to be the right one What is still wrong is that as soon as we instantiate we lose the information that all occurrences of must be synchronized The role of labels on inner nodes is to preverve this information Revisiting the example the partial application now has type a a we still temporarily omit the annotation on arrow types as they do not play a role in this example This is saying that the type is currently a a but remembering that the domain and codomain must be kept synchronized Then the interger 1 of type int can also be seen with type int a and unified with the domain of the fun
27. o should be rejected But should we really reject it Consider these two slight variations in the definition of f let f type a x a int eq match x with Eq gt true let f5 type a x a int eq y a match x with Eq gt y gt 0 In f we just return true which has the type bool unrelated to the equation In f2 we actually use the equation to turn y into an int but eventually return a boolean These variants are not ambiguous How do they differ from the original The only reason we have deemed f to be ambiguous is that 1 could potentially have type a by using the equation However nothing forces us to use this equation and if we do not use it the only possible type is int It looks even more innocuous than 5 where we indirectly need the equation to infer the type of the body So what would be a truly ambiguous type We obtain one by mixing a s and int s in the returned value the left margin vertical rules indicate failure 3 Examples in this section use OCaml syntax 7 Letter stands for a flexible variable as usual while letter a stands for a rigid variable that cannot be instantiated This will be detailed later 4 Jacques Garrigue and Didier R my let g type a x a int eg y a match x with Eq gt if y gt O then y else 0 Here the then branch has type a while the else branch has type int so choosing either one would be ambiguous How can we capture this refined notion o
28. pe Using ex plicit type annotations solves both problems Unfortunately while it is relatively easy to design a sound typing algorithm for a language with GADTs it is surprisingly difficult to keep principal types without requesting full type annotations on every case analysis Repeatedly writing full type annotations being cumbersome a first approach to a stronger type inference algorithm is to propagate annotations This comes from the basic remark that in many cases the type of a function contains enough information to determine the type of its inner case analyses A simple way to do this is to use program transformations pushing type annotations inside the body of expressions Stratified type inference for GADTs 9 goes further in that direction converting from an external language where type annotations are optional to an internal language where the scrutinee of case analysis and all coercions between equivalent types must be annotated This conversion is an elaboration phase that collects all typing information not only type annotations and propagates it where it is needed The internal lan guage allows for straightforward type inference and it has the principal type property Part of this work has been done at IRILL 2 Jacques Garrigue and Didier R my It also enjoys monotonicity strengthening the type of a free variable by making it more general preserves well typedness As expected principality does not hold in general i
29. rhaps good enough if we only consider small functions as shown for g2 we may write the function type in one piece and still get the full type information However the situation degrades with local let bindings let p type a x a int eq int Ambivalent Types for Principal Type Inference with GADTs 5 let y match x with Eq gt 1 in y 2 The return type int only applies to y 2 so we cannot propagate it automatically as an annotation for the definition of y Basically one would have to explicitly annotate all let bindings whose definitions use pattern matching on GADTs This may easily become a burden especially when the type is completely unrelated to the GADTs or accidentally related as in the definition of f above We believe that our notion of ambiguity is simple enough to be understood easily by users avoids an important number of seemingly redundant type annotations and pro vides an interesting alternative to non monotonic approaches see q5 for comparison 3 Formal presentation Since our interest is type inference we may assume without loss of generality that there is a unique predefined binary GADT eq with a unique constructor Eq of type V a eq a at The type eq 1i T2 denotes a witness of the equality of T and T2 and Eq is the unique value of type eq 11 T2 For conciseness we specialize pattern matching to this unique constructor and just write use M T in Mo for match M4 with Eq gt
30. s which is a semantic issue and does not care about sharing of inner nodes For example types int xa int a and int za int za are interpreted in the same way namely as int int a a a int int a A type is said truly ambivalent if its interpretation is not a singleton Notice that y may be a singleton p even though y is truly ambivalent since ambivalence may be buried deeper inside p as in int xa gt int a Converting a simple type to an ambivalent type Given a simple type 7 we may build a not truly ambivalent type such that t This introduces new variables 7 that are in fnv while the variables of ftv come from t We write tS for the most general type scheme of the form V 7 which is obtained by labeling all inner nodes of T with different labels and quantifying over these fresh labels For example lint gt int is V 2 int int and la gt af is V yo 99 Notice that free type variables of T remain free in 7j 3 2 Typing contexts Typing contexts I bind program variables to types and introduce rigid type variables a type equations 7 7 and node descriptions V I 0 D x o DI a I 05 o lI a w 8 Jacques Garrigue and Didier R my WF CTX EQUAL WF TYPE EQUAL WF TYPE FLEX Er TrKy h Try Tr ftv t ftv 20 EF a wer FDu cv TKuy h rH y WF CTX FLEX WF TYPE AMBIVALENT Fr Try a dom r Fpgf Trik
31. self uses a variant of Milner s algorithm Z 5 Related works While GADTs have been an active research area for about 10 years early works usually focused on their type checking and expressiveness ignoring ML style type inference Typically they rely on an explicitly typed core language and use local type inference techniques to leave some type information implicit Other recent works with rich de pendent type systems also fit in this category and are only loosely related to ours Relatively few papers are dedicated to principal type inference for GADTs The tension between ambiguity and principality is so strong that it has been assumed that the only way to reach principality is to know exactly the external type of each GADT match case As a result research has not been so much focused on finding a type system with principal types but rather on clever propagation of type information so that pro grams have enough type annotations after propagation to admit principal types or are rejected otherwise Hence some existing approaches always return principal solutions but do not have a clear specification of when they will succeed because this depends on the propagation algorithm or some idealized version of it which does not have a compositional specification OutsideIn improves on this by using uses constraint solving in place of directional annotation propagation which greatly reduces the need for annotations Stratified type inferenc
32. so that this change of behavior appears as a good compromise for Haskell they are still frequent enough and their coresponding type annotations large enough so that we prefer to keep local polymorphism in OCaml Moreover local polymorphism is critical for the annotation propagation mechanism used by OCaml as a complement to ambivalent types and for polymorphic methods let pj type a x a int eq y a let z match x with Eq gt if y 0 then y else O inz 1 6 Results differ for GHC 7 6 as it slightly departs from OutsideIn allowing some biased choices but next versions of GHC should strictly comply with OutsidelIn Ambivalent Types for Principal Type Inference with GADTs 15 All examples above are specifically chosen to illustrate the mechanisms underly ing ambivalence and do not cover all uses of GADTs Thus they do not mean that our approach always outperforms other ones but they emphasize the relevance of ambiva lence The question is not whichever approach taken alone performs better but rather how ambivalence can be used to improve type inference with GADTs Indeed ambiva lence could be added to other existing approaches to improve them as well Besides this comparison on examples the main advantage of ambivalent types is to preserve principal type inference and monotonicity so that type inference and program refactoring are less surprising An interesting proposal by Lin and Sheard 8 called point wis
33. t Type equations are added to the typing context while typecheck ing the expression at the current program point The set of equations in the context defines an equivalence between types Rule WF TvPE AMBIVALENT shows that ambivalent types can only be formed between equiv alent types the well formedness of the judgment I y requires I IF y i e that all types in y are provably equal under the equations in I which is critical for type sound ness the rightmost premise requires that at most one type in y is not a rigid variable For example the ambivalent types int int int and intY gt int a a are ill formed This is however not restrictive as the former would be unsound in any consistent context while the later could instead be written int xa int xa Well formedness of a type environment requires that its equations do not contain free type variables Equalities in I may thus be seen as unification problems where rigid variables are the unknowns If they admit a principal solution it is a substitution of the form a 7 lt then the set of equations a 7 lt is equivalent to the equations in I If the unification problem fails then the equations are inconsistent in the standard model where type constructors cannot be equated This is acceptable and it just means This is not always true for ML abstract types as type constructors may be compatible in another context but we
34. ture all these cases with the same operation we define in Figure 2 a general form of substitution or lt that may graft arbitrary nodes C at every occurrence of a label ar written o 4 As a result of this generality substitutions are purely syntactic and may replace an ambivalent node with a less ambivalent one or even prune types replacing a whole subtree by a leaf Of course we should only apply substitutions to types when they preserve or increase ambivalence Definition 2 A substitution 0 preserves ambivalence in a type if and only if for any amp in dom 0 and any node y in C we have yO C w 0 As a particular case an atomic substitution lt Co preserves ambivalence in if for any node y in we have y C 6o since well formedness of y implies that may not occur free in y hence y is just y 3 5 Typing rules Typing judgments are of the form I M o as in ML However typing rules defined in Figure 3 differ from the traditional presentation of ML typing rules in two ways On the one hand we use a constraint framework where I carries node descriptions V to enforce their sharing within different types On the other hand typing rules 10 Jacques Garrigue and Didier R my M VAR M INST ED x cer DL F M v a o a ve wow rry Tkx 60 TEM olat y M GEN M NEW I a w M o I aa a M o LFv a o a e TEM V a o IF v a M a ofa e M FUN
35. y w lt 1 FEIa y Try Fig 1 Well formedness of contexts and types excerpt Both flexible and rigid type variables are explicitly introduced in typing contexts Hence well formedness of types is defined relatively to some typing context In addition to routine checks well formedness judgments also ensure soundness of ambivalent types and coherent use of type variables Well formedness of contexts T is recursively defined with the well formedness of types I p and type schemes I c Characteristic rules are in Figure 1 It also uses the entailment judgment I y which means intuitively that all raw types appearing in the set y can be proved equal from the equations in I see q 3 The last premise of Rule WF TvPE AMBIVALENT ensures that ambivalent types contain at most one raw type that is not a rigid variable As usual well formedness of contexts ensures that type variables are introduced before being used and that types are well formed It also ensures coherent use of type variables alias constraints y in the context I define a mapping that provides evidence that is used coherently in the type o This is an essential feature of our system so that refining ambivalence earlier or later commutes as explained above 3 3 Entailment Typing contexts may contain type equations Type equations are used to express equali ties between types that are known to hold when the evaluation of a program has reached a given program poin
Download Pdf Manuals
Related Search