Changes between Version 17 and Version 18 of NewAxioms


Ignore:
Timestamp:
Dec 23, 2012 5:22:41 AM (3 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms

    v17 v18  
    33This page describes an extension to type families that supports overlap.
    44
    5  * We'll use GHC branch `overlapping-tyfams` for development work.
    65 * See also the ''' [wiki:NewAxioms/DiscussionPage Discussion Page] ''' added May 2012, for comment/suggestions/requests for clarification/alternative solutions, to explore the design space.
    76 * See also the ''' [wiki:NewAxioms/CoincidentOverlap Coincident Overlap] ''' page (added August 2012) for a discussion around the usefulness of allowing certain overlaps when the right-hand sides coincide.
     
    1110
    1211Status (Aug 12): A working prototype implementation is in `overlapping-tyfams`.
     12
     13Status (Dec 12): A working implementation has been pushed to HEAD.
    1314
    1415== Background ==
     
    4950== What to do about it ==
    5051
    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 source-language extension, that does allow overlapping type families, with care.  Here's the idea of the surface-level 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].)
     52A new version of axioms is now implemented. The formal treatment can be found in docs/core-spec/core-spec.pdf.
    5253
    53 All of the following is currently implemented in the `overlapping-tyfams` branch.
     54Here are the changes to source Haskell.
    5455
    5556 *  A `type instance` declaration can define multiple equations, not just one:
     
    6061}}}
    6162
    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.
    6364
    6465 * A single type family may, as now, have multiple `type instance` declarations:
     
    7576}}}
    7677
    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 right-hand 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 right-hand sides coincide (but see the [wiki:NewAxioms/CoincidentOverlap Coincident Overlap] page for discussion).
    7879
    7980 * 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.)
     
    8788  Here the second equation can never match.
    8889
    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 (Aug 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}}}?
     90For 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}}}?
    9091
    9192 * The equations do not need to share a common pattern:
     
    9697}}}
    9798
    98  * When matching a use of a type family against a group, special care must be taken not 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:
    99100{{{
    100101type instance where
     
    105106More formally, we only match a type against an equation in an instance group when no previous equation can ''unify'' against the type.
    106107
    107  * Taking the above point into account, we will still simplify a type family use when those previous unifying equations produce coincident right-hand sides. For example,
    108 {{{
    109 type instance where
    110   And True x = x
    111   And y True = y
    112 }}}
    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 right-hand side ({{{y}}}) and just the second substitution to the first ({{{x}}}}), we see that both right-hand 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 where
    118   Equal a a = True
    119   Equal a b = False
    120 
    121 type family Member (a :: k) (b :: '[k]) :: Bool where
    122   Member a '[] = False                      -- (not overlapping)
    123   Member a ( a ': bs ) = True
    124   Member a ( b ': bs ) = Member a bs
    125 }}}
    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) = Char
    134             F Bool    = Char
    135 
    136 (B)      type instance of         -- Use "of" (yuk)
    137             F (a,b)   = [Char]
    138             F (Int,b) = Char
    139             F Bool    = Char
    140 
    141 (C)      type instance F where     -- Redundantly mention F in the header
    142             F (a,b)   = [Char]
    143             F (Int,b) = Char
    144             F Bool    = Char
    145 }}}
    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 
    148108== Limitations ==
    149109
    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 be 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 intra-module overlapping associated types without a change.
     110The 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 intra-module overlapping associated types without a change.
    151111
    152112It seems that inter-module overlapping non-coincident 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.