[Haskell-cafe] Using fundeps to resolve polymorphic types to
concrete types
wren ng thornton
wren at freegeek.org
Tue Jul 29 03:12:48 EDT 2008
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
More information about the Haskell-Cafe
mailing list