Functional dependencies and Constructor Classes

[Martin Sulzmann]

Hi,

I was wondering whether other people made similiar observations.
Functional dependencies seem to be expressiveness enough to encode
some of the kinding rules required for Constructor Classes.

Take a look at the Haskell code below
(runs under hugs -98 or  ghci -fglasgow-exts-fallow-undecidable-instances)

Martin



-- An alternative to constructor classes

module Fmap where

{- Instead of
class Functor f where fmap :: (a->b)->(f a->f b)

use
-}

class Fmap a b fa fb | a fb -> b fa, 
                       b fa -> a fb,
                       fa fb -> a b 
    where fmap2 :: (a->b)->(fa -> fb)

{- We require:

(1) fmap2 transforms a function into another function,
    i.e. fmap2's type should always be of shape (a->b)->(fa->fb)

(2) b, fa uniquely determine a and fb

(3) a, fb   "                b and fa

(4) fa, fb  "                a and b

Note that (1) is enforced by the class definition. (2)-(4) are enforced by FDs.

My guess/conjecture is that the above axiomatization of functors is equivalent to the
one found in Haskell98.
-}

-- some Examples

{- The following is a variation of an example taken from Mark Jones original paper 
"A System of Constructor Classes: Overloading and Implicit Higher-Order Polymorphism".
He used this example to motivate the introduction of constructor classes. The example
is type correct using the alternative formulation of functors.
-}

cmap :: (Fmap a b fb1 fb, Fmap a1 b1 fa fb1) =>
         (a1 -> b1) -> (a -> b) -> fa -> fb
cmap f g = (fmap2 g) . (fmap2 f)


-- identity functor
instance Fmap a a a a where fmap2 h = h

-- functor composition 
-- Instance is not allowed, cause leads to undecidable type inference

{-
instance (Fmap a b c d, Fmap e f a b) => Fmap e f c d
   where fmap2 h = fmap2 (fmap2 h)
-}

comp :: (Fmap fa1 fb1 fa fb, Fmap a b fa1 fb1) =>
         (a -> b) -> fa -> fb
comp h = fmap2 (fmap2 h)