Changes between Version 4 and Version 5 of NewAxioms/DiscussionPage


Ignore:
Timestamp:
Jun 11, 2012 4:16:49 AM (3 years 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