Restricted Data Types

[Ben Rudiak-Gould]

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