Changes between Version 4 and Version 5 of NewAxioms/DiscussionPage


Ignore:
Timestamp:
Jun 11, 2012 4:16:49 AM (23 months ago)
Author:
AntC
Comment:

note SPJ's clarifications; add link to Etienne's comparisons

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/DiscussionPage

    v4 v5  
    77 * Please add further comment/detail. And correct anything I've mis-represented [AntC]. 
    88 
    9 == Requests for Clarification == 
    10  
    11  * Is it possible to have more than one grouping for a given type function? (Possibly declared in separate modules.) Example: 
    12  
    13 {{{ 
    14 module M1 where 
    15     type instance H Int b  where 
    16         ... -- sequence of patterns to dis-overlap on b 
    17  
    18 module M2 where 
    19     type instance H Char b where 
    20         ... -- sequence of unrelated patterns on b 
    21 }}} 
    22  
    23   (Section 3.3 Transltion of the draft design/Law 3.6 (Consistent instance groups) seems to be saying multiple groupings are OK. An example would make it clearer.) 
    24  
    25  * Are there any rules/validation around the sequence of patterns within a grouping? 
    26  
    27   If a later pattern is more specific than an earlier (so could never get selected) is that pattern flagged, or just (in effect) silently ignored? 
    28  
    29  * Must there be a most general pattern? (By most general, I mean exactly matching the instance head. Presumably it would appear last in the group.) 
    30  
    31   If not, presumably at a use site type inference could fail to find a match. For example: 
    32  
    33 {{{ 
    34 type instance G a b where 
    35     G (c, d) Int = c 
    36     G Bool b     = b 
    37 -- stop there 
    38  
    39 g :: G Int Int               -- what happens now? 
    40 }}} 
    41  
    42  * Can inference get 'stuck'? (I'm guessing so. See the groundedness issues in the '''HList''' paper, at beginning of Section 9.) 
    43  
    44   For example, at a use site for `F a b`, we can infer `a ~ Int` and `b ~ (Num b0) => b0`, but we can't refine `b` any further. So we don't have sufficient evidence to match pattern `F a a = True`; but neither can we move on to pattern `F a b = False`. 
    45  
    46 SCW: For these last two, it would be consistent with current treatment (and with multiple groups) to allow 'stuck' type families. Perhaps GHC could flag a few more bugs if the user could specify when a type family was expected to be fully covered, but I don't think that failing to do this check will jeopardize type soundness.   
    479 
    4810== Suggestions == 
     
    7436 
    7537 
     38 * '''Idiom of total instance''' (this would apply to all the HList examples). We only need one instance group for the whole; then it's the type family decl that seems superfluous. Perhaps we could allow: 
     39{{{ 
     40    type family Equal a b :: Bool where 
     41        Equal a a = True 
     42        Equal a b = False 
     43 
     44    type family HasMember a (b :: '[]) :: Bool where 
     45        HasMember a '[] = False                      -- (not overlapping) 
     46        HasMember a ( a ': bs ) = True 
     47        HasMember a ( b ': bs ) = HasMember a bs 
     48}}} 
     49 
    7650== Alternative Solutions == 
    7751 
     
    11690 
    11791  (By the way, arguably the whole TTypeable project might have been unnecessary. Oleg built the approach because of persistent trouble around overlaps. But you can't do overlaps without fundeps (in any yet availabe version of GHC -- and Hugs is far worse.) Perhaps the trouble was really because of fundeps interfering with overlap? http://www.haskell.org/pipermail/haskell-prime/2012-May/003688.html As and when matching coercions are available, we'll be able to experiment.) 
     92 
     93== Comparisons to other approaches with overlaps == 
     94 
     95 * http://hackage.haskell.org/trac/ghc/wiki/TFvsFD [Thank you Etienne, and there's a very helpful '''See also'''.] Several examples where Type Functions don't seem to be as helpful as Type Classes/Constraints/FunDeps. Some of these examples need overlaps, but not all. Equality constraints seem to make type refinement more 'eager' than under TF's.  
     96 
     97 * http://okmij.org/ftp/Haskell/PeanoArithm.lhs [referenced from the TF vs FD discussion] 
     98 
    11899 
    119100== Comments == 
     
    132113 * '''Undecidability:''' presumably the UndecidableInstances option is still applicable, with all the issues around termination and coverage conditions. Are there any additional considerations raised by overlaps/matching coercions? 
    133114 
     115 * '''Partial vs. Total Overlap''' 
     116 
     117  Total overlap means that any substitution that fits the narrower pattern will necessarily fit the wider. Partial overlap between two patterns means that some substitutions will fit both; some only the one; some only t'other. Examples: 
     118 
     119{{{ 
     120    type instance F Int Bool = ...         -- (1) is totally overlapped by (2), (3) and (4) 
     121    type instance F Int b = ...            -- (2) partially overlaps (3) 
     122    type instance F a Bool = ...           -- (3) 
     123    type instance F a b = ...              -- (4) totally overlaps (1), (2) and (3) 
     124}}} 
     125 
     126  (For reasons I don't understand) when GHC introduced Associated Types (Families), they seemed particularly concerned about partial overlaps (and confluence thereof). Compare that Hugs handles pertial overlaps badly, so it's usually better to 'factor' into total overlaps. (That is: if you have instances like (2) and (3), add an instance like (1).) 
     127 
     128 * '''Generalisation and Unification of instance groups''' and disequality guards 
     129 
     130  Presumably common-or-garden type instances can be generalised to instance groups, and different instance groups can be unified providing their patterns don't overlap. Like this: 
     131 
     132 
    134133== Example Applications/Uses for Instance Overlap == 
    135134 
     
    148147== References and Links == 
    149148 
    150 [To do ...] 
     149 * http://hackage.haskell.org/trac/ghc/wiki/TFvsFD#SeeAlso2 
     150 
     151[More to do ...] 
    151152 
    152153Surprisingly few wiki pages discuss overlaps. 
     
    155156 
    156157See Haskell-cafe and Haskell-prime mailing lists anon. 
     158 
     159 
     160== Requests for Clarification == 
     161 
     162  (Moved to the end: SPJ has now (10 June 2012) clarified these on the main page.) 
     163 
     164 * Is it possible to have more than one grouping for a given type function? (Possibly declared in separate modules.) Example: 
     165 
     166{{{ 
     167module M1 where 
     168    type instance H Int b  where 
     169        ... -- sequence of patterns to dis-overlap on b 
     170 
     171module M2 where 
     172    type instance H Char b where 
     173        ... -- sequence of unrelated patterns on b 
     174}}} 
     175 
     176  (Section 3.3 Transltion of the draft design/Law 3.6 (Consistent instance groups) seems to be saying multiple groupings are OK. An example would make it clearer.) 
     177 
     178 * Are there any rules/validation around the sequence of patterns within a grouping? 
     179 
     180  If a later pattern is more specific than an earlier (so could never get selected) is that pattern flagged, or just (in effect) silently ignored? 
     181 
     182 * Must there be a most general pattern? (By most general, I mean exactly matching the instance head. Presumably it would appear last in the group.) 
     183 
     184  If not, presumably at a use site type inference could fail to find a match. For example: 
     185 
     186{{{ 
     187type instance G a b where 
     188    G (c, d) Int = c 
     189    G Bool b     = b 
     190-- stop there 
     191 
     192g :: G Int Int               -- what happens now? 
     193}}} 
     194 
     195 * Can inference get 'stuck'? (I'm guessing so. See the groundedness issues in the '''HList''' paper, at beginning of Section 9.) 
     196 
     197  For example, at a use site for `F a b`, we can infer `a ~ Int` and `b ~ (Num b0) => b0`, but we can't refine `b` any further. So we don't have sufficient evidence to match pattern `F a a = True`; but neither can we move on to pattern `F a b = False`. 
     198 
     199SCW: For these last two, it would be consistent with current treatment (and with multiple groups) to allow 'stuck' type families. Perhaps GHC could flag a few more bugs if the user could specify when a type family was expected to be fully covered, but I don't think that failing to do this check will jeopardize type soundness.   
     200 
     201 * Arethe examples for the multi- type instance declarations quite as intended? The heads have no head, as it were. Is this allowed? 
     202{{{ 
     203    type instance F [a] where ... 
     204 
     205    type instance F (a, b) where ... 
     206}}} 
     207  (From a documentation point of view, this shows that the instance groups are non-overlapping.) 
     208