John Hughes wrote:
That means that the Monad class is not allowed to declare
return :: a -> m a
because there's no guarantee that the type m a would be well-formed. The type declared for return has to become
return :: wft (m a) => a -> m a
I'm confused. It seems like the type (a -> m a) can't be permitted in any context, because it would make the type system unsound. If so, there's no reason to require the constraint (wft (m a)) to be explicit in the type signature, since you can infer its existence from the body of the type (or the fields of a datatype declaration). Correct, a -> m a can't be permitted anywhere. You're suggesting that wft (m a) be implicit therefore. The trouble is that ALL such contraints can't be implicit... there's an example in the paper showing a case where a constraint is needed on the type of a function to make its BODY well typed, but that constraint can't be inferred from the type alone. With your suggestion then, the programmer would need to write some, but not all, of the wft constraints. My suggestion was, in that case, that it's simpler and more consistent to write all. It's a design decision which could be made either way, of course, but writing all of them is my preference. Okay, simplify, simplify. How about the following: For every datatype in the program, imagine that there's a class declaration with the same name .... singleton :: a -> Set a becomes (internally) singleton :: (Set a) => a -> Set a and fmapM :: (Functor f, Monad m) => (a -> m b) -> f a -> m (f b) becomes fmapM :: (Functor f, Monad m, m b, f a, m (f b), f b) => (a -> m b) -> f a -> m (f b) ... Now you do type inference as normal, dealing with constraints of the form (tvar type+) pretty much like any other constraint. Does that correctly handle every case? I think this is the same as what I suggest, except that where I write wft (Set a), you write Set a and overload Set as both a type and a class. Again, that's a possible design decision one could take, but doesn't really simplify anything except perhaps the notation. John