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

oleg at pobox.com oleg at pobox.com
Thu Apr 13 22:56:17 EDT 2006

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

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