[Haskell-cafe] Getting rid of functional dependencies with type proxies

[Reiner Pope]

On Thu, Nov 13, 2008 at 9:09 PM, Tobias Bexelius
<tobias.bexelius at avalanchestudios.se> wrote:
> Hi,
>
> some time ago I asked about a problem I had with functional dependencies
> conflicting when using overlapping instances in a code like this:
>
>
> {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances
> -fallow-incoherent-instances #-}
> data V2 a = V2 a a
> class Vec v a where
>        dot :: v a -> v a -> a
> instance Num a => Vec V2 a where
>        V2 a1 a2 `dot` V2 b1 b2 = a1*b1+a2*b2
> class Mult a b c | a b -> c where
>        (*.) :: a -> b -> c
> instance (Num x) => Mult x x x where (*.) = (*)
> instance (Vec a x) => Mult (a x) (a x) x where (*.) = dot
>
> {-
> Functional dependencies conflict between instance declarations:
>      instance [overlap ok] (Num x) => Mult x x x
>      instance [overlap ok] (Vec a x) => Mult (a x) (a x) x
> -}
>
> The problem here is that the dependency check is occuring too soon.
> Removing the dependency would solve the problem, but then you would need
> to put type annotations everywhere you use the multiplication operator,
> and that's not acceptable.
> However, I did found a solution I would like to share with you: Creating
> a "type proxy"! I find it strange that such a simple solution to such a
> (for me at least) common problem hasn't been documented more.
> This is the working code:
>
> {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances
> -fallow-incoherent-instances #-}
> data V2 a = V2 a a
> class Vec v a where
>        dot :: v a -> v a -> a
> instance Num a => Vec V2 a where
>        V2 a1 a2 `dot` V2 b1 b2 = a1*b1+a2*b2
> class Mult a b c | a b -> c where
>        (*.) :: a -> b -> c
> class MultProxy a b c where
>        (*..) :: a -> b -> c
> instance MultProxy a b c => Mult a b c where
>        (*.) = (*..)
> instance (Num x) => MultProxy x x x where (*..) = (*)
> instance (Vec a x) => MultProxy (a x) (a x) x where (*..) = dot
>
>
> Thanks to Emil Axelsson that pointed me to
> http://haskell.org/haskellwiki/GHC/AdvancedOverlap, where similar
> problems where discussed. Again, I haven't found links to this page in
> any of the Haskell tutorials I've read so far.
>
> /Tobias
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

Hi,

I'm not convinced your solution actually preserves the fundeps as you
might expect. What I've taken to "test" the fundeps have been the
following two functions: (of course, we need the following extensions
to have sensible type inference)

> {-# OPTIONS -fglasgow-exts #-}
> {-# LANGUAGE NoMonomorphismRestriction #-}
>
> foo x y = x *. y where
>    _ = x * y

The "_ = x * y" clause ensures that x's type has a Num constraint.
Depending on the setup, different types will be inferred by GHCi for
foo.

Consider your initial code, which didn't working because of
conflicting instances. If you remove the (Vec a x)=>... instance, then
the code compiles. With the fundeps, then foo's type is inferred as

> foo :: Num a => a -> a -> a

However, with your new Proxy-based code, foo's type is inferred as

> foo :: (Num a, MultProxy a a c) => a -> a -> c

so some of the fundep information has been "lost", in some sense.

If you will consider using type equality constraints (which come with
GHC 6.10) then there is another solution which I personally find more
understandable than the fundeps/proxies approach. Write the classes as

> class Mult a b c where
>    (*.) :: a -> b -> c
>
> instance (x ~ y, Num x) => Mult x x y where
>    (*.) = (*)
>
> instance (x ~ y, Vec a x) => Mult (a x) (a x) y where
>    (*.) = dot

(Note that this doesn't require UndecidableInstances.) What's
intuitively going on here is that the equality constraint in the
instances acts similarly to a fundep (in that, if x is determined,
then y is determined), but it's like a fundep /within the instance/.
Thus, there is no "conflicting instances" problem, yet the fundep-like
more-precise inference still works once we've selected an instance.

Note that we do need to select an instance first; this requires
IncoherentInstances, which you had in your code anyway. As long as
IncoherentInstances is enabled, then foo's type is inferred as

> foo :: Num a => a -> a -> a

as required.

As I said, I personally find type equality constraints much easier to
reason about than fundeps, so I like using them for this kind of
problem.

Cheers,
Reiner