Bryan Donlan wrote:
Hi,
Is there any theoretical reason that functional dependencies can't be used to resolve a polymorphic type to a concrete type? For example:
-- compile with -fglasgow-exts
class DeriveType a b | a -> b
data A = A data B = B
instance DeriveType A B
simpleNarrow :: DeriveType A b => b -> B simpleNarrow = id
I'm not entirely sure what your use case is, but the reason this fails is that you gave a type signature which is more general than what the body can possibly be. Even with fundeps, the signature is claiming that the function works for *any* b provided it happens to be the right one for DeriveType A. That is, the signature is somewhat agnostic to whatever actual implementations happen to exist [though it must be consistent with them]. A true (DeriveType A b => b -> B) function would work even if we edited the instance declaration to be for DeriveType A C instead. And naturally 'id' is (a -> a) so giving a return type of B requires that the input type must also be B. It compiles just fine with (DeriveType A b => b -> b) after all, which resolves directly to (B -> B) [which I think is what you want?]. Though again, if we changed the instance then it would resolve to (C -> C) instead.
The motivation is this case:
data ComplexType a where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a
specialCaseFunc :: ComplexType A -> B specialCaseFunc (SomeConstructor _ b) = b
Again the issue is that while the instance declaration says that the result happens to be B now, that's not what the "real" type of the result is-- it's (DeriveType A b => b) where b is *exactly* the one from the SomeConstructor signature, and hence the signature (DeriveType A b => ComplexType A -> b) doesn't work either since that's a different b. Since b --whatever it happens to be-- is fixed by A it seems like the (DeriveType A b => ComplexType A -> b) signature should work and consider it the same b. However, since the GADT is doing existential quantification, even though the b type is fixed we've lost that information and so we can't be certain that it *really* is the same b. If you're familiar with existential quantification then the behavior makes sense, though I agree it isn't quite what would be expected at first. I'm not sure off hand whether it should really be called a bug however. If you don't really need the existential in there, then this version works just fine:
{-# OPTIONS_GHC -fglasgow-exts #-}
class DeriveType a b | a -> b
data A = A data B = B
instance DeriveType A B
simpleNarrow :: DeriveType A b => b -> b simpleNarrow = id
data ComplexType a b where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a b
specialCaseFunc :: ComplexType A b -> b specialCaseFunc (SomeConstructor _ b) = b
Essentially, if I have a data structure with two types used as fields, and one uniquely determines the other, I'd like to use these instances to avoid re-stating the implied one in the type equations, if possible.
If you do want the existential after all, you can keep it provided the context restriction [i.e. DeriveType] gives you a method to get it back. If all you're doing is type passing then an implementation like this works just fine:
class DeriveType a b | a -> b where someDestructor :: ComplexType a -> b
instance DeriveType A B where someDestructor _ = B
data ComplexType a where SomeConstructor :: DeriveType a b => a -> b -> ComplexType a
[1 of 1] Compiling Main ( fundep.hs, interpreted ) Ok, modules loaded: Main. *Main> someDestructor (SomeConstructor undefined undefined :: ComplexType A) B *Main> But if you have actual values rather than just unit types, note that this won't work:
instance DeriveType A B where someDestructor (SomeConstructor _ b) = b
The key to note here is that when we existentially quantify over b and loose the type information, any class dictionaries for b are packaged up with the value and can still be used to get views onto the value of b. We can only get *views* onto b but can't do anything which might recover information about the actual type of b, however [aka "existential escapes"]. So this may or may not be sufficient for your needs. The fact that existential quantification looses information which can never be recovered is one of the reasons why they can be difficult to deal with. -- Live well, ~wren