Creighton Hogg posed the following problem. Given a rather straightforward matrix multiplication code
-- The elements and the size data Vec a = Vec (Array Int a) Int deriving (Show,Eq) type Matrix a = (Vec (Vec a)) class MatrixProduct a b c | a b -> c where (<*>) :: a -> b -> c instance (Num a) => MatrixProduct a (Vec a) (Vec a) where (<*>) num (Vec a s) = Vec (fmap (*num) a) s vector n elms = Vec (array (0,n-1) $ zip [0..n-1] elms) n
we'd like to get the following straightforward test to compile:
test = 10 <*> (vector 10 [0..9])
The trouble it doesn't: the function (<*>) has the type a->b->c so the type of the scalar doesn't have to be in any a priori relation with the type of the matrix (to permit efficient representations for particular sorts of matrices). Such a general type for (<*>) means that the test expression does not constrain "10" to be of the same numeric type as the type of matrix elements. So, the inferred type for test is test :: (Num a, Num b, MatrixProduct a (Vec b) c) => c The constraint must be resolved (top level, monomorphism restriction): but it can't because there is no instance MatrixProduct a (Vec b) c There is only more specialized instance, which doesn't match. The solution exists: change test so that the type of the scalar and the base type of the vector are the same:
test1 = (10::Int) <*> (vector 10 [0..9::Int]) test2 = let n = 10 in n <*> (vector 10 [0..(9 `asTypeOf` n)])
or add the type annotations in other ways. But that is annoying. Creighton Hogg asked if there is another way? There is. Change the instances to
instance (Num a,Num b,TypeCast a b) => MatrixProduct a (Vec b) (Vec b) where (<*>) num (Vec a s) = Vec (fmap (* (typeCast num)) a) s
The difference is subtle but important: given such a general instance, trying to resolve "MatrixProduct a (Vec b) c" now succeeds. Instance selection is done only based on the types in the head; constraints are not taken into account. When the match succeeds, GHC commits to it and goes checking the constraints. One of the constraints, TypeCast a b, says that the type a must be the same as b. Because 'a' and 'b' were just type variables (could be instantiated), that constraint succeeds and we accomplished our task. Now the original test types and works. In short: given the instance "C a a" and the constraint "C a b", we see failure: "C a a" can't match "C a b". The type variables of the latter aren't instantiated: this is matching, not the full unification. The re-written instance "TypeCast a b => C a b", effectively describes the same set of types. Now, however, "C a b" matches that instance -- and, the TypeCast constraint forces "a" and "b" to be the same. These _local_, per-instance functional dependencies notably improve the power of instance selection: from mere matching to some type improvement (towards the full unification). The net result is fewer type annotations required from the user. One might consider that useful. The full code: {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} module Foo where import Array data Vec a = Vec (Array Int a) Int deriving (Show,Eq) type Matrix a = (Vec (Vec a)) class MatrixProduct a b c | a b -> c where (<*>) :: a -> b -> c {- previously: instance (Num a) => MatrixProduct a (Vec a) (Vec a) where (<*>) num (Vec a s) = Vec (fmap (*num) a) s -} instance (Num a,Num b,TypeCast a b) => MatrixProduct a (Vec b) (Vec b) where (<*>) num (Vec a s) = Vec (fmap (* (typeCast num)) a) s vector n elms = Vec (array (0,n-1) $ zip [0..n-1] elms) n test = 10 <*> (vector 10 [0..9]) test1 = (10::Int) <*> (vector 10 [0..9::Int]) test2 = let n = 10 in n <*> (vector 10 [0..(9 `asTypeOf` n)]) class TypeCast a b | a -> b, b->a where typeCast :: a -> b class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x