Restricted Data Types

[John Hughes]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org//pipermail/haskell-prime/attachments/20060207/9557cba5/attachment.htm