Getting rid of functional dependencies with type proxies

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

On Thu, Nov 13, 2008 at 9:09 PM, Tobias Bexelius
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@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
participants (2)
-
Reiner Pope
-
Tobias Bexelius