Changes between Version 23 and Version 24 of NewAxioms


Ignore:
Timestamp:
Jun 24, 2013 8:50:53 AM (10 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms

    v23 v24  
    1313 
    1414Status (Dec 12): A working implementation has been pushed to HEAD. 
     15 
     16Status (Jun 13): A working re-implementation, with closed type families, has been pushed to HEAD. The description of the feature below is accurate as of Jun 24, 2013. 
    1517 
    1618== Background ==  
     
    5557Here are the changes to source Haskell. 
    5658 
    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: 
    5860{{{ 
    59 type instance where 
     61type family Equal a b :: Bool where 
    6062  Equal a a = True 
    6163  Equal a b = False 
    6264}}} 
    6365 
    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. 
    6567 
    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. 
    6969 
    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 right-hand 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.) 
    8271 
    8372 * An error is issued when a later equation is matched by a former, making the later one inaccessible. 
    8473{{{ 
    85 type instance where 
     74type family F a where 
    8675  F (a,b)   = [Char] 
    8776  F (Int,b) = Char 
     
    9382 * The equations do not need to share a common pattern: 
    9483{{{ 
    95 type instance where 
    96   F Int = Char 
     84type family F a where 
     85  F Int   = Char 
    9786  F (a,b) = Int 
    9887}}} 
    9988 
    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: 
    10190{{{ 
    102 type instance where 
     91type family F a where 
    10392  F Int = Bool 
    10493  F a   = Char 
    10594}}} 
    10695  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 
     103For example: 
     104{{{ 
     105type 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}}} 
     112All of these equations are compatible, meaning that GHC does not have to do the apartness check against the target. 
    108113 
    109114== Limitations == 
    110115 
    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 intra-module 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: 
     116The 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: 
    112117 
    113118It 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.