Hi Zhanyong,
| In Haskell, instances of a type class can only be well-formed type
| constructors ...
| Note there is no type constructor abstraction.
|
| In practice, I found this rule too restrictive.
There are good reasons for the restrictions that were alluded to in
my constructor classes paper, and again in Typing Haskell in Haskell.
Some text from emails written when this topic came up previously is
attached to the end of this message.
Actually, the first part of the attached email deals with a different
problem (making Set an instance of Monad), but since that also came
up for discussion again quite recently, I don't think it will hurt to
include it again here.
| How about extending TC with a branch for abstraction:
|
| TC ::= ...
| | /\a. TC -- abstraction
|
| This is too powerful and will get out of control -- we surely don't want
| to give TC the full power of lambda-calculus. So let's impose a
| restriction: in /\a.TC, a must occur free in TC *exactly once*. This
| way, abstraction can only be used to specify with respect to which
| argument a partial application is. (or I think so -- I haven't tried to
| prove it.)
My instinct (which perhaps somebody will prove incorrect) is that this will
not help. Suppose, for example, that you needed to unify ([a],[b]) with f c
as part of the type inference process. How would you solve this problem?
Alas, there are several different, and incompatible ways:
([a], [b]) = (/\a. ([a],[b])) a
= (/\b. ([a],[b])) b
= (/\c. (c, [b])) [a]
= (/\d. ([a], d)) [b]
= (/\e. e) ([a], [b])
Note that the /\-terms in each of these examples satisfies your restriction.
So I don't think you'll be able to obtain most general unifiers or principal
types with this restriction.
In my opinion, Dale Miller's work on Higher-order patterns (introduced, I think
in about 1991, but I don't have references) would probably be the best starting
point for serious experimentation in this area.
Hope this helps,
Mark
-- From the archives: -------------------------------------------------------
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.
----------------------------------------------------------------------------
