Hi Michael,
| "...type synonyms must be fully applied". I think the above
| example is a valid objection to this.
I'll append some text that I wrote on a previous occasion when somebody
asked why type synonyms couldn't be partially applied. I hope that it
will help to explain why the restriction is not easy to lift, however
desirable it might be. The example there was a little different, but
I'm sure that you'll see the correspondence.
| The other example of something that I want to declare as a monad, but
| which I can not is this: Consider a type of collection of some sort that
| requires the types of the elements to be instances of some specific class.
This too is a problem that has come up quite a few times in the past.
As yet, I'm not sure that anyone has a definitive answer for it either,
although the work that John Hughes presented at the Haskell workshop on
Restricted Datatypes is perhaps the closest that anyone has come so far.
A general problem here is that there are differences between conventional
mathematics---where you can have sets of any type---and the mathematics of
programming languages---where interesting set datatypes can only be
constructed on types whose elements have, at least, an equality. In Haskell
terms, mathematics has an equality function of type: forall a. a -> a -> Bool;
the same operator is available to mathematicians who reason about Haskell
programs. But Haskell programmers have to make do with a more restrictive
operator of type forall a. Eq a => a -> a -> Bool. (Which is not actually
an equality operator at all when you look at what's really going on; it's
just a kind of identity function or projection!)
All the best,
Mark
Here's the text I promised:
| I'd like to use monadic code on the following type
| type IOF b a = b -> IO a
| The following seemed reasonable enough:
| instance Monad (IOF b) where ...
| But Hugs and GHC both object ...
The example is rejected because type synonyms can only be used if a
full complement of arguments has been given. There are at least two
kinds of problem that can occur if you relax this restriction, but
both are related to unification/matching.
Suppose that we allow your definition. And suppose that we also allow:
instance Monad ((->) env) where ...
which is a perfectly reasonable thing to do (it's the reader monad).
Now what should we do when faced with the problem of unifying two
type expressions like: m c and b -> IO a ... Haskell unifies these
with the substitution: {m +-> ((->) b), c +-> IO a}, but with your
instance decl, you might have preferred { m +-> IOF b, c +-> a }.
In other words, it's ambiguous, and the choice between these two could
change the semantics because you'll end up picking different instances
depending on which choice you make.
Or consider what you really mean when you write (IOF b) ... my guess
is that you're thinking of it as adding a kind of lambda, so that
IOF b = \a. a -> IO b
This is appealing, but also means that we'd need to move up to higher-order
unification which is undecidable and non-unitary. For example, now
we could match m c to b -> IO a in all kinds of interesting ways:
b -> IO a = (\b . b -> IO a) b
= (\a . b -> IO a) a
= (\z . b -> z) (IO a)
= (\z . b -> IO a) Int
= ...
Now we really have ambiguity problems to worry about!
Requiring type synonyms to be fully applied --- in effect, telling us
that a synonym is nothing more than an abbreviation, and has no other
consequences for the semantics --- seems like a nice way to avoid these
problems.
----------------------------------------------------------------------------
[EMAIL PROTECTED] Pacific Software Research Center, Oregon Graduate Institute
Looking for a PhD or PostDoc? Interested in joining PacSoft? Let us know!
