[Haskell-cafe] Local Fundeps [was: Fundeps: I feel dumb]

[oleg at pobox.com]

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