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. ----------------------------------------------------------------------------