Please excuse my rather muddled remarks about generalising
type-constructor classes in my last message.
What led to them was the following:
Suppose you want a type-constructor Group, so that (Group a)
is the free group on generators tagged by values of type a. For
example
>data Group a = Word [Generator a]
>type Generator a = Positive a | Negative a
so that Negative a is to be the inverse of a generator Positive a.
To define group multiplication generically, a will have to belong
to some class, so that cancellation of elements with their inverses
can be done. For example, with the implementation above, you could have
> groupMul :: Eq a => BinOp (Group a)
> type BinOp a = a -> a -> a
> groupMul (Word xs) (Word ys) = Word (reduce (xs++ys))
> where reduce ..........
The reduce function has to have a qualified type because (Positive a)
cannot be cancelled against (Negative a') unless you know that a==a'.
Mathematically, Group is an archetypal example of a monad.
One would like to make Group an instance of Monad, with
> instance Monad Group where
> result a = Word [Positive a]
> ...............
but for bind or join you are stuck, because they have to have the
qualified types
bind :: Eq b => Group a -> (a -> Group b) -> Group b
join :: Eq a => Group (Group a) -> Group a
There is no way that
> instance Eq a => Monad Group where ...
makes sense, because the variable a does not appear in (Monad Group).
This suggests that it would be useful to be able to say something like
> class Eq_Monad f where
> result :: a -> f a
> bind :: Eq b => f a -> (a -> f b) -> f b
> join :: Eq a => f (f a) -> f a
> ...........
Is there any reason why qualified types should not appear as the
declared types of instance variables in class declarations? Polymorphic
type expressions are really universally quantified at the top level.
Qualifying contexts may be thought of as cutting down the domain over
which quantification takes place. Higher kind type constructors can
be thought of as lambda-abstractions of types. What I am asking for
are qualified lambda-abstractions of types.
-- Gavin Wraith
-- Gavin Wraith
