50 | | 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, but do look at the Latex document pointed to from the top of this page for details. |
| 50 | 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].) |
| 51 | |
| 52 | All of the following is currently implemented in the `overlapping-tyfams` branch. |
93 | | * Optional extra: 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: |
| 97 | * 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: |
| 98 | {{{ |
| 99 | type instance where |
| 100 | F Int = Bool |
| 101 | F a = Char |
| 102 | }}} |
| 103 | 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}}}. |
| 104 | More formally, we only match a type against an equation in an instance group when no previous equation can ''unify'' against the type. |
| 105 | |
| 106 | * 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, |
| 107 | {{{ |
| 108 | type instance where |
| 109 | And True x = x |
| 110 | And y True = y |
| 111 | }}} |
| 112 | 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. |
| 113 | |
| 114 | * 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: |
| 146 | |
| 147 | == Limitations == |
| 148 | |
| 149 | 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. |
| 150 | |
| 151 | It 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. |
| 152 | |
| 153 | This last point doesn't apply to overlapping type class instances because type class instance selection compiles to a term-level thing (a dictionary). Using two different dictionaries for the same constraint in different places may be silly, but it won't end the world. |