Generic Functional Logic Programs - GPD
Contents
1. Ti Te TT n does not affect Ti gt T y E ftolri gt 72 A 4 1 T ftor does not affect T T gt Te Tu TE te me ftolre 1 1 oe Thh gt Te definition of Tu 1 T gt Yiu Theorem TaT Ti y E ftv te application of substitution pepon TtT peo rt 7 YTu TtTu F Tu m gt 7 Tu Moreover it is clear that 7 is a most general unifier of Ti gt Temi and Te gt Y SO Ty Ty ftue Yri By Theorem B 2 and the type derivation for e we obtain the type inference b A Xn Bn lI e Tele and there exists a type substitution m such that Ter T4 and A Xn Bn reny AB Xn Tn ie Amer A and Bineri Ti By Remark we also know that Ane A so Ar A To prove c we need to find a type substitution m such that Te Banne n Yng Anning Let I be the set containing the indexes of the data variables in t which appear in fu e and N its complement We can define the substitution m as the simultaneous composition m Te lV ea sen Gi aime7 t E N This substitution is well defined because the domains of the two substitutions are disjoint The first component is the substitution 7m restricted to the variables which appear in its domain but not in i E N while the domain of the second component contains only the variables i N Notice that the data variables in X 2 E N do not occur in fu e so they are not involved in the t2. arbL2 Arb a gt a 10 arbL2 arb arb The expression arbP2 Bool Bool is translated into arbP2 dictArbBool dictArbBool whose evaluation generates pre cisely the values true true true false false true and false false However the expression arbL2 Bool is translated into arbL2 dictArbBool which generates only the values true true and false false The reason is that call time choice semantics imposes that the arguments of a function must be evaluated to a pattern before applying them The following reduction using let rewriting shows the problem arbL2 dictArbBool Cetin let D dictArbBool in arbL2 D iy let D dict ArbBool in arb D arb D let D dictArb arbBool in arb D arb D let B arbBool in let D dictArb B in arb D arb D Fapp Fapp t LetIn Flat bind let B arbBool in arb dictArb B arb dictArb B if let B arbBool in B B Fapp Fapp Notice that we cannot apply Bind with D bound to dict Arb arbBool because that is not a pattern as arbBool is a function totally applied Hence we introduce a new bind ing for arbBool so after some let flattening the Bind step becomes enabled and we can continue evaluating the two copies of arb dictArb B We end up with a let in which is obvious that the two elements of the resulting list will share its value Using type witnesses we solve this problem A arb Vaa a arbP2 Va 3 a 6 gt
3. gt a gt a gt Bool search x False search x y ys eq x y I less y x amp amp search x ys There are only two type classes Eq and Ord being Ord a subclass of Eq Both classes Eq and Ord contain only one function eq and less respectively The function search takes an element in the Ord class and a sorted list and returns whether the given element is in the list or not using the overloaded functions eq and less We assume that an usual type inference algorithm supporting type classes has inferred the types of functions and expressions in the program types that we will use in both translations Fig 7 a shows the usual translation of this program us ing dictionaries First every class declaration generates a dictionary type dictEq and dictOrd containing the mem ber functions and the dictionaries of its direct superclasses Every member function eq and less is converted into a pro jecting function which extracts the concrete implementation from the dictionary Functions to extract superclass dic tionaries from subclass dictionaries getEgfromOrd are also needed Every instance generates concrete implementations of the member functions eqNat and lessNat with the suit able type as well as particular dictionaries dictEqNat and dictOrdNat containing that functions and the concrete dic tionaries of its superclasses Finally every function search is extended appending as many dictionaries as class restric
4. tions appears in the context of its type and placing that dictionaries as arguments of the overloaded functions The alternative translation using type indexed functions and type witnesses appears in Figure 7 b This translation is simpler generating a program approximately as long as the original one The steps are 1 Each data type is extended with a type witness for that type The type witness of the data type C Gm is C with type Van an C Qn In the example program the wit ness generated for nat is simply nat of type nat We use the special symbol to be sure that the constructor C cannot appear in the program and to provide homogeneity to the names of the type witnesses Type witnesses are a way of representing types as values which follows the same idea of type representations 15 For example type wit nesses of bool and pair bool nat would be list bool and pair bool nat respectively 2 Member functions are extended with an extra argu ment representing the type witness In the example both eq and less functions of types Va Eq a gt a a bool and Va Ord a a a bool are extended to Va a gt a gt a bool The new first argument is the type witness of the elements to compare Like in the translation using dictionar ies each occurrence of an overloaded function in the right hand side must be completed with the corresponding type witness In the example the rule eq S x S y eq x y is
5. T A is coherent with C S so any possible type derived for the symbol c has the form Tj gt Ta gt C TI T Then after m applications of the APP rule the type derived for cti tmisC Ti T This type is not a functional one as we expected T T so we have found a contradiction Using the previous result we can now prove the Progress m3 cture ofe Proof of Progress Theorem PROOF By induction over Base case X This cannot happen because e is ground c E CS Then cis a pattern regardless of its arity n This case covers e fail f FS Depending on n there are two cases e n gt 0 Then f is a partially applied function sym bols so it is a pattern e n 0 If there is a rule f r P then we can apply rule Fapp so P H s gt r Otherwise there is not any rule l r P such that l and f unify so we can apply the rule for the matching failure Ffail obtaining P s gt fail Inductive Step 1 2 From the premises we know that there is a type deriva tion AFer m1 gt T AF e n Ate 2 T Both e and e2 are well typed and ground If e is not a pattern by the Induction Hypothesis we have P H e1 gt e and using the Contx rule we obtain P F e1 e2 of APP 15 e e2 If e2 is not a pattern we can apply the same reasoning Therefore we only have to treat the case when both e and e2 are patterns We make a distinction over the s
6. functional programs In Proc POPL 82 207 212 ACM 1982 6 A Gerdes Comparing generic programming libraries Master s thesis Dep Computer Science Open University 2007 7 J Gonzalez Moreno M Hortala Gonzalez and M Rodriguez Artalejo A higher order rewriting logic for functional logic programming In Proc ICLP 97 153 167 MIT Press 1997 8 J C Gonzalez Moreno M T Hortala Gonzalez and M Rodriguez Artalejo Polymorphic types in functional logic programming Journal of Functional and Logic Programming 2001 1 July 2001 9 J C Gonzdlez Moreno T Hortald Gonzalez F L pez Fraguas and M Rodriguez Artalejo An approach to declarative programming based on a rewriting logic Journal of Logic Programming 40 1 47 87 1999 10 C V Hall K Hammond S L Peyton Jones and P L Wadler Type classes in haskell ACM TOPLAS 18 2 109 138 1996 11 M Hanus Multi paradigm declarative languages In Proc ICLP 07 45 75 Springer LNCS 4670 2007 12 M Hanus ed Curry An integrated functional logic language version 0 8 2 March 2006 Available at http www informatik uni kiel de curry report html 13 M Hanus ed PAKCS 1 8 1 The Portland Aachen Kiel Curry System User manual 2007 14 R Hinze Generics for the masses Journal of Functional Programming 16 4 5 451 483 2006 15 R Hinze and A L h Generic programming now In Lecture notes for the Spring School on
7. GADTs which are used to allow some program rules to have a more specific type than the type for the function they define Instead of using GADT arguments to propagate this liberal typing to the arguments with which they share some type variable as we did in the eq example from Sect EI we specify this behaviour by means of these annotations which affect to each function ar gument Therefore it is easier to define functions for which we want a liberal behaviour for several independent argu ments The combination is based in B 20 a procedure that given a set of assumptions and a program calculates a type sub stitution 7 that makes the program well typed wrt the notion in that paper ane assures that well typed programs using the definition in are also well typed with the definition used in this paper so we can use to infer usual types for functions and these types will make the pro gram well typed The global procedure works stratifically in each strongly connected component of the dependency graph in a topological order If the functions in the compo nent do not have annotations B is used to infer the types of the whole block and then they are generalized Otherwise the rules are checked using Definition 3 1 Notice that pro ceeding this way the initial assumptions when type checking a block of relaxed functions will be closed Therefore the last point of the definition will hold trivially For simplic ity we assume that a
8. I e rt gt ArFe rT Theorem B 2 expresses the completeness of the inference process If we can derive a type for an expression applying a substitution to the assumptions then inference will succeed and will find a type and a substitution which are the most general ones THEOREM B 2 COMPLETENESS OF ll WRT H If An H e 7 then Jr r r All e r r A Ann An NTT 7 The following theorem shows some useful properties of the typing relation F used in the proofs THEOREM B 3 PROPERTIES OF THE TYPING RELATION a If AF e rT then Ant e rm for any 7 b Let s be a symbol not appearing ine Then AF e T lt AO s oas Fe r 13 c IfA X ta e 7 and A G X t2 b e Ta then A X Tr F X e 7 ProoF The proof of Theorems B 1 B 2 and B 3 appears in 25 REMARK B 1 IfA Xn m F e 7 and AD Xn an IH e 7 r then we can assume that Ar A B 2 Proof of Theorem B I PrRooF In and this paper the definition of well typed program proceeds rule by rule so we only have to prove that if wt f t1 tn gt e then wta f t tn gt e For the sake of conciseness we will consider functions with just one argument f t e Since patterns are linear all the variables are different the proof for functions with more arguments follows the same ideas From wta S t e we know that A H At e 7 gt 7 being 7 T4 a variant of A f Then we have a type derivati
9. Tn By Arz A D and Arrm A H we know that N An A From D and N follows O Atram Anm Ar A By O and M we have P A Xn mn Se F TET Me EET Using Theorem B 3 b we can add the type assumptions Xn Tn to the Ta ao in F obtaining Q A Xn m th Ti By wal we can replace the data variables Xn in P by expressions of the same type We use the patterns tn in Q R A Xn Tm F r0 T Finally the data variables X do not appear in r so by Theorem B 3 b we can erase that assumptions in R HAF r r Ffail and FailP Straightforward since in both cases e is fail A type derivation At fail r is possible for any T since A contains the assumption fail Va a The rest of the cases are the same as the proof in B 4 Theorem Progress For the proof of Progress we will need a result stating that junk expressions cannot have a valid type wrt any coherent set of assumptions A LEMMA B 1 Ife is a junk expression wrt a set of con structor symbols CS then there are not any A and type T such that A is coherent with CS and AF e r ProoF If e is junk then it has the form c t tn with c E CS and n gt m Since application is left associative we can rewrite this expression as c t1 tm tm41 tn In the type derivation of e appears a subderivation of the form AF cti tm i771 gt T F tm41 LET n or n AF cti tm bmi
10. X toU c z toU X Xs c s z toU X toU Xs s abbreviates iterated s s It is in this toU function where we use the specific features of our system It is interesting also to remark that in our system the truly generic rule size usize toU can coexist with the type indexed rules for size of Section I This might be useful in practice one can give specific more efficient definitions for some concrete types and a generic default case via toU conversion for other types Admittedly the type univ has less representation power than the spines of 15 that could be a better option in more complex situations But notice that since spines are based on GADTs they are also supported by us 4 4 Type Classes Type classes are according to some authors the most beloved feature of Haskell They provide a clean mod ular and elegant way of writing overloaded functions Type classes are usually implemented by means of dictionary pass ing every overloaded function receives a dictionary at run time which contains the concrete function to execute In this section we expose a new translation of type classes us ing type indexed functions and type witnesses This trans lation is interesting for a number of reasons First it obtains a gain in efficiency over the usual translation using dictio naries 10 fact that we have measured experimentally Second it also solves a problem of excess of sharing that appears in fun
11. a b arbL2 Ya a a P arb bool true arb bool false arbP2 WitA WitB arb WitA arb WitB arbL2 Wit arb Wit arb Wit The evaluation of arbP2 Bool Bool i e arbP2 bool bool obtains the same values as before However the evalu ation of arbL2 Bool i e arbL2 bool obtains the four expected values true true true false false true and false false The following reduction shows the difference arbL2 bool oe arb bool arb bool Fapp true arb bool Fapp true false 5 PRACTICAL ISSUES As we have seen the proposed type system accepts more functions than usual Damas Milner type system or the sys tem in 20 And this relaxation allows us to write type indexed functions programs with GADTs generic functions or programs with existential types However the program mer may want to write functions with the usual Damas Milner type and let the compiler to infer it We propose to combine the type system presented here and that of that is equivalent to Damas Milner for Haskell 98 like programs allowing the programmer to choose between them by means of annotations Functions annotated with relaxed will be treated by the type system proposed here therefore their type must be provided and it will be checked Otherwise they will be treated with the usual type system and their type will be inferred if not provided This is simi lar to what it is done with
12. as discussed in Section 5 Another point making type inference for functions difficult is that functions unlike expressions do not have principal types Consider the following rule not true false Possible types for the not function are Va a gt a Va a gt bool and bool bool but none of them is more general than the others In other definition of well typed programs based on type derivations is proposed we write wt P for that We have proved that programs accepted there are also ac cepted in the type system proposed in this paper THEOREM 3 1 If wt P then wta P This result is specially relevant taking into account that the type system from is equivalent to Damas Milner s system for programs not containing higher order patterns We remark that all the examples in Section 4 are rejected as ill typed by the type system in 20 Therefore the type system proposed here is a strict and useful generalization 3 4 Properties of the type system Our type system is more general than the classical Damas Milner type system or the type system in 25 How ever it still has the needed properties demanded to type systems subject reduction and progress The following the orem shows that if an expression e with type 7 is rewritten to other expression e in one step then e has also type T THEOREM 3 2 SUBJECT REDUCTION Ifwta P AF e r andPke gt e then AF e r Theorem 3 3 states that well typ
13. expression e using the Fapp rule is because e has the form f t10 tn0 being f t tm gt T a rule in P and e is r0 In this case we want to prove that At r 7 Since wta P then wta f ti tm gt e and by the definition of well typed rule Definition 3 1 we have A AS Xn san lF f ti B A Xn Bn lH r TRI wR C An TR BntR TL OnT D Arr A Arr A and Ar A By the premises we have the derivation EVAL f t10 tm TL TL tmO T where 0 Xn th Since the type derivation E exists then there exists also a type derivation for each pattern t F AF t 7 If we replace every pattern t in the type derivation E by their associated variable X and we add the assumptions Xn Tn to A we obtain the type derivation GJA Xn i Tn F f ti By A and G and T we have H 4m A Xn annem AP Xn and TLT1 T Therefore Anim A and ainet T for each i By B and the soundness of the inference Theorem B 1 DArr Xn Bntr Fr TR etm 2 T Using the fact that type derivations are closed under substi tutions Theorem a we can add the substitution m of C to I obtaining Arran Xn Bntra Fr TRT By J y C we have that K Anrntr Xn anne Fr TE Using the closure under substitutions of type derivations Theorem a we can add the substitution m of H to K L Arram Xn Annemi Fr TuT By L and H we have M Arrmm Xn
14. extended to eq nat s X s Y gt eq nat X Y 3 Normal functions using overloaded functions in its right hand side must also be completed For every type with a class constraint in the context of the type we need to add a type witness as an argument Besides it is also necessary to place the type witness as arguments of the overloaded functions As an example the original rule search x y ys eq x y Il less y x amp amp search x ys is extended to search Witness X cons Y Ys gt eq Witness X Y V less Witness Y X A search Witness X Ys Since the type of search is Ord a gt a gt a gt Bool we need to add a type witness as the first argument Witness Then this type witness is passed to the overloaded functions namely eq less and search 4 As in the translation using dictionaries goals are ex tended introducing the concrete type witnesses For example the goal search Z S Z S Z is translated to search nat z s z s z Although in Section we show how our type system allows writing type indexed functions without extra param eters in the translation of type classes we have included them The reason is that type witness are sometimes nec essary when the type variable with the class constraint ap pears only on the result type and when the rules do not use constructors in the left hand side As an example of the first situation consider the following program instance Gen Nat where gen False Z
15. flag to print the elapsed time after each expression evaluation Hugs does not print any time information but the number of reductions so we have used that information to calculate the speedup Al though it is not a real speedup we consider that it shows faithfully the gain in efficiency obtained For GHC we have used the system command time to measure the time con sumption of the compiled binary executable These exe cutables have been generated using the 02 option to enable optimizations Detailed results and source programs can be found in http gpd sip ucm es enrique publications genericF speedup zip B PROOFS AND AUXILIARY RESULTS We first present some notions used in the proofs a For any type substitution m its domain is defined as dom r a aw a and the variable range of m is Uaedom r ftv ar b Provided the domains of two type substitutions 71 and m2 are disjoints the simultaneous composition m 72 is defined as a m 72 ar if a dom m arz otherwise c If A is a set of type variables the restriction of a substitution m to A z a is defined as alas ar ifacA TIA otherwise We use 7 4 as an abbreviation of m rv a B 1 Auxiliary results Theorem B 1 shows that the type and substitution found by the inference are correct i e we can build a type deriva tion for the same type if we apply the substitution to the assumptions THEOREM B 1 SOUNDNESS OF IlF A
16. indexed functions already described in Example 3 1 and further ex ploited in Section 4 The examples of ill typed rules show a good control of existential types that could come either from HO patterns like snd X or the assumptions for constructor symbols The definition of well typed rule is simple and can be im plemented easily The first two points use the algorithm of type inference for expressions while the third is just a matching The last point which seems harder requires to calculate the intersection between the domain of three dif ferent substitutions and the free type variables of a set of assumptions However as we will see in Section this point is trivial when type checking real programs because the assumptions will be closed The definition of well typed rule assumes that a type as sumption is given for each function otherwise the inference of the left hand side fails This implies that this definition cannot be used as a type inference mechanism for the types of the functions but as a type checking method It is not a major weakness since explicit type declarations are manda tory in the presence of polymorphic recursion and other common extensions of the type system like arbitrary rank polymorphism or GADTs 32 Moreover pro grammers do include type annotations for functions in or der to document programs In any case type checking for generic functions and usual type inference can be combined in real programs
17. motivates us to think that these systems do not use the usual dictionary based translation but a more sophis ticated optimized one However our proposed translation using type witnesses can compete in efficiency with this opti mized translation being the only exception GHCi when few subclasses are used On the other hand the translation us ing type witnesses obtains an interesting gain in efficiency compared to handwritten dictionaries where the translation was performed manually by us following the specifications from 33 10 These facts encourage us to use type witnesses instead of dictionaries when implementing type classes in FLP languages since the obtained efficiency is comparable or even better to the one obtained with the dictionary tech nique in either cases Moreover our proposed translation solves a particular problem of type classes in FLP as we will see in the next section 4 4 3 Problems with dictionaries in FLP Apart from a gain in efficiency the translation using type witnesses and type indexed functions also solves a problem of undesired sharing that appears with type classes and non determinism if dictionaries are used This problem which affects type classes with member functions without argu ments was pointed out in 24 as we explain now Consider the following code class Arb a where instance Arb Bool where arb a arb True arb False arbP2 Arb a Arb b gt a b arbP2 arb arb
18. not restrict the types of variables more than left hand sides a condition that is violated in the rule for f above Definition 3 1 states that with precision and allows us to prove type safety subject reduction progress for our system Contributions We can identify a few of them e A novel even in the FP setting notion of well typed program that induces a simple and direct way of program ming type indexed and generic functions is presented in Sec tion It is based on simple calculi for what essentially is Damas Milner type derivation and inference for expres sions not for programs The approach supports also exis tential types and GADTs e At the formal level we prove that well typed programs enjoy subject reduction an essential property for a type sys tem By introducing failure rules a side contribution of our work to the formal operational calculus we also are able to ensure the progress property of well typed programs Sec tion 3 4 e We give a significant collection of examples showing the interest of the proposal in Section 4 As distinguished case study in Section 4 4 we show how to use our generic func tions to implement type classes in a way that can com pete in simplicity and performance we give experimen tal data with the traditional dictionary based approach to type classes implementation Moreover it overcomes a known problem of interference of dictionaries with call time choice seman
19. program rule gives support to existential types and GADTs opens new possibilities to genericity f i the nat ural rules for equality and apply are well typed has good properties type safety allows implementing type classes with good performance and respecting call time choice se mantics avoids unsafe uses of HO patterns One negative aspect is that types must be declared for functions but this is not so unusual moreover see Section 5 Another point yet not discussed is the following relaxing the well typedness condition has the risk of accepting some expressions than one might prefer to detect and reject at compile time This problem is always present in typed lan guages For instance in Haskell 98 the expression head is well typed but its evaluation fails and produces a run time error Being more liberal when typing a program we have more opportunities for such situations Consider for in stance our initial example of the function size with declared type Va a nat Any expression size e for any well typed e is itself well typed even if e s type is not considered in the definition of size for instance a functional type We remark however that the case is a bit odder but at least in our setting not that different from head in both cases the evaluation will fail since there is no applicable rule and notice that in our system there could be rules for size e even for functional e s thanks to H
20. tm TEITE Ad Xn Bn IF e trl wR e Irn TR BntRr n TL On7L e Att HA Anr A AT HA Fapp f t10 tn0 gt r0 if f ti tn ar EP Ffail f ti tn gt fail FailP faile fail LetIn e1 e2 gt let X e ine X Bind let X tine gt e X t Elim let X e1 in e2 f e2 if X g fv e2 Flat let X let Y e1 in e2 in e3 gt let Y e1 in let X e2 ines if X fules if C e f e using any of the previous rules LetAp let X e1 in e2 e3 gt let X e1 in e2 e3 Contx Cle f C e if A f t t gt r P such that f ti th and f t tn unify if e2 is junk active variable application or let rooted for X fresh if Y fu es Figure 2 Higher order let rewriting relation with pattern matching failure lf ID S gt S if ED Al s T HARES AFer 1 gt T APP AF e t AFee T AF e1 Tx LET A X Gen Tx A F e2 T At let X e ine T a Type derivation rules iA PP LET A X Gen Tx Arx llk e2 T 7r AF sirji 1f Als Hvar T A IIH 1 Ti T An lI ez T2 r2 if AllF e1 e2 an mitan a fresh type variable T MgJU TIT2 T2 gt a A IIF i Tx TX A llF let X e1 in eg T nXxT b Type inference rules Figure 3 where Xn var f ti tn and an Bn are fresh type variables A program P is well typed wrt A written wta P iff all its rules are
21. Datatype Generic Programming 2006 150 208 Springer LNCS 4719 2007 16 S P Jones D Vytiniotis S Weirich and M Shields Practical type inference for arbitrary rank types Journal of Functional Programming 17 1 1 82 2007 17 A J Kfoury J Tiuryn and P Urzyczyn Type reconstruction in the presence of polymorphic 18 19 20 21 22 23 24 25 28 29 30 31 32 33 recursion ACM TOPLAS 15 2 290 311 1993 K Laufer and M Odersky Polymorphic type inference and abstract data types ACM TOPLAS 16 5 1411 1430 1994 A L h and R Hinze Open data types and open functions In Proc PPDP 06 133 144 ACM 2006 F J L pez Fraguas E Martin Martin and J Rodriguez Hortala Advances in type systems for functional logic programming In Pre proc WFLP 09 157 171 June 2009 F L pez Fraguas J Rodriguez Hortala and J Sanchez Hernandez Rewriting and call time choice the HO case In Proc FLOPS 08 147 162 Springer LNCS 4989 2008 F L pez Fraguas and J S nchez Hern ndez TOY A multiparadigm declarative system In Proc RTA 99 244 247 Springer LNCS 1631 1999 W Lux Adding haskell style overloading to curry In Workshop of Working Group 2 1 4 of the German Computing Science Association GI 2008 W Lux Type classes and call time choice vs run time choice Post to the Curry mailing list August 2009 E Martin Ma
22. Generic Functional Logic Programs Technical Report SIC 03 10 2010 Francisco J L6pez Fraguas Enrique Martin Martin Juan Rodriguez Hortala Dpto de Sistemas Inform ticos y Computaci n Facultad de Informatica Universidad Complutense de Madrid fraguas sip ucm es emartinm fdi ucm es juanrh fdi ucm es ABSTRACT In this paper we provide functional logic programs with generic programming capabilities This is achieved by a remarkably simple extension of Damas Milner type system The most important aspect is a new notion of well typed pro grams which is liberal enough as to allow generic program ming but also restrictive enough as to ensure type safety for reductions as we formally prove We give an extense collection of examples showing the possibilities of our pro posal with one distinguished case of study addressing how to use our generic functions to implement type classes We show that our approach compares favorably with the tradi tional dictionary based approach to type classes implemen tation Not only we overcome a known problem of interfer ence of dictionaries with the semantics of non determinism adopted by standard functional logic languages but also the resulting translated code is simpler and exhibits better per formance than the code using dictionaries Although our proposal has been devised with functional logic programs in mind and at the formal level for instance to prove sub ject reduction we rely on oper
23. O patterns Moreover failed evaluation in FLP should not be seen as errors rather as useless branches in a possibly non deterministic compu tation space Would type classes or GADTs do any better Type classes impose more control size e is only accepted if e has a type in the class Sizeable There is a burden here you need a class for each generic function or at least for each range of types for which a generic function exists as a consequence the number of class instance declarations for a given type can be very high GADTs are in the middle way At a first sight it seems that the types to which size can be applied are perfectly controlled because only repre sentable types are permitted The problem as with classes comes when considering other functions that are generic but for other ranges of types Now there are two options ei ther you enlarge the family of representable functions facing up again the possibility of applying size to unwanted argu ments or you introduce a family of distinct representation types which is a programming overhead somehow against genericity Anyway this discussion lead us to the conclusion that our approach should not be regarded as opposed to type classes or GADTs but rather as a complementary means We find suggestive to think of the following scenario for our system TOY in the next future type classes are added to the system and implemented through our generic functions ordinary Damas Milner
24. T There are two case whether e is a pattern or not LET e e is a pattern Then we can use the Bind rule ob taining P F let X e1 in e2 f e2 X e1 e e is not a pattern Since let X e1 in ez is ground we know that e1 is ground notice that this does not force e2 to be ground Moreover A F e1 7 so by the Induction Hypothesis we can rewrite e1 to some e4 P H Using the Contx rule we can transform this local step into a step in the whole expression P let X e1 in e2 gt let X el in e2 ey of ele
25. Top top stack R Push Pop Top gt Top R makeListStack stack nil cons tail head Figure 5 Module stack as a first class citizen using existential types III Abasic length A nat append A gt A gt A add nat nat gt nat Va B a B a gt B P s X sx cons X cons X cons X Y gt cons X Y length X length X append Q X append X append X Y append X Y snd Q X snd X snd X Y gt snd X Y Figure 6 Translation HO to FO pilation of functional logic programs see e g eJm In short this translation introduces a new function symbol adds calls to in some points in the program and adds appropriate rules for evaluating it It is this latter aspect which is interesting here since the rules are not Damas Milner typeable Fig 6 contains the rules for a concrete example involving the data constructors z s nil cons and the functions length append and snd with the usual types These rules use HO patterns which is a cause of rejection in most systems Even if HO patterns were allowed the rules for would be rejected by a Damas Milner type system no matter if extended to support existential types or GADTs However using Definition 3 1 they are all well typed pro vided we declare to have the type Va 3 a b gt a b As a consequence of all this the introduction stage of the FLP compilation process can be conside
26. ans that a key constructor contains a value of some type and a function from that type to natural numbers but we cannot know exactly what type it is In functional logic languages higher order patterns can introduce the same opacity than existentially quantified con structors A prototypical example is snd X Here we know that X has some type but we cannot know anything about it from the type B of the expression A type system managing the opacity appearing in higher order patterns is proposed in 20 In that paper a distinction is made be tween opaque and transparent variables Then only trans parent variables those whose type is univocally fixed by the type of the pattern that contains them are allowed in right hand sides Therefore a rule as g snd X gt snd X is rejected since X is opaque in the pattern snd X and ap pears in the right hand side The system we propose in this paper generalizes 20 accepting functions which were re jected by the type system of those papers As an example the previous rule for g is well typed wrt the assumption g Va B a a gt 8 8 This is desirable since the rule is the identity over snd X and it will not generate any error at run time despite the opacity Figure 5 shows a stack a typical example using existen tial types borrowed from 18 The constructor stack has an existential type because the type of its first argument does not appear in the final type This fi
27. arch Dict X Ys a gt a bool gt dictOrd a search Witness X nil false Ap Abasic eq Va a gt a gt a gt bool less Va a gt a gt a gt bool nat nat search Va a a a bool Pp eq nat z z gt true eq nat z s X false eq nat s X z gt false eq nat s X s Y gt eq nat X Y less nat z false less nat s X true less nat s X z gt false less nat s X s Y gt less nat X Y search Witness X cons Y Ys eq Witness X Y V less Witness Y X search Witness X Ys Figure 7 Translation using dictionaries Aa Pa and with type indexed functions and type witnesses Aj P As an example of the second situation consider the trans lation in Figure 7 b It is well typed if we drop the type witnesses since the constructors in the left hand side force the variables to have a more specific type than in the right hand side For example in the rule eq s X s Y eq XY the variables X and Y have type nat in the left hand side because of the s constructor but they are inferred a type a a fresh type variable in the right hand side But the pro grammer could have written the instance of Eq in a slightly different way instance Eq Nat where eq eqNat being eqNat a function that calculates the equality of nat urals The resulting program without type witnesses would be rejected because the rule eq eqNat is ill ty
28. ational calculus proposed for those languages our approach is also applicable to a pure functional setting as many of our examples in particular the type classes case study show Keywords Functional logic programming generic functions type indexed functions existential types type classes 1 INTRODUCTION Functional logic programming Modern functional logic languages like Curry or Toy have a strong resemblance to lazy functional languages like Haskell 80 A remarkable difference is that functional logic programs FLP in short can be non confluent giving raise to non deterministic functions for which a call time choice seman tics pl is adopted In the HO CRWL approach to FLP M followed by the Toy system programs can use HO patterns essentially par tial applications of symbols to other patterns in left hand sides of function definitions This corresponds to an inten sional view of functions i e different descriptions of the same extensional function can be distinguished by the se This work has been partially supported by the Spanish projects TIN2008 06622 C03 01 S2009TIC 1465 and UCM BSCH GR58 08 910502 mantics This is not an exoticism it is known that ex tensionality is not a valid principle within the combination of HO non determinism and call time choice Still some people do not like HO patterns in left hand sides one of the reasons being that they cause some bad interferences with typ
29. ctional logic languages when using dictionar ies the evaluation of expressions in translated programs may lose expected values Finally the translation is simpler which makes the implementation easier and also results in smaller and more understable translated programs 4 4 1 Translation to type indexed functions The classical translation of type classes using dictionaries has been used for years in functional systems like Haskell and several optimizations have been developed 3For this to be really practical in FLP systems where there is not a first fit policy for pattern matching in case of over lapping rules a specific syntactic construction for default rule would be needed 29 Here we show a different translation that takes advan tage of the flexibility provided by our type system and uses type indexed functions and type witnesees instead of dictio naries Consider the following simple program for searching in a sorted list Notice that we have used Haskell syntax for the original program with type classes and our syntax for the translated programs class Eq a where eq a gt a gt Bool class Eq a gt Ord a where less a gt a gt Bool data Nat Z S Nat instance Eq Nat where eq ZZ True eq Z S x False eq S x Z False eq S x S y eqxy instance Ord Nat where less Z Z False less Z S x True less S x Z False less S x S y less x y search Ord a
30. ed ground expressions are not stuck wrt a well typed program i e they are patterns or we can perform a let rewriting step THEOREM 3 3 PROGRESS Ifwt P e is ground and At e 7 then either e is a pattern or Je PH e gt e The following result is a straightforward combination of the two previous theorems THEOREM 3 4 TYPE SAFETY Assume wta P e is ground and Ake tT Then one of the two following condi tions holds a e is a pattern b E e PH e gt e 0 and for every e E AFe rT 4 EXAMPLES In this section there are some examples showing the flex ibility achieved by our type system They are written in two parts a set of assumptions A over constructors and functions and a set of program rules P In the examples we consider an initial set of assumptions basic true bool false bool z nat s nat nat pair Va 8 a gt b pair a B A V bool bool bool snd Va p a p B nil Va a cons Va a gt a gt a 4 1 Type indexed functions Type indexed functions in the sense appeared in 15 are functions that have a particular definition for each type in a certain family The function size of Section 1 was an example of such a function A similar example is given in Figure Ba containing the code for an equality function which only operates with booleans natural numbers and pairs An interesing point is that we do not need a type repre s
31. entation as an extra argument of this function as we would need in a system using GADTs 4 15 In these systems the pattern matching on the GADT induces a type refine ment allowing the rule to have a more specific type than the type of the function In our case this flexibility resides in the notion of well typed rule Then a type representation is not necessary because the two arguments of every rule already fix the type of the left hand side and its variables to be more specific or the same than the inferred in the right hand side The absence of extra arguments provides simplicity to rules and programs since extra arguments im ply that all functions using eq direct or indirectly must be extended to accept and pass these arguments In contrast our rules for eq extended to cover all constructed types are the standard rules defining strict equality that one can find in FLP papers see e g 1 but that cannot be writ ten directly in existing systems like Curry or Toy because Abasic eq Va a a bool eq true true true eq true false false eq false true false eq false false true iI X Ill eq z z true eq z s X false eq s X z gt false s X s Y gt eq XY pair X Y pair X Y2 gt eq X X2 A eq Y Y2 eq eq a Original program A Abasic eq Ya repr a gt a gt a bool rbool repr bool rnat repr nat rpair Va 8 r
32. epr a gt repr B repr pair a 3 P eq rbool true true gt true eq rbool true false false eq rbool false true gt false eq rbool false false true eq rnat z z true eq rnat z s X gt false eq rnat s X z gt false eq rnat s X s Y gt eq rnat X Y eq rpair Ra Rb pair X Y pair X2 Y2 gt eq Ra X X A eq Rb Y Y2 b Equality using GADTs Figure 4 Type indexed equality they are ill typed according to Damas Milner types We stress also the fact that the program of Figure 4 a would be rejected by systems supporting GADTs while the encoding of equality using GADTs as type representations in Figure 4 b is accepted by our type system Another interesting point is that we can handle equality in a quite fine way much more flexible than in Curry or Toy where equality is a built in that proceeds structurally as in Figure ia With our proposed type system program mers can define structural equality as in 4ta for some types choose another behavior for others and omitting the rules for the cases they do not want to handle Moreover the type system protects against unsafe definitions as we ex plain now it_is known 8 that in the presence of higher order pattern structural equality can lead to the problem of opaque decomposition For example consider the snd function defined by the rule snd X Y Y and with type Va 86 a B b In this situation eq snd z s
33. er for instance the program Pi true A X X false X false and the expres sion let Y true in Y true The application Y A true unifies with the function rule left hand side true A X so no failure is generated If we use pattern matching as condition a failure is incorrectly generated since neither true A X nor false X match with Y Atrue Using unification in Ffail can contribute also to early detection of failures Consider the program P2 f true false true g g and the expression let Y gin f Y Y Since f Y Y does not unify with f true false Ffail detects a failure while other op erational approaches to failure in FLP would lead to a divergence Notice that in presence of non determinism call time choice semantics is essential for Ffail to be sound Finally rule FailP is used to propagate the pattern match ing failure when it is applied to other expression Notice that since let rewriting is lazy the occurrence of a pattern matching failure in a subexpression does not always force the whole expression to be reduced to fail 3 2 Type system and type inference Both derivation and inference rules are based on those presented in Our type derivation rules for expres sions Figure 3ta correspond to the well known variation of Damas Milner s type system with syntax directed rules Gen r A is the closure or generalization of r wrt A which generalizes all the type variables of 7 that do not appear f
34. ere invented to deal with those situations Some further developments of the idea of generic programming e g 14 are based on type classes while others e g 15 have preferred to use simpler extensions of Damas Milner system such as GADTs see also 6 for a survey on generic functional programming Our paper aims at providing also FLP with abilities for generic programming Noticeably our solution is applicable also in a pure FP setting The following example should serve to illustrate the main points An introductory example Consider a program that manipulates several constructor data types Peano natural numbers given by the constructors z d booleans and poly We follow syntactic conventions of some functional logic languages where function and constructor names are lower cased and variables are uppercased morphic lists Programming a function size to compute the number of constructor occurrences in its argument is an easy task in a type free language with functional syntax size true s z size false gt s z size z gt sz size s X gt s size X size sz size X Xs s add size X size Xs assuming a natural definition for add However as far as bool nat and a are different types this program would be rejected as ill typed in a language using Damas Milner sys tem since we obtain contradictory types for different rules of size This is a typical case where one wants some support for
35. es Some works have addressed that problem and this paper does further contributions to overcome it All those aspects of FLP will play a role in the paper and in Section 3 we use a formal setting according to that However most of the paper can be read from a standard functional programming perspective where it offers also hopefully interesting novelties leaving aside the specifici ties of FLP Types FLP and genericity FLP languages are typed languages adopting classical Damas Milner types 5 How ever their treatment of types is very simple far away from the impressive set of possibilities offered e g for Haskell type and constructor classes existential types GADTs ge neric programming arbitrary rank polymorphism Some exceptions to this fact are some preliminary proposals for type classes in FLP 27 23 where in particular a technical treatment of the type system is absent The term generic programming is not used in the liter ature in a unique sense With it we refer generically to any situation in which a program piece maybe something as simple as a function name serves for a family of types instead of a single concrete type Parametric polymorphism as provided by Damas Milner system is probably the main contribution to genericity in the functional programming setting However in a sense it is too generic and leaves out many functions which are generic by nature like equality Type classes w
36. gen True 5S2Z class Gen a where gen Bool gt a If we do not use a type witness the translated rules of gen in the instance Gen Nat are gen false z and gen true gt s z They are ill typed wrt the type gen Va bool a because the type inferred for the right hand side nat is more specific than the type inferred for the left hand side a When we introduce the type witness nat to the rules we obtain gen nat false z and gen nat true gt s z and the type gen Va a bool a Here type witness forces both sides to have type nat making the rules well typed eqNat nat nat bool lessNat nat nat bool search Dict X nil false Aa Avasic dictEq Va a a bool dictEq a dictOrd Va dictEq a eq Va dictEg a a gt a gt bool less Va dictOrd a a gt a bool getEqfromOrd Va dictOrd a dictEq a dictEqNat dictEq nat dictOrdNat dictOrd nat search Va dictOrd a a a bool Pa eq dictEq X gt X less dictOrd X Y gt Y getEqFromOrd dictOrd X Y gt X eqNat z z true eqNat z s X gt false eqNat s X z gt false eqNat s X s Y eqNat X Y lessNat z z false lessNat z s X true lessNat s X z false lessNat s X s Y gt lessNat X Y dictEqNat dictEq eqNat dictOrdNat dictOrd dictEqNat lessNat search Dict X cons Y Ys eq getEqFromOrd Dict X Y V less Dict Y X se
37. genericity Type classes certainly solve the problem if you define a class Sizeable and declare bool nat and a as instances of it A price to pay is that the running program is not the program above but the result of adding hidden dictionaries GADT based solutions would add an explicit representation of types to the encoding of size converting it into a so called type indexed function GADTs are also supported by our system see Section and 4 1 but the interesting point is that our approach allows also a simpler solution the program above becomes well typed in our sys tem simply by declaring size to have the type Va a nat of which each rule of size gives a more concrete instance Moreover the well typedness criterion requires only a quite simple additional check over usual type inference for expres sions Simple does not mean naive Imposing the type of each function rule to be an instance of the declared type is a too weak requirement leading easily to type unsafety As an example consider the rule f X not X with the assumptions f Va a bool not bool bool The type of the rule is bool bool which is an instance of the type declared for f However that rule does not preserve subject reduction the expression f z is well typed according to f s declared type but reduces to the ill typed expression not z Our notion of well typedness roughly explained requires also that right hand sides of rules do
38. ication of type substitutions to simple types is defined in the natural way and for type schemes consists in applying the substitution only to their free variables This notion is extended to set of assumptions in the obvious way We will say o is an in stance of o if o o r for some m A simple type 7 is a generic instance of o Yan T if tT Tlan Tn for some Tr and we write it o gt T Finally 7 is a variant of o Van T 0 var T if T Tlan Bn and Bn are fresh type variables 3 FORMAL SETUP 3 1 Semantics As the operational semantics of our functional logic pro grams we have chosen let rewriting 21 a simple and high level notion of reduction step devised to express the seman tics of call time choice inspired by 2 We have extended it for this paper with two more rules for managing failure of pattern matching Figure 2 an aspect that can be inter esting in its own The new rule Ffail generates a pattern matching failure when no program rule can be used to re duce an expression Notice the use of unification instead of simple pattern matching to check that the variables of the expression will not be able to match the patterns in the rule This allows us to perform this failure test locally without having to consider the possible bindings for the free variables in the expression caused by the surrounding con text Otherwise these should be checked in an additional condition for Contx Consid
39. itnesses than dictionaries Consider a func tion with type f Eq a Show a gt a gt Bool In the common translation we introduce a dictionary for every class constraint in the type of the function Therefore this function needs two extra paremeteres f Va dictEq a gt dictShow a a bool However only one type witness is necessary since both class contraints Eq a and Show a affect the same type a f Va a a bool We have measured the real gain in efficiency obtained using type witnesses and type indexed functions instead of handwritten dictionaries and built in type classes over dif ferent systems Translated programs using dictionaries are valid in all the systems since they only need a Damas Milner type system Programs using type witnesses and type indexed functions require an implementation with our proposed type system None of the tested systems support it so we have followed two solutions For TOY 2 3 1 we have used an spe cial version disabling type checking This does not distort the measures since once compiled programs do not carry any type information at run time so compiled programs are the same regardless of the chosen type system For the rest of the systems GHC 6 10 4 Hugs Sept 2006 and PAKCS 1 9 1 7 13 we have included all the data constructors in side the same universal data type Thus only one instance for each type class is needed and all the rules fit inside mak ing the program we
40. ll the functions in a strongly connected component will have the annotation relaxed or not i e combinations of relaxed and usual functions are not allowed in the components The following example shows the method in a very simple program EXAMPLE 5 1 Program with annotations relaxed eq A gt A gt bool eq false false true eq false true true eq z z true eq z s X false isFalse X eq X false isFalse depends on eq but not viceversa Therefore each one forms a strongly connected component eq will be first treated Since it has a Qrelaxed annotation its type will be checked using Definition 5 1 The rules of eq are well typed wrt Va a gt a gt bool so isFalse will be treated next As it does not have any annotation the usual method will be used inferring the type bool bool Apart from functions in this paper data constructor are also relaxed since they can have any type provided it is co herent with CS For them we propose a syntax similar to GADTs where the type of each one is given explicitly by the programmer 6 CONCLUSIONS Starting from a simple type system essentially Damas Milners s one we have proposed a new notion of well typed 11 program that exhibits interesting properties Let us give a short final summary and discussion of pros and cons of our proposal some of them discussed more thoroughly before In the positive side it is simple needs only a check for each
41. ll typed We have measured the speedup in programs with differ ent levels of subclasses Figure 8 The obtained speedup grows almost linearly with the subclass depth in all the cases except in GHC using handwritten dictionaries In general terms the translation using type witnesses performs faster with an speedup ranging from 1 1 3 using one subclass to 1 5 2 5 when nine subclasses are used The only exception is in GHCi using the built in type classes where the trans lation using type witnesses runs about a 10 slower for one subclass although for higher subclass depth the time 4 Although this problem can be solved flattening the dictio nary structure 3 OU TOY handwritten dictionaries PAKCS handwritten dictionaries GHCi built in type classes GHCi handwritten dictionaries GHC built in type classes m GHC handwritten dictionaries F 25 4 ae Hugs built in type classes soo Hugs handwritten dictionaries Speedup 0 5 T T 7 T T T T Subclass Depth Figure 8 Speedup of the translation over different systems used in both translation is the same Detailed results and source programs can be found in http gpd sip ucm es enrique publications genericFLP speedup zip As Figure 8 shows in all the Haskell systems the ob tained speedup is greater when compared to handwritten dictionaries than when compared to built in type classes This
42. nd true is well typed but after a decomposition step using the struc tural equality we obtain eq z true which is ill typed Dif ferent solutions have been proposed B but all of them need fully type annotated expressions at run time which penal izes efficiency With the proposed type system that over loading at run time is not necessary since this problem of This situation also appears with first order patterns con taining data constructors with existential types opaque decomposition is handled statically at compile time we simply cannot write equality rules leading to opaque de composition because they are rejected by our system This happens with the rule eq snd X snd Y gt eq X Y which will produce the previous problematic step It is re jected because the inferred type for the right hand side and its variables X and Y is bool y y which is more more spe cific than the inferred in the left hand side bool a 3 This is a good example of how our system combines flexibility with control Our next section pursues that idea 4 2 Existential types opacity and HO patterns Existential types appear when type variables in the type of a constructor do not occur in the final type For example the constructor key Va a a nat key has an existential type since does not appear in the final type key This type is called existential because it can be viewed as da a a nat key In practice this me
43. o not support re cursive definitions the bindings of the variable only affect e2 follet X e1 in e2 fu e1 U fu ez X We say that an expression e is ground if fu e A one hole context C is an expression with exactly one hole A data substitution 0 is a finite mapping from data variables to patterns Xn tn Substitution application over data variables and expressions is defined in the usual way The empty substitution is writ ten as id A program rule r is defined as f t e where the set of patterns is linear there is not repetition of vari ables and fu e C U ezvar t Therefore extra variables are not considered in this paper The constructor fail is not supposed to occur in the rules although it does not produce any technical problem A program P is a set of program rules r1 7n n gt 0 For the types we assume a denumerable set TV of type variables a and a countable alphabet TC Ucn TC of type constructors C As before if C TC then we write ar C n Figure I shows the syntax of simple types and type schemes The set of free type variables ftv of a sim ple type 7 is var r and for type schemes ftv Yan T ftu r an We say a type scheme a is closed if ftu a A set of assumptions A is 5n 0n where si DCU FSU DY We only consider coherent sets of assumptions wrt C S DEFINITION 2 1 COHERENCE OF A WRT CS A set of assumptions A is coherent wrt a set of constructor
44. on of the form A Xn mmi F tin AS Xn Tmn Fe r AF Ate rl A and we know that critVar At e 0 i e that opaqueVar4 t N fv e We want to prove that A Xn san Qn lk ft TL TL A Xn Bn IIF e TRI wR T TR BnTR T TL On7L Arr A Anr A AT A Lu By the type derivation of t and Theorem B 2 we obtain the type inference A Xn 1 Qn An lF t Te Te and there exists a type substitution m such that Teny T and A Xn i an On mm AP Xn Tn ie Amma A and aimn Ti Moreover from critVar At e we know that for every data variable X fu e then ftv aim C ftu r Then we can build the type inference for the application f t A Xn an l f 7 rid A Xn an id IIF t Telme iA a AG Xn san lF f t yag te7g By Remark B 1 we are sure that Am A Since 7 gt T4 is a variant of A f we know that it contains only free type variables in A or fresh variables so Tt gt T2 t Ti gt T4 In order to complete the type inference we need to create a unifier 7 for tT 72 and Te y being y a fresh type variable Notice that by Theorem B 2 we know that Amn A and by Remark B 1 Am A so An A Since Tt T4 contains only type variables which are free in A or fresh type variables generated during the inference 7 will not affect it Defining mu as 77 feo 7 y 7 we have an unifier since
45. ped wrt the assumption eq Va a a bool as the right hand side has a more specific type nat nat bool than the left hand side a a bool Using a type witness the rule will be eq nat eqNat which now is well typed since both sides have type nat nat bool wrt the assumption eq Va a gt a gt a gt bool The possibility of a translation using type representa tions instead of dictionaries was already mentioned in 4 although it was not further developed In the next two sub sections we will show that this translation generates more efficient programs and also solves a problem of excess of sharing in FLP when using the common translation of dic tionaries 4 4 2 Efficiency The structure of type witnesses depend on the data type unlike dictionaries whose structure depends on the type class they contain the member functions and the dictionar ies of the direct superclasses It is difficult to compare their size because it is highly program dependent Programs with many nested type classes and many member function will require big dictionaries even for basic data while programs with few classes and member functions will need big type witnesses if the overloaded functions are applied to complex data With dictionaries member functions must be extracted before applying them and it can mean traversing a chain of superclasses dictionaries Another point in favor is that we need less type w
46. rce snd X gt cons z X X IIl at oF The rule of snd is trivially well typed The rule for cast is not well typed since the tuple TL Qn7L inferred for the left hand side is 7 6 which is not matched by the tuple n n inferred as Tr BntR for the right hand side This shows the problem of existential type variables which escape from the scope If that rule were well typed then subject reduc tion could not be granted anymore e g consider the step cast snd true f true where the type nat can be as signed to cast snd true but true can only have type bool The rule eq is well typed because the tuple inferred for the right hand side bool y matches the one inferred for the left hand side bool nat In the rule for show the inference obtains char nat for the left hand side and char nat for the right hand side so it is well typed Finally the rule for force is not well typed because the tuple nat y in ferred for the left hand side is not an instance of the tuple nat nat inferred in the right hand side This shows the problem of a existential type variable rigid variable which has a concrete type in the right hand side Notice that the last point of the definition holds trivially in all the rules because A is closed The examples of well typed rules together with the fact that well typedness for programs simply proceeds rule by rule suggest the capabilities of our notion for type
47. red as a source to source transformation instead of a hard wired step 4 3 Generic functions According to a strict view of genericity the functions size and eqin Sections I and 4 Tare not truly generic We have a definition for each type instead of one canonical definition to be used by each concrete type However we can achieve this by introducing a universal data type over which we define the function we develop the idea for size and then use it for concrete types via a conversion function This can be done by using GADTs to represent uniformly the applicative structure of expressions for instance the spines of 15 by defining size over that uniform represen tations and then applying it to concrete types via conver sion functions But again we can also offer a similar but simpler alternative A uniform universal representation of constructed data can be achieved with a standard data type data univ c nat univ where the first argument of c is for numbering constructors and the second is the list of arguments of a constructor ap plication A universal size can be then defined as usize c__ Xs s foldr add z map usize Xs using some functions of Haskell s prelude Now a generic size can be defined as size usize toU where toU is a conversion function with declared type toU Va a univ toU true gt c z toU false c s z toU z gt c z toU s X c z toU
48. ree in A Formally Gen r A V n 7 where an ftu r ftv A The type inference algorithm IlI Figure 3 b follows the same ideas that wf We have given the type inference a relational style to show the similarities with the typing rules But in essence the inference rules represent an algo rithm which fails if any of the rules cannot be applied This algorithm accepts a set of assumptions A and an expression e and returns a simple type 7 and a type substitution 7 Intuitively T is the most general type which can be given to e and r the most general substitution we have to apply to A in order to be able to derive any type for e 3 3 Well typed programs In the functional setting the problem of checking if a pro gram is well typed is reduced to checking that an expression has a valid type because programs can be written as a chain of let expressions defining the functions accompanied with a goal expression to evaluate Doing that in our formalism would not preserve call time choice semantics and further more we do not consider A abstractions Therefore we need an explicit definition of how to check that a program is well typed The following definition is the main contribution of this paper and it is based on type inference for expressions DEFINITION 3 1 WELL TYPED PROGRAM WRT A The program rule f t tm e is well typed wrt a set of assumptions A wta f t1 tm e iff A Xn anh lF f ti
49. rst argument is the con crete implementation of the stack and the other arguments are functions that push an element in the stack remove the last element and ask for the last element We do not know anything about the implementation of the stack but we are sure that the contained functions operate correctly with that implementation Therefore we can write the functions push pop and top which extract the respective function and apply it to the implementation We can create stacks with differ ent implementations but these functions will work for all the stacks Notice that all the rules except makeListStack are ill typed in 20 This example shows how using existen tial types we can create first class abstract data types that can be passed and returned by functions Therefore at run time we can mix stacks with different implementations crate copies of stacks with different implementations or add new implementations As far as we know this kind of flexibility cannot be easily achieved using modules Another remarkable example is given by the well known translation to first order usually used as a stage of the com stack Va 3 3 a B Bb 8 B 8 gt a gt stack a push Va a stack a stack a pop Va stack a stack a top Va stack a gt a makeListStack Va stack a push X stack R Push Pop Top stack Push X R Push Pop Top pop stack R Push Pop Top gt stack Pop R Push Pop
50. rtin Advances in type systems for functional logic programming Master s thesis Universidad Complutense de Madrid July 2009 Available at J C Mitchell and G D Plotkin Abstract types have existential type ACM Transactions on Programming Languages and Systems 10 3 470 502 1988 J J Moreno Navarro J Mari o A del Pozo Pietro A Herranz Nieva and J Garcfa Martin Adding type classes to functional logic languages In Proc APPIA GULP PRODE 96 427 438 1996 M Odersky and K Laufer Putting type annotations to work In Proc POPL 96 54 67 ACM 1996 J Peterson and M Jones Implementing type classes In Proc PLDI 93 227 236 ACM 1993 S Peyton Jones Haskell 98 Language and Libraries The Revised Report Cambridge Univ Press 2003 J Sanchez Hernandez Constructive failure in functional logic programming From theory to implementation Journal of Universal Computer Science 12 11 1574 1593 2006 T Schrijvers S Peyton Jones M Sulzmann and D Vytiniotis Complete and decidable type inference for GADTs In Proc ICFP 09 341 352 ACM 2009 P Wadler and S Blott How to make ad hoc polymorphism less ad hoc In Proc POPL 89 60 76 ACM 1989 APPENDIX A MEASUREMENT OF THE SPEEDUP For each system and subclass depth we have performed 100 speedup measurements The mean of these speedups is the value which appears in Figure For interpreted sys tems we have activated the corresponding
51. sym bols CS if for every constructor symbol c in CS different from fail c CS implies A c V 711 gt C TL Tm with ar C m and A fail Va a Therefore the assumptions for constructors are related with their arity On the other hand the assumption for fail together with the rules of the type system presented Data variables X Y Z Type variables a 3 7 Data constructors c Type constructors C Function symbols f Expressions e X c flee let X eine Patterns t A cty tn ifn lt ar c f ti tn ifn lt ar f Symbol s X clf Non variable symbol h of Simple Types T a C Tita ifar C n TOT Type Schemes o 7 Va r Assumptions A s1 01 8n on Program rule r x ft e t linear Program P a E Data substitution O a Aata Type substitution T an Tn Figure 1 Syntax of expressions and programs in Section 3 2 allow fail to appear at any place of a well typed expression The union of sets of assumptions is de noted by A A contains all the assumptions in A and the assumptions in A over symbols not appearing in A For sets of assumptions ftu 3n gt On U ftv oi Notice that type schemes for data constructors may be ex istential i e they can be of the form Va n T T where Une ftu mi x fto r 0 If s o A we write A s o A type substitution m is a finite mapping from type variables to simple types an T Appl
52. tics e Our well typedness criterion goes far beyond the solutions given in previous works to type unsoundness prob lems of the use of HO patterns in function definitions We can type equality solving known problems of opaque decom position Section 4 3 and most remarkably we can type the apply function appearing in the HO to FO translation used in standard FLP implementations Section 4 2 2 PRELIMINARIES We assume a signature X DCU FS where DC and FS are two disjoint sets of data constructor and function sym bols resp all them with associated arity We write DC resp FS for the set of constructor function symbols of arity n and if a symbol h is in DC or FS we write ar h n We consider an special constructor fail DO to represent pattern matching failure in programs We also assume a denumerable set DV of data variables X Fig ure 1 shows the syntax of patterns Pat and expressions Exp We split the set of patterns in two first order pat terns FOPat 3 fot X c t tn where ar c n and higher order patterns HOPat Pat FO Pat i e patterns containing some partial application of a symbol of the sig nature Expressions c e1 n are called junk if n gt ar c and c fail and expressions f 1 en are called active ifn gt ar f fv e is the set of variables in e which are not bound by any let expression and is defined in the usual way notice that since our let expressions d
53. tructure of the pattern e1 e X This cannot happen because e is ground ect tn with c E CS and n lt m Depending on m and n we distinguish two cases n lt m Then e1 e2 is c t tn e2 withn 1 lt m which is a pattern n m x If c fail then m n 0 so we have the expression fail e2 In this case we can apply rule FailP so P H fail e2 gt fail x Otherwise e1 e2 is c t tn e2 with n 1 gt nm which is junk This cannot happen because A is coherent and A F e1 e2 T and Lemma B 1 states that junk expressions cannot be well typed wrt a coherent set of assumptions e f t1 tn with c E FS and n lt m Depending on m and n we distinguish two cases n 1 lt m Then e1 e2 is f t tn e2 which is a partially applied function symbol i e a pattern n 1 m Then e1 e2 is f t tn e2 If there is a rule l gt r P such that 10 f t tn e2 then we can apply rule Fapp so P F e1 e2 gt f r0 If such a rule does not exist then there is not any rule U r P such that l and f ti tn e2 unify Notice that since f t tn e2 is ground it does not have variables so in this case pattern matching and unification are equivalent Therefore we can apply the rule for the matching failure Ffail obtaining P F e1 ef fail let X e in e2 From the premises we know that there is a type derivation At e1 Tx AS X Gen Tx A F e2 7 At let X e in e2
54. typing and generic typing can be freely mixed using annotations as described in Section 5 the programmer can choose the feature ordinary types classes GADTs or our more direct generic functions that best fits his needs of genericity and or control in each specific situation Apart from the implementation work to realize that vi sion will require further developments of our present work e A formal specification of the translation of type classes into our generic functions following the ideas sketched in Section It should cover also constructor classes and multipa rameter type classes e Despite of the lack of principal types some work on type inference can be done in the spirit of 32 e Combining our genericity with the existence of modules could require adopting open types and functions 19 e Narrowing which poses specific problems to types should be also considered 7 REFERENCES 1 S Antoy and A P Tolmach Typed higher order narrowing without higher order strategies In Proc FLOPS 99 335 353 Springer LNCS 1722 1999 2 Z M Ariola M Felleisen J Maraist M Odersky and P Wadler A Call by need Lambda Calculus In Proc POPL 95 233 246 ACM 1995 3 L Augustsson Implementing haskell overloading In Proc FPCA 93 65 73 ACM 1993 4 J Cheney and R Hinze First class phantom types Technical report Cornell University July 2003 5 L Damas and R Milner Principal type schemes for
55. well typed The first two points check that both right and left hand sides of the rule can have a valid type assigning some types for the variables Furthermore it obtains the most general types for those variables in both sides The third point is the most important It checks that the type inferred for the right hand side and the variables appearing in it are more general than the inferred for the left hand side This fact guarantees the subject reduction property i e that an ex pression resulting after a reduction step can have the same type as the original one when applying a program rule Moreover this point ensures a correct management of both skolem constructors and opaque variables 20 intro duced either by the presence of existentially qualified con structors or higher order patterns Finally the last point guarantees that the set of assumptions is not modified nei ther by the type inference nor the matching substitution EXAMPLE 3 1 WELL AND ILL TYPED RULES Let us con Type system sider the following assumptions and program A z nat s nat nat true bool false bool cons Va a a gt a rnat repr nat snd Va b a gt b gt P cast Va 3 a gt a gt 8B eq Va a bool show Va repr a a gt char showNat nat char force Va a gt a nat snd X Y Y cast snd X gt X eq s X z gt false show rnat X showNat X fo
56. ype inference for e Therefore the type variables in 2 E N do not appear in ftv te dom me or vRan me With this substitution 7 the equality Te Bnte m Yng AnntTg holds because e Since Ter T and the type variables in 3 i N do not occur in ftu te we know that Tem Tene N 1 ieN a a Tene Te YTg e We know that the variables in X i I cannot be opaque in t so ftv aim C ftu m for every i I and aititg aimT fev 7 Ti for those variables Since the type variables f i N do not occur in vRan re then binet Binene 3 teN binene Ti QintTg for every i I e Since the type variables f i N do not occur in dom tre then Binter Bir QuTtTg for every i N Finally we have to prove that d Ama A Ane A and Ar A For the first case we already know that Am A and Ary A Since rg is defined as my ptv r Y r and y is a fresh type variable not appearing in ftv A then Amn Ang AT ftum A For the second case Are A holds using Remark For the last case we know that Arg A Since 7 is defined as 72 a ten G aim 7 i E N and no type variable 8 appears in ftv A they are fresh type variables then Ar Ar A 14 B 3 Proof of Subject Reduction Theorem 3 2 PROOF We proceed by case distinction over the rule of the let rewriting relation Figure 2 used to reduce e to e Fapp If we reduce an
Download Pdf Manuals
Related Search