Specializing a function for distinctly typed parameters

Question

I'd like to write a function bar :: Foo a -> Foo b -> Foo c, such that if a and b is the same type, then c is of that type, otherwise it is (). I suspect that functional dependencies would help me, but I'm not sure how. I write

class Bar a b c | a b -> c where
  bar :: Foo a -> Foo b -> Foo c 

instance Bar x x x where
  bar (Foo a) (Foo b) = Foo a

instance Bar x y () where
  bar _ _ = Foo ()

but obviously, bar (Foo 'a') (Foo 'b') satisfies both instances. How would I declare an instance for two distinct types x /= y only?

Answer 1

You're almost there. You can do this pretty easily with OverlappingInstances and UndecidableInstances. Since this is probably intended as a closed world sort of class, undecidable instances are probably no big deal for you:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances
 , OverlappingInstances, TypeFamilies, UndecidableInstances #-}

data Foo a = Foo a deriving Show

class Bar a b c | a b -> c where
  bar :: Foo a -> Foo b -> Foo c 

instance Bar x x x where
  bar (Foo a) (Foo b) = Foo a

instance (u ~ ())=> Bar x y u where
  bar _ _ = Foo ()

Notice the last instance: if we put () in the instance head it becomes more specific than the other instance and would get matched first, so we instead use the type equality assertion from TypeFamilies (~). I learned this from Oleg.

Notice how this behaves:

*Main> bar (Foo 'a') (Foo 'b')
Foo 'a'
*Main> bar (Foo 'a') (Foo True)
Foo ()
*Main> bar (Foo 'a') (Foo 1)

<interactive>:16:1:
    Overlapping instances for Bar Char b0 c0
      arising from a use of `bar'
    Matching instances:
      instance [overlap ok] u ~ () => Bar x y u
        -- Defined at foo.hs:13:10
      instance [overlap ok] Bar x x x -- Defined at foo.hs:9:10
    (The choice depends on the instantiation of `b0, c0'
     To pick the first instance above, use -XIncoherentInstances
     when compiling the other instance declarations)
    In the expression: bar (Foo 'a') (Foo 1)
    In an equation for `it': it = bar (Foo 'a') (Foo 1)

<interactive>:16:20:
    No instance for (Num b0) arising from the literal `1'
    The type variable `b0' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Note: there are several potential instances:
      instance Num Double -- Defined in `GHC.Float'
      instance Num Float -- Defined in `GHC.Float'
      instance Integral a => Num (GHC.Real.Ratio a)
        -- Defined in `GHC.Real'
      ...plus three others
    In the first argument of `Foo', namely `1'
    In the second argument of `bar', namely `(Foo 1)'
    In the expression: bar (Foo 'a') (Foo 1)

Also in GHC 7.8 you'll have access to closed type families which I think (and hope, as it's relevant to my interests) will be able to handle this in a more palatable way, but the details get a bit confusing