Changes between Version 17 and Version 18 of NewAxioms
 Timestamp:
 Dec 23, 2012 5:22:41 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

NewAxioms
v17 v18 3 3 This page describes an extension to type families that supports overlap. 4 4 5 * We'll use GHC branch `overlappingtyfams` for development work.6 5 * See also the ''' [wiki:NewAxioms/DiscussionPage Discussion Page] ''' added May 2012, for comment/suggestions/requests for clarification/alternative solutions, to explore the design space. 7 6 * See also the ''' [wiki:NewAxioms/CoincidentOverlap Coincident Overlap] ''' page (added August 2012) for a discussion around the usefulness of allowing certain overlaps when the righthand sides coincide. … … 11 10 12 11 Status (Aug 12): A working prototype implementation is in `overlappingtyfams`. 12 13 Status (Dec 12): A working implementation has been pushed to HEAD. 13 14 14 15 == Background == … … 49 50 == What to do about it == 50 51 51 So the deficiency is in System FC, and it seems fundamental. We've been working on an extension to System FC, with a corresponding sourcelanguage extension, that does allow overlapping type families, with care. Here's the idea of the surfacelevel extension, but see the attached PDF for the details on the FC extension. (The attached PDF uses the FC formalism fully presented [http://www.cis.upenn.edu/~eir/papers/2013/jmnokinds/jmnokinds.pdf here].) 52 A new version of axioms is now implemented. The formal treatment can be found in docs/corespec/corespec.pdf. 52 53 53 All of the following is currently implemented in the `overlappingtyfams` branch.54 Here are the changes to source Haskell. 54 55 55 56 * A `type instance` declaration can define multiple equations, not just one: … … 60 61 }}} 61 62 62 * Patterns within a single `type instance` declaration (henceforth " group") may overlap, and are matched top to bottom.63 * Patterns within a single `type instance` declaration (henceforth "branches") may overlap, and are matched top to bottom. 63 64 64 65 * A single type family may, as now, have multiple `type instance` declarations: … … 75 76 }}} 76 77 77 * The groups for `F` may not overlap. That is, there must be no type `t` such that `(F t)` matches both groups. 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).78 * 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). 78 79 79 80 * 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.) … … 87 88 Here the second equation can never match. 88 89 89 For closed kinds (and maybe for open ones, but I can't unravel it), it seems possible to write a set of equations that will catch all possible cases but doesn't match the general case. This situation is currently ( Aug2012) undetected, because I (Richard, `eir` at `cis.upenn.edu`) am unconvinced I have a strong enough handle on the details. For example, what about {{{Any}}}?90 For closed kinds (and maybe for open ones, but I can't unravel it), it seems possible to write a set of equations that will catch all possible cases but doesn't match the general case. This situation is currently (Dec 2012) undetected, because I (Richard, `eir` at `cis.upenn.edu`) am unconvinced I have a strong enough handle on the details. For example, what about {{{Any}}}? 90 91 91 92 * The equations do not need to share a common pattern: … … 96 97 }}} 97 98 98 * When matching a use of a type family against a group, special care must be takennot to accidentally introduce incoherence. Consider the following example:99 * 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: 99 100 {{{ 100 101 type instance where … … 105 106 More formally, we only match a type against an equation in an instance group when no previous equation can ''unify'' against the type. 106 107 107 * Taking the above point into account, we will still simplify a type family use when those previous unifying equations produce coincident righthand sides. For example,108 {{{109 type instance where110 And True x = x111 And y True = y112 }}}113 and we want to simplify {{{And z True}}}. The first equation does not match. The second one does, with the substitution {{{y > z}}}! But then, the first one unifies with the substitution {{{x > True, z > True}}}. Applying both substitutions to the second righthand side ({{{y}}}) and just the second substitution to the first ({{{x}}}}), we see that both righthand sides reduce to {{{True}}} in the problematic case (which is when {{{z}}} will unify with {{{True}}} at some later point). So, we can indeed reduce {{{And z True}}} to {{{z}}} as desired. This is indeed a little fiddly, but it seems useful enough to include.114 115 * Optional extra (not yet (August 2012) implemented): It would make sense to allow the `type family` and `type instance` declaration to be combined into one, in cases where all the equations can be given at the definition site. For example:116 {{{117 type family Equal a b :: Bool where118 Equal a a = True119 Equal a b = False120 121 type family Member (a :: k) (b :: '[k]) :: Bool where122 Member a '[] = False  (not overlapping)123 Member a ( a ': bs ) = True124 Member a ( b ': bs ) = Member a bs125 }}}126 127 == Questions of syntax ==128 129 What should the "header" look like?130 {{{131 (A) type instance where  Use "where"132 F (a,b) = [Char]133 F (Int,b) = Char134 F Bool = Char135 136 (B) type instance of  Use "of" (yuk)137 F (a,b) = [Char]138 F (Int,b) = Char139 F Bool = Char140 141 (C) type instance F where  Redundantly mention F in the header142 F (a,b) = [Char]143 F (Int,b) = Char144 F Bool = Char145 }}}146 We need one of the existing "layout herald" keywords (`of`, `let`, `where`) to smoothly support the nested block of equations. It's not clear whether or not it is useful to mention the name of the function in the header.147 148 108 == Limitations == 149 109 150 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 will bea 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.110 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. 151 111 152 112 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.