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).
Okay, simplify, simplify. How about the following:
For every datatype in the program, imagine that there's a class declaration
with the same name. In the case of
data Maybe a = ...
it's
class Maybe a where {}
In the case of
data Ord a => Map a b = ...
it's
class Ord a => Map a b where {}
It's illegal to refer to these classes in the source code; they're only for
internal bookkeeping.
Now, for every type signature in the program (counting the "type signatures"
of data constructors, though they have a different syntax), for every type
application within the type of the form ((tcon|tvar) type+), add a
corresponding constraint to the type context. E.g.
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)
You also have to do this for the contexts of type constructors, I guess,
e.g. data Foo a = Foo (a Int) becomes data (a Int) => Foo a = Foo (a Int).
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?
-- Ben
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
