| > > 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
| Huh?? Methods with a context are perectly fine in Haskell.
I think I can explain the confusion here; version 2.28b of Gofer
doesn't allow qualifiers in the types of member functions But Haskell
does, and so does the next release of Gofer.
However, in my opinion, the class declaration above is not the solution
to the problem at hand. I've been playing with similar examples for some
time and come up with a few ideas for dealing with it.
There are two parts to this. First, we we really do want the original
class declaration for Monad without qualified types for member
functions:
class Monad m where result :: a -> m a
bind :: m a -> (a -> m b) -> m b
Restricting the type of bind to require, for example, an equality on
elements of type a is a bad idea because:
- in many cases, it's unnecessary (eg. List, Maybe, State, ...),
- in some cases, it's not good enough (eg. Monad Set where Set is
implemented using an ordered search tree, requiring Ord a).
Second, we need to be able to add the qualifying restrictions on a
per-constructor basis. My favoured way to do this is to reuse a
current piece of Haskell syntax with a new semantics. For example, if
I write a type declaration of the form:
data Ord a => Set a = ...
then I would expect the Set constructor to be treated as having kind
Ord a => a -> *. (This last kind is essentially what Gavin suggested
in an earlier message except that kind variables are necessary.) Now,
when you instantiate a fully polymorphic type like that for bind with
the Set constructor, you get the qualified type:
bind :: (Ord a, Ord b) => Set a -> (a -> Set b) -> Set b
and you are free to use functions from the Ord class in the definition
of bind on sets.
Seems simple? Actually, there are some nasty complications. First of
all, it requires polymorphic kinds, rather than the monomorphic kinds
in my current system. This is feasible, but it's not yet clear to me
what additional costs this would impose on the type checker or on the
user who has to work out why a type/kind error occurred. Secondly,
there are some curious interactions between the type and kind system,
for example, moving a qualifier from a kind into a type, that are quite
difficult to deal with in the general case.
For what it's worth, if you think adding qualifiers to types would be
useful, I've also been considering simple implicit subkinding
constraints for other applications. However, I strongly believe that a
type system in a practical language should be intuitive, and I'm
concerned that, even if these extensions work well on paper, they may
be too complicated for practical use. The way to test this is to
develop experimental implementations, coupled with the development of
the theory, and see how they go ...
All the best,
Mark
