Restricted Data Types

[John Hughes]

From: John Meacham <john at repetae.net>
Subject: Re: Restricted Data Types

however, what prevents the following from being _infered_

return Foo :: Moand m => m Foo
so, we think we can specialize it to
return Foo :: Set Foo

however, we no longer have the constraint that Foo must be in Eq!

Maybe I wasn't up-front enough about this in the paper: RDTs add a new 
form of constraint in contexts, wft t, meaning that type t is 
well-formed. While base types and type variables can be assumed to be 
well-formed, other types may only be used at all in the context of a 
suitable well-formedness constraint. 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.e. when return is called, it has to be passed a dictionary proving 
that m a is well-formed. In the case of Set, that's an Eq a dictionary.

In your example, the most general type of return Foo is (Monad m, wft (m 
Foo)) => m Foo, and when you instantiate m to Set, you're left with the 
contraint wft (Set Foo), which reduces to Eq Foo.

The changes to the type system are that all typing rules have to add wft 
t constraints to the context, for every type t that appears in them. 
Fortunately most can be immediately discarded, since base types are 
always well-formed, and data type definitions imply constraint reduction 
rules that eliminate wft constraints unless the datatype is restricted. 
For example, wft [a] reduces to wft a, because lists place no 
restriction on their element type. Wft constraints on type *variables* 
can be discarded where the variables are generalised, *provided* the 
instantiation rule only permits variables to be instantiated at 
well-formed types. There's no need to write the type of reverse as wft a 
=> [a] -> [a], if polymorphic type variables can only every be 
instantiated to well formed types. The only wft constraints that cannot 
be discarded are thus those where the type that must be well-formed is 
an application of a type constructor variable, such as wft (m a) in the 
type of return. That suggests that wft constraints ought not to be too 
common in real code, but they do crop up in monadic library code--

  class Monad m where
     return :: wft (m a) => a -> m a
     (>>=) :: (wft (m a), wft (m b)) => m a -> (a -> m b) -> m b

That's why, without some clever optimisation, RDTs will lead to massive 
extra dictionary passing (in implementations that use dictionaries). 
"It'll be just fine as long as you don't use monads" isn't really a good 
enough argument, is it?!

John