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@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