Changes between Version 23 and Version 24 of NewAxioms
 Timestamp:
 Jun 24, 2013 8:50:53 AM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

NewAxioms
v23 v24 13 13 14 14 Status (Dec 12): A working implementation has been pushed to HEAD. 15 16 Status (Jun 13): A working reimplementation, with closed type families, has been pushed to HEAD. The description of the feature below is accurate as of Jun 24, 2013. 15 17 16 18 == Background == … … 55 57 Here are the changes to source Haskell. 56 58 57 * A `type instance` declaration can define multiple equations, not just one:59 * A `type family` declaration can now define equations, making a closed type family: 58 60 {{{ 59 type instancewhere61 type family Equal a b :: Bool where 60 62 Equal a a = True 61 63 Equal a b = False 62 64 }}} 63 65 64 * Patterns within a single `type instance` declaration (henceforth "branches")may overlap, and are matched top to bottom.66 * Patterns within a single closed declaration may overlap, and are matched top to bottom. 65 67 66 * A single type family may, as now, have multiple `type instance` declarations: 67 {{{ 68 type family F a :: * 68 * Open type families are unchanged. 69 69 70 type instance where 71 F [Int] = Int 72 F [a] = Bool 73 74 type instance where 75 F (Int,b) = Char 76 F (a,b) = [Char] 77 }}} 78 79 * The instances for `F` may not overlap. That is, there must be no type `t` such that `(F t)` matches more than one instance. This rule explicitly excludes overlaps among group members, even if the righthand sides coincide (but see the [wiki:NewAxioms/CoincidentOverlap Coincident Overlap] page for discussion). 80 81 * The groups do not need to be exhaustive. If there is no equation that matches, the call is stuck. (This is exactly as at present.) 70 * A closed family does not need to be exhaustive. If there is no equation that matches, the call is stuck. (This is exactly as at present.) 82 71 83 72 * An error is issued when a later equation is matched by a former, making the later one inaccessible. 84 73 {{{ 85 type instancewhere74 type family F a where 86 75 F (a,b) = [Char] 87 76 F (Int,b) = Char … … 93 82 * The equations do not need to share a common pattern: 94 83 {{{ 95 type instancewhere96 F Int = Char84 type family F a where 85 F Int = Char 97 86 F (a,b) = Int 98 87 }}} 99 88 100 * When matching a use of a type family against a branched instance, special care must be taken (by GHC) not to accidentally introduce incoherence. Consider the following example:89 * When matching a use of a closed type family, special care must be taken (by GHC) not to accidentally introduce incoherence. Consider the following example: 101 90 {{{ 102 type instancewhere91 type family F a where 103 92 F Int = Bool 104 93 F a = Char 105 94 }}} 106 95 and we try to simplify the type {{{F b}}}. The naive implementation would just simplify {{{F b}}} to {{{Char}}}, but this would be wrong. The problem is that {{{b}}} may later be unified with {{{Int}}}, meaning {{{F b}}} should simplify to {{{Bool}}}, not {{{Char}}}. So, the correct behavior is not to simplify {{{F b}}} at all; it is stuck for now. Note that the second equation above is not useless: we will still simplify, say, {{{F Double}}} to {{{Char}}}. 107 More formally, we only match a type against an equation in an instance group when no previous equation can ''unify'' against the type. 96 97 * More formally, we only match a type (called the target) against an equation in a closed type family when, for all previous equations: the LHS is ''apart'' from the target, '''or''' the equation is ''compatible'' with the chosen one. Apartness and compatibility are defined below. 98 99 * Two types are ''apart'' when they cannot simplify to a common reduct, even after arbitrary substitutions. This is undecidable, in general, so we implement a conservative check as follows: two types are considered to be apart when they cannot unify, omitting the occurs check in the unification algorithm. 100 101 * Two equations are ''compatible'' if, either, their LHSs are apart, or their RHSs are syntactically equal after substitution with the unifier of their LHSs. This last condition allows closed type families to participate in the coincident overlap that open families have supported for years. 102 103 For example: 104 {{{ 105 type family And (a :: Bool) (b :: Bool) where 106 And False a = False 107 And True b = b 108 And c False = False 109 And d True = d 110 And e e = e 111 }}} 112 All of these equations are compatible, meaning that GHC does not have to do the apartness check against the target. 108 113 109 114 == Limitations == 110 115 111 The implementation described above does not address all desired use cases. In particular, it does not work with associated types at all. (Using something like {{{type where}}} in a class definition is a parse error.) There's no set reason the approach couldn't be expanded to work with associated types, but it is not done yet. In particular, the FC extension will handle intramodule overlapping associated types without a change.The biggest reason not to add associated types into the mix is that it will be a confusing feature. Overlap among class instances is directed by specificity; overlap among family instances is ordered by the programmer. Users would likely expect the two to coincide, but they don't and can't, as it would not be type safe:116 The implementation described above does not address all desired use cases. In particular, it does not work with associated types at all. The biggest reason not to add associated types into the mix is that it will be a confusing feature. Overlap among class instances is directed by specificity; overlap among family instances is ordered by the programmer. Users would likely expect the two to coincide, but they don't and can't, as it would not be type safe: 112 117 113 118 It seems that intermodule overlapping noncoincident associated types are a Bad Idea, but please add comments if you think otherwise and/or need such a feature. Why is it a Bad Idea? Because it would violate type safety: different modules with different visible instances could simplify type family applications to different ground types, perhaps concluding {{{True ~ False}}}, and the world would immediately cease to exist.