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