[Haskell-cafe] Using fundeps to resolve polymorphic types to concrete types

[wren ng thornton]

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