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. |
| 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 | |
| 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 | {{{ |
| 167 | module M1 where |
| 168 | type instance H Int b where |
| 169 | ... -- sequence of patterns to dis-overlap on b |
| 170 | |
| 171 | module 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 | {{{ |
| 187 | type instance G a b where |
| 188 | G (c, d) Int = c |
| 189 | G Bool b = b |
| 190 | -- stop there |
| 191 | |
| 192 | g :: 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 | |
| 199 | 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. |
| 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 | |