How do I write the type of 'inverse'?

[John Hughes]

	I'll try explaining via example:
	I am trying to define a `Pairable' class, which is an abstraction
	of all kinds of pairs:  (a,b),   Pair a b,  etc.

	> class Ord p => Pairable p where
	>     is_pair      :: p -> Bool
	>     pair_fst     :: Ord a => p -> a    -- Precondition: is_pair
	>     pair_snd     :: Ord b => p -> b    -- Precondition: is_pair
	>     make_pair    :: (Ord a, Ord b) => a -> b -> p

	> instance (Ord a, Ord b) => Pairable (a,b) where
	>     is_pair  (a,b) = True
	>     pair_fst (a,b) = a
	>     pair_snd (a,b) = b
	>     make_pair a b  = (a,b)

Funny: I get an error from just this instance declaration! The problem is that
the class definition means that pair_fst is *polymorphic* in a, that is, it
should be able to return *any* type in class Ord. Of course, your instance
can't: it can only return the type of the first component. Thus the instance
is not general enough.

The solution (using hugs -98 or ghc -fglasgow-exts, because this is an
extension to Haskell 98) is to use a multi-parameter class:

	> class (Ord p, Ord a, Ord b) => Pairable p a b where
	>     is_pair      :: p -> Bool
	>     pair_fst     :: p -> a    -- Precondition: is_pair
	>     pair_snd     :: p -> b    -- Precondition: is_pair
	>     make_pair    :: a -> b -> p

	> instance Pairable (a,b) a b where
	>     is_pair  (a,b) = True
	>     pair_fst (a,b) = a
	>     pair_snd (a,b) = b
	>     make_pair a b  = (a,b)

This is what you were after here:

	It seems like I want to pass the component types into the
	class definition somehow:   class Pairable (p a b)

Now the instances of pair_fst and pair_snd are for a *particular* component
type, and all is fine.

This works, but tends to lead to many ambiguities, since the type-checker
cannot know that there isn't an instance

       instance Pairable (a,b) b a where
         ...
	 pair_fst (a,b) = b
	 ...

also. That means it cannot infer, when it sees pair_fst (a,b), that the result
is of the same type as a.

You can avoid the ambiguities too, by adding a *functional dependency* to the
class definition. In this case, the type of the "pair" presumably determines
the type of each component, so you could write

	> class (Ord p, Ord a, Ord b) => Pairable p a b | p->a, p->b where
	>     is_pair      :: p -> Bool
	>     pair_fst     :: p -> a    -- Precondition: is_pair
	>     pair_snd     :: p -> b    -- Precondition: is_pair
	>     make_pair    :: a -> b -> p

to declare that for each type p, there can only be one type a and one type
b. This permits the type-checker to infer the result type of pair_fst and
pair_snd from the argument type.

Of course, if you actually *want* to declare pairs with reversed components as
"pair-like" also, then you can't do this: you have to put up with the
ambiguities (and add types by hand to resolve them) because the ambiguities
are really there.

John