<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
<title></title>
</head>
<body bgcolor="#ffffff" text="#000000">
<blockquote>
<pre wrap="">John Hughes wrote:
</pre>
<blockquote type="cite">
<pre wrap=""><span class="moz-txt-citetags">> </span>That means that the Monad class is not allowed to declare
<span class="moz-txt-citetags">> </span>
<span class="moz-txt-citetags">> </span> return :: a -> m a
<span class="moz-txt-citetags">> </span>
<span class="moz-txt-citetags">> </span>because there's no guarantee that the type m a would be well-formed. The
<span class="moz-txt-citetags">> </span>type declared for return has to become
<span class="moz-txt-citetags">> </span>
<span class="moz-txt-citetags">> </span> return :: wft (m a) => a -> m a
</pre>
</blockquote>
<br>
I'm confused. It seems like the type (a -> m a) can't be permitted
in any <br>
context, because it would make the type system unsound. If so, there's
no <br>
reason to require the constraint (wft (m a)) to be explicit in the type
<br>
signature, since you can infer its existence from the body of the type
(or <br>
the fields of a datatype declaration).<br>
<br>
</blockquote>
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.<br>
<blockquote><br>
Okay, simplify, simplify. How about the following:<br>
<br>
For every datatype in the program, imagine that there's a class
declaration <br>
with the same name<br>
<br>
....<br>
<br>
singleton :: a -> Set a<br>
<br>
becomes (internally)<br>
<br>
singleton :: (Set a) => a -> Set a<br>
<br>
and<br>
<br>
fmapM :: (Functor f, Monad m) => (a -> m b) -> f a -> m (f
b)<br>
<br>
becomes<br>
<br>
fmapM :: (Functor f, Monad m, m b, f a, m (f b), f b) =><br>
(a -> m b) -> f a -> m (f b)<br>
<br>
...<br>
<br>
Now you do type inference as normal, dealing with constraints of the
form <br>
(tvar type+) pretty much like any other constraint.<br>
<br>
Does that correctly handle every case?<br>
</blockquote>
<pre wrap=""><!---->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
</pre>
</body>
</html>