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

[wren ng thornton]

Ryan Ingram wrote:
> Hmm, I'm kind of confused by this now.  I feel like the following code
> really should compile, but it doesn't.  There's no use of existentials
> to hide type information at all.  The functional dependency seems like
> it should give us the constraint (b1 ~ b2) allowing Refl to typecheck.

It may be worth noting that GADTs subsume existential types. Not that 
that matters here.


>> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GADTs #-}
>> module DeriveType where
>>
>> class DeriveType a b | a -> b
>> data TypeEq a b where Refl :: TypeEq a a
>>
>> test :: (DeriveType a b1, DeriveType a b2) => a -> TypeEq b1 b2
>> test _ = Refl
> 
> But...
> 
> derivetype.hs:8:9:
>     Couldn't match expected type `b1' against inferred type `b2'

Like I was saying, contexts are only ever verified as constraints on 
polymorphism, they never drive the type inference algorithm. Think of 
them as something that happens after the fact, "delayed constraints" if 
you will.

The constructor Refl defines a constant of type (forall t. TypeEq t t). 
This constrains the return type of 'test' to have the same type, namely 
that the two arguments to the TypeEq type constructor are both the same. 
The signature you gave is more polymorphic than that, it allows for the 
possibility that they might be different. This is the same as the 
previous example using 'id' and wanting to give it the type (b -> B).

If we simplify the example it might be more apparent why it fails.

     [0] wren at xenobia:~/test $ cat wacky2.lhs && ghci wacky2.lhs
     > module DeriveType where
     >
     > data TypeEq a b = TE
     >
     > refl :: TypeEq a a
     > refl  = TE
     >
     > test  :: a -> TypeEq b1 b2
     > test _ = refl

     GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
     Loading package base ... linking ... done.
     [1 of 1] Compiling DeriveType       ( wacky2.lhs, interpreted )

     wacky2.lhs:9:11:
         Couldn't match expected type `b1' against inferred type `b2'
           `b1' is a rigid type variable bound by
                the type signature for `test' at wacky2.lhs:8:22
           `b2' is a rigid type variable bound by
                the type signature for `test' at wacky2.lhs:8:25
           Expected type: TypeEq b1 b2
           Inferred type: TypeEq b2 b2
         In the expression: refl
         In the definition of `test': test _ = refl
     Failed, modules loaded: none.
     Prelude>


In your version we'd like the fundeps to kick in and say there can be 
only one type paired with 'a' and so we can infer that 'b1' and 'b2' are 
the same, but fundeps are part of type classes and so they too are just 
delayed constraints.[1]

At the time of determining what the principal type of the function is, 
we don't see the type classes or the fundeps associated with them. While 
inferring the principal type we build up a set of delayed constraints 
(i.e. requisite type class instances, based on the functions used). 
After we've determined the principal type, we then verify that we can 
fulfill all the delayed requirements if we assume the type class 
instances in the context actually exist. If we pass type inference and 
context verification, then we deem the function OK.

The main use of fundeps is to assist type inference at *use* sites for 
the function. Say we have a function (foo :: DeriveType a b => a -> b). 
If somewhere we use that function in the expression (foo x), if we've 
already determined that x has type A, this will let us infer some type B 
for specializing the polymorphism of foo in this expression. Without 
fundeps we would have to give a type signature in order to clarify which 
B should be used, if it couldn't otherwise be inferred. But this is all 
fundeps do, they don't help in determining what the type of foo itself 
is when we're defining it.

There are some cute tricks that can be played with fundeps in order to 
do type arithmetic and such, but Haskell doesn't really have dependent 
types and so it doesn't really use contexts to drive inference either. 
Sadly fundeps aren't quite as well integrated or general as they could 
be, but trying to resolve the MPTC/fundep/type families/... stuff into a 
single coherent approach is part of what the haskell' committee is 
trying to work out. One of the tricks in all this is to figure out how 
to have enough of dependent typing to do what we want, but without 
sacrificing decidability(/verifiability) of type inference.



[1] Also, Haskell has only one way of representing that two types are 
identical, namely unification i.e. using the same type variable. So even 
if fundeps did drive type inference, that type signature would still be 
wrong because the principal type is (DeriveType a b => a -> TypeEq b b) 
since it's guaranteed that DeriveType a is defined at only one 'b'.

-- 
Live well,
~wren