Typing deep pattern-matching in presence of polymorphic variants
Contents
1. Peer used with an argument However this still leaves us with two possibilities The most intuitive one may be val show3 lt Apple Peer This stands for show3 accepts Apple and Peer and any other constructor Yet ex perience proved that this was a bad idea this type is too weak Some clearly erroneous pro grams are accepted with their expected type let j x show3 x id x val j lt Apple Orange of a Pear gt string int let it show3 Pear val it string int unknown 3 If we assume that Peer was a typo for Pear then this answer is incorrect An alternative and actually simpler possibil ity is to force all constructors to be present val show3 gt Apple Peer This avoids the above problem as constructors in open variants can no longer vanish This is simpler because we can limit types to acceptor types with a finite bound presence types and combined types This is also the type that we would obtain for an implementation of show3 using an association list For these reasons the latter typing was chosen in Objective Caml 4 Deep matching If we limit ourselves to flat matching exam ples in the previous sections describe almost all possibilities and it seems that no problems would arise However with deep pattern matching the 3 typing of pattern matching needs to be further refined 4 1 Conjunctiv2. 5 1 Rough typing The corresponding typing rules are presented in figure 2 A pattern typing judgment is of them form F p T where 7 is the type of the pattern Again full typing would also provide a binding environment but we don t need it in the absence of variables The first step of our typing algorithm is to infer the most general type for an or pattern containing all the cases in a pattern matching That is we want to infer 7 such that for any 7 the judgment p T is derivable if and only if there is a type substitution 0 giving 0 T 7 This is easily done by unification Rather than detailing here the unification algorithm we re fer you to other papers Note that since we have only presence types for polymorphic vari ants in pattern types unification is very simple and Ohori s approach is sufficient For instance consider the pattern p TF A PPI TEP 0 B Qi 0 EREN its most general typing is abbreviating unit Fp T F x DA of P B of Q A A MONO ae M Cp tT ad F Cy BU X X Th 1 M B Tk41 X X Tn C Gy p C of TilcicL A A POLY ae coun t ME p Tk tb MC un Di A Cy B Ti X X Tk 1 Me B Tk41 X X T E Cr p Ci of ril A TUPLE A oR1 A OR2 Pu Cpe lt i lt n FMEp T FMEp T FMio o Mn E P1 Pn T1 X X Tn F MC py p2 T F MC py p2 T Fig 3 Acceptability rules 5 2 Exhaustive
3. Again this would result in a non exhaustive pattern matching Considering these problems we choose the second option It should make us able to infer the following types preserving exhaustiveness val f bool lt A B gt int val g K A B list gt int But we have not yet explained how we ob tain these types Indeed the second option sug gests inferring the set of constructors associ ated to a type but does not define how to do it Clearly exhaustiveness has something to do with it by closing some types we were able to make some pattern matchings exhaustive A possible approach would then be enforce exhaustiveness by restricting the type of poly morphic variants when they are breaking ex haustiveness This is actually our ideal goal However this cannot be used as definition there are too many ways to restrict types let h function A _ gt 1 B _ gt 2 _ A gt 3 _ B gt 4 In this case either of these two types val h val h lt A B gt A B gt int gt A B lt A B gt int is enough to ensure exhaustiveness Deciding to use one of the two would loose symmetry the typing would become dependent on the order of the patterns in the pair and the order of the rules in the matching The first type would also make the last two cases unusable which seems to go against the wishes of the programmer
4. M 7 A of P B of Q t3 M r P ta M r Q A pattern matching is exhaustive when all lines in the exhaustiveness matrix are accepted by a pattern For this we define the accept ability relation at a type 7 in figure 3 If mi Min is the i line of M r then it is accepted by p if and only if F mi1 Min E p T is derivable using the acceptability rules One can easily see that in our example the 3rd line of the exhaustiveness matrix is not ac cepted This means that using directly the principal type given by the typing rules this pattern matching would not be exhaustive Note that the order of clauses inside an or pattern or the order of lines inside the exhaus tiveness matrix does not change acceptability Moreover if 7 is a tuple type changing the or der of its components creates a matrix identical to the original one modulo permutations of lines and columns and acceptability of each line does not change if we permute the patterns identi cally From these two facts we can see that the exhaustiveness of a pattern matching at a given type is a symmetrical property preserved by both permutation of or patterns and tuple patterns 5 3 Type refinement The third step of our algorithm is to use ex haustiveness check to decide which polymorphic variant types should be kept open as presence types and which should be reverted to closed acceptor types We proceed in the following way For
5. a purely syntactic point of view this pattern matching is open it contains a wild card which actually matches variants How ever if we look at the first column we see that only A and B will be accepted when the first component is true The real question here appears to be what does _ mean in the context of polymorphic variants We can base ourselves on two differ ent analogies e The string type the set of all possible variant constructors is infinite and _ in dicates all of them so a pattern including a wild card must be open e Usual sum types for any practical appli cation the set of intended constructors is finite and _ indicates all other construc tors in a finite set which should be inferred when possible Interestingly most people seem to find the first option to be more intuitive Its main ad vantage is that the meaning of _ is indepen dent from the context Yet this solution is weak the type inferred for f would be Warning this pattern matching is not exhaustive Here is an example of a value that is not matched true AnyExtraTag val f bool gt A B gt int Moreover it becomes impractical when poly morphic variants are mixed with algebraic datatypes let g function Aor o gt 1 Bi _ gt 2 g gt 3 Here _ means any list but the first inter pretation makes it mean a list containing any variant
6. be cause it allows to use the same constructor in side different types and allows structural equal ity and subtyping between variant types The strict binding of a constructor to a spe cific type enforced by ML algebraic datatypes is sometimes burdensome Think for instance of the multiple intermediate data structures you have in a staged compiler They are of ten very similar in structure but because of some small differences all their constructors must have different names so we end up with an Avariable and a Bvariable an Afunction and a Bfunction and all code working on these data structures must be rewritten for each type With polymorphic variant types you get more freedom you can reuse the same con structor name without fear of conflict and you can even reuse pieces of code working on com mon sets of constructors A complete example of such code reuse has been described While the main interest of polymorphic vari TOOOOODUUO0COO Kyoto University Research Institute for Mathemat ical Sciences ants resides in their typing a subtle part of the problem had not been seriously studied until now the interaction between pattern matching and polymorphic variant typing To be more specific all accounts of polymorphic variant only consider flat pattern matching in which the choice of the branch depends only on the constructor and each constructor oc curs only once In that case the list of han d
7. each column corresponding to a poly morphic variant type we extract all the lines with only a C4 in this column but not in other ones If all these lines are accepted then the type is kept open otherwise it must be closed Formally assuming M r m of width n then for all k s such that i H ma Min Z pit Vj mij C Sj k the polymorphic variant type t M r C of 7 corresponding to the column k must be converted to the acceptor type C of 7 4 Since permuting or patterns or tuple patterns would only change the order of lines and columns in the exhaustiveness matrix the choice of the types to close is symmetrical The type judgment Ffin P Tfin indicates that Tfin is the final type obtained for p by this whole process That is the principal type 7 of p was refined into Tgn by checking the exhaustiveness matrix M r Going on with our running example the rel evant lines are T Cy F C4 While the second line is accepted F FC TT CF 7 since _ matches anything the first line is not only the A and B cases are handled by p As a result the corresponding variant type must be closed and the final pattern type is Ffin p T F x A of P B of Q If we compute the exhaustiveness matrix corre sponding to this new type it contains no longer C lines an acceptor type produces the same matrix as a normal type M T F x A of P B of Q T A PT
8. sharing Finally the ability of acceptor types to loose members makes necessary the introduction of conjunctive types in variant arguments let id2 function Apple gt 1 Orange n gt n val id2 lt Apple Orange of int gt int let h x show x id2 x val h lt Apple Orange of int amp string gt string int The type int amp string means that in order to be accepted by h an orange should have an argument of type both int and string This is of course impossible which limits possible in puts to apples From an inference point of view all members of a conjunctive type have to be unified when its constructor becomes present Conjunctive types are only useful in intermedi ate steps of type inference to make sure that unification is associative and that principality is kept 3 Closed and open matching All the functions we have considered up to now have used closed pattern matching That is an exhaustive list of accepted constructors was provided However it is not rare for pattern matchings to use wild cards to catch all remaining cases let show3 function Apple gt apple Peer gt pear gt unknown Coherently with the usual behavior of pattern matching the meaning of _ can be seen as all other variant constructors We expect such a function to accept any variant value ex cept Apple e and Peer e i e Apple or
9. If we cannot choose between these two types then we should either close both sides mak ing the last two cases unusable or keep both sides open making the pattern matching non exhaustive We could discuss at length on which of the two is worse insisting that non exhaustiveness denotes fundamentally a bug of the program However what matters here is not whether the style of this program is good or bad there are warnings for that but what was the intent of the program From that point of view making a case unusable clearly departs from the intent of the program and we should avoid it as much as possible As a result in this particular case we shall keep both sides open Warning this pattern matching is not exhaustive Here is an example of a value that is not matched AnyExtraTag AnyExtraTag val h gt A B gt A B gt int After considering all these examples now comes the time to define a clear set of rules defining what type should be given to polymor phic variants in a pattern This will be done formally in the next section but we give here the basic steps 1 Type each pattern in the pattern matching and unify the obtained types In this step all variants have open pres ence types 2 Build the exhaustiveness matrix corre sponding to the inferred type 3 For each column of the matrix corre sponding to a variant check whether it allows extra constructors i e the ty
10. TBT BY A P T F B T This means that with this new type our pattern matching is exhaustive Let us now check with another example namely a simplification of the function h in the previous section HA0 lB 0 DA x DB The corresponding matrix is A B M AlxPB 2 St Coes 7 For the first column two lines contain C4 but only one is relevant as relevant lines must con tain only one C It is accepted Cy B E B I A x B Similarly the only relevant line for the second column is also accepted 4 C4 EA DA x B As a result the two variant types must be kept open Fin A 5B 0 0 Al xD BI Of course since the last line is not accepted H Cy C4 ZA 1 5B 0 DA xD BI this also means that the resulting pattern matching is not exhaustive 6 Conclusion We have seen in this paper a possible typing strategy for deep pattern matching containing polymorphic variants This strategy attempts at making the pattern matching exhaustive by eventually closing some variant types The be havior is symmetrical with respect to or pattern and tuple pattern order Whether this is the best strategy and the inferred type is always the most intuitive one remains an open question There are two possible criticisms On one side contrary to some strategies used in older versions of Objective Caml this strategy does not guarantee that all polymorphic variant pattern matchings are complete as we hav
11. Typing deep pattern matching in presence of polymorphic variants JACQUES GARRIGUEt Polymorphic variants are a well known feature of the Objective Caml programming lan guage and they have turned popular since their introduction They allow structural equality of algebraic type definitions and code reuse through their polymorphism Their typing and compilation have been studied in the past and there are already detailed published works for both 4 By their very nature polymorphic variants depend on pattern matching to analyze their contents However only typing for shallow pattern matching was studied in the past In that case checking exhaustiveness is trivial and the natural typing rule guarantees it Deep pattern matching is more complex as other constructors may appear nested in the same pattern matching Exhaustiveness check is available but only after finishing type check ing while we would like to use it to define the typing of polymorphic variant patterns We explain the tradeoffs and define a type checking algorithm for pattern matching containing polymorphic variants which is symmetric 1 Introduction The name polymorphic variant stands for a particular kind of sum type whose constructors are automatically inferred by the type checker This automatic inference is not only useful be cause it avoids writing a type definition actually one could argue that writing a type definition is a good idea anyway but also
12. e seen in our last example This would be a nice property to have but it seems more co herent with other datatypes to limit ourselves to a warning when enforcing it would require an overly restrictive type On the other side the type produced may sometimes be more restrictive than the one in tended by the programmer This could be the case when the type causes a pattern to be un used let f function les SA SP 4 true _ gt 2 Warning this pattern is unused val f bool A gt int One could require the strategy to force all pat terns to be used However this cannot be enforced as this warning can appear even in pattern matchings without variants And we believe that as this definition is inherently am biguous at the type level a warning is the right behavior to obtain in this case References 1 Augustsson L Compiling Pattern Match ing Proc ACM Symposium on Functional Pro gramming and Computer Architectures Jouan naud J P ed Springer Verlag LNCS 201 pp 368 381 1985 2 Garrigue J Programming with Polymorphic Variants ML Workshop Baltimore 1998 3 Garrigue J Code reuse through polymorphic variants Workshop on Foundations of Soft ware Engineering Lecture Notes in Software Science No 25 Sasaguri Japan Kindai Ka gakusha pp 93 100 2000 4 Garrigue J Simple type inference for struc tural polymorphism The Ninth International Workshop on Foundations o
13. e types In the experimental version 2 99 of Objective Caml pattern matching was typed just as nor mal terms let f function true A x gt Ax false A x gt Bx _ B x gt Bx val f bool lt A of a amp b B of b gt gt A of a B of b The resulting type was correct but not intu itive it means that the A case will only be usable if a and b can be bound to the same type While conjunctive types are useful in gen eral here they contradict the assumption that in a pattern matching all cases should be us able This only delays errors The approach in more recent versions of Objective Caml is to first type the patterns independently of envi roning expressions in order to keep principal ity and disallow conjunctive types during this phase Patterns are then unified with the type of the matched expression this time allowing conjunctive types As a result we obtain the following typing val f bool lt A of a B of a gt gt A of a B of a All conjunctive type variables have been col lapsed to one and we obtain a more intuitive typing 4 2 Open or not open With flat matching the distinction between closed and open pattern matchings is easy this is a purely syntactical problem Deep pattern matching introduces grey cases let f function true A gt 1 true B gt 2 false _ gt 3 From
14. f Object Oriented Languages Portland Oregon 2002 5 Leroy X Doligez D Garrigue J R my D and Vouillon J The Objective Caml system re lease 3 07 Documentation and user s manual Projet Cristal INRIA 2003 6 Maranget L Les avertissements du filtrage Journ es Francophones des Langages Applicat ifs 2003 7 Milner R Tofte M and Harper R The Definition of Standard ML MIT Press Cam bridge Massachusetts 1990 8 Ohori A A Polymorphic Record Calculus and Its Compilation ACM Transactions on Programming Languages and Systems Vol 17 No 6 pp 844 895 1995 9 Wadler P Efficient Compilation of Pattern Matching The Implementation of Functional Programming Languages Peyton Jones ed Prentice Hall chapter 5 pp 78 103 1987
15. general being non monotonous can break the princi pality of type inference However this algo rithm only applies to the pattern part of the pattern matching As a result it does not im port any information from the environing ex pression and is functionally computed from the patterns This preserves the principality of type inference on programs 5 Exhaustiveness and typing In this section we formalize our typing strat egy We call it a strategy rather than an algo rithm because its goal is to give an intuitive definition of the typing obtained rather than to pursue efficiency Since we are only interested in pattern matching we need just define patterns and their types as done in figure 1 Patterns are either a wild card a normal variant construc tor C applied to a pattern where L is the list of constructors for the corresponding sum type a polymorphic variant constructor C ap plied to a pattern a tuple including the 0 ary unit tuple or an or pattern Variables would the absence of expressions we can just replace them by wild cards This also lets us consider a whole pattern matching as a single or pattern they are equivalent for both typing and exhaus tiveness To further simplify the description we used here the same notation for normal and polymorphic variants This way we do not need to introduce explicit type definitions a normal variant is just a variant for which the construc tor list is fixed
16. led constructors and the upper bound of the corresponding polymorphic variant type comes from a direct reading of the pattern matching However if we think of deep pattern matching where polymorphic variant constructors may occur deeper in the structure then which con structors are handled in all cases is no longer trivial and we must be very careful about how we type pattern matching lest we loose sym metry for instance changing the order of the cases in a pattern matching could lead to a dif ferent type or even principality of the whole type system typing of other parts of a program could influence the typing of patterns in a non monotonic way As a matter of fact the problem of typing pattern matching has rarely been studied In most cases it is just subsumed by the typing of isomorphic expressions Outside of polymor phic variants the only specific constructs that come to mind are Standard ML record ellipsis or Objective Caml s variables in or patterns and they are not really difficult Our concern with deep matching is related to exhaustive ness check yet it differs from this previous work unfortunately only available in French 2 in that polymorphic variants are a new feature and that we need exhaustiveness information to refine our types while in general exhaus tiveness depends on the type hence we must avoid a semantic loop On the other hand while the main problem of pattern matching namel
17. ness matrix The next step is to build the exhaustiveness matrix corresponding to the inferred type This is done by induction on the structure of the type M a M unit M C of 7 Cy e M 71 B T2 X X Tn e B T X X Tn 1 ts M Ci of rit Cy e M 71 B T2 X X Tn Cn B t X X Tr 1 M t Cie B T1 X X Tn M t X XTn M T1 M t The matrix contains variant constructors C the extra constructor C and blank marks T In this definition denotes a matrix of 1 line and 0 column M N denotes matrix line wise con catenation and B r is a 1 line matrix of T s with the same number of columns as M r By line wise concatenation we mean the fol lowing operation assuming that M mj is a l line l column matrix and N nij is a k line k column matrix then P p is a lx k line I k column matrix and M i 1 k 1 j gx M i 1 modk 1 j1 J gt V Applying the above definition the exhaus tiveness matrix for p is M T F x A of P B of Q A PT B TQ Cy A PT BT Q C4 Pij iea ien i a Ma a As you can see the exhaustiveness matrix has a size exponential in the size of the type A prac tical algorithm would not build it physically but only enumerate it as needed Note that by construction each of its columns corresponds to a single variant type We note this type t M In this example t M 7 T F t
18. pe is open If it does then assuming that all other variant columns have closed types limited to the constructors inferred in step 1 check whether the lines corre sponding to an extra constructor produce an exhaustive matching If any of these two checks fails close the variant type 4 Convert all closed variant types to accep tor types i e remove the presence in formation Open variant types are not p f wild card T a variable Gp normal variant C of 7 normal variant Cp poly variant DCi of 7 polymorphic variant p p tuple Tx xT tuple plp or pattern unit unit tuple L 4 C1 Cn constructors Fig 1 Patterns and types i Mono POLY DRT Loran T l lt k lt n er SES C p C of ri b C T F Ck p Ci of 7 U TUPLE OR O uii bpm A lt i lt n Fp r Fp t l F Prs Pn i TLX X Tn Ppl per Fig 2 Typing rules modified be needed to bind values in expressions but in As you can see all steps are symmetric In particular step 2 does not privilege a row or a column over another Two different pattern matching leading to the same matrix modulo reordering of rows and columns will result in the same typing Note also that the last step means that this algorithm is not monotonous a presence type is not provably more general than an acceptor type with the same constructors Indeed it cannot be unified with an acceptor type con taining strictly less constructors In
19. s of the original types can be unified to obtain a larger type The symmetric of constructor introduction is destruction through pattern matching let show function Apple gt apple Orange s gt orange s val show lt Apple Orange of string gt string let 1 List map show 1 val 1 string list apple orange Spain As you can see the type inferred for pattern matching starts with a lt rather than a gt This denotes a list of accepted variant construc tors with the types of their arguments Again the type is polymorphic and can be applied to several kinds of variant constructors Ac ceptor types can be unified together resulting in a type accepting less constructors Presence types and acceptor types can be unified as long as all present constructors are also accepted let id function Apple gt 1 Orange _ gt 2 Pear gt 3 val id lt Apple Orange of a Pear gt int let f x show x id x val f lt Apple Orange of string gt string int While id accepts more constructors than show applying both to the same variable results in a smaller type let g x if id x 3 then Apple else x val g lt Apple Orange of b Pear gt Apple J as a gt a Since it appears in both input and output the type of x contains both acceptor and presence information The as denotes
20. y compilation has been studied for a long time already it is not directly related to our en deavor once properly typed polymorphic vari ants can easily be combined in a compilation algorithm After giving some basic notions of polymor phic variants and their typing we will see the problems caused by deep pattern matching and how they can be solved We will then give a formal account of our solution 2 Polymorphic variants basics Polymorphic variants are a standard feature of Objective Caml since version 3 To make our account more intuitive we will use exam ples typed by the Objective Caml toplevel We will not enter here into the details of the type system which can be found in other papers Polymorphic variants are particular in that a different type is constructed for each value introduced let a Apple val a gt Apple let b Orange Spain val b gt Orange of string The backquote indicates a polymorphic variant constructor When used without argu ment the type indicates just that this construc tor is present When there is an argument to the constructor its type appears in the poly morphic variant type let 1 a b val 1 gt Apple Orange of string list If you define a list containing apples and or anges then it becomes a list of apples and or anges There is actually a type variable hidden behind the gt in the above types and copie
Download Pdf Manuals
Related Search