type families not advertised for 6.8
Simon Peyton-Jones
simonpj at microsoft.com
Fri Oct 19 07:44:37 EDT 2007
| But the problem in the HList example is that two equations apply where the
| most specific one should be taken.
There is no difficulty in principle with this. You just need to state (and implement) the rule that the most specific equation applies. That is, there's no reason in principle you should not be able to write
type instance Eq t t = True
type instance Eq a b = False
BUT, we need to take care here. There is one way in which indexed type family instances differ in a fundamental way from type-class instances (and hence FDs). Suppose we have
module M where
class C a where { foo :: ... }
instance C [a] where ...
Now suppose you import this into module X
module X where
import M
instance C [Int] where ...
Now, with type classes it's sort-of-OK that inside M we'll use one instance decl for (C [Int]), but a different one inside X. OK, so the two implementations of method foo will be different, but the program won't crash.
Things are different with type families. Suppose we have
module M where
type family F :: * -> *
type instance F [a] = a
module X where
import M
type instance F [Int] = Bool
Then you'll get a *seg fault* if you use the F [a] instance in one place, and the F [Int] instance in another place, when resolving a constraint involving F [Int]! (Because Bool /= Int.) That is why the current impl strictly rules out overlap for type families.
Our proposed solution is that you can only use overlapping type-family instances for "closed" type families; here "closed" means that you can't add "more" instance later. Something like this:
type family Eq :: * -> * -> * where
Eq t t = True
Eq t1 t2 = False
(The 'where' means it's a closed family.) Which is fine for the application you mention. Of course none of this is implemented!
Simon
More information about the Glasgow-haskell-users
mailing list