From: John Meacham
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
