<div class="gmail_quote">On Thu, Jan 1, 2009 at 12:25 PM, Brian Hurt <span dir="ltr"><<a href="mailto:bhurt@spnz.org">bhurt@spnz.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br>
First off, let me apologize for this ongoing series of stupid newbie questions. Haskell just recently went from that theoretically interesting language I really need to learn some day to a language I actually kinda understand and can write real code in (thanks to Real World Haskell). Of course, this gives rise to a whole bunch of "wait- why is it this way?" sort of questions.<br>
<br>
So today's question is: why isn't there a Strict monad? Something like:<br>
<br>
data Strict a = X a<br>
<br>
instance Monad Strict where<br>
( >>= ) (X m) f = let x = f m in x `seq` (X x)<br>
return a = a `seq` (X a)</blockquote><div><br></div><div>First, the error is: f :: a -> Strict b, so you have to unpack the result first.</div><div><br></div><div> <span class="Apple-style-span" style="font-family: 'courier new', monospace;">X m >>= f = let X x = f m in x `seq` X x</span></div>
<div><br></div><div>Now I would like to take a moment to point out something that is a cause of much fuzziness and confusion when talking about strictness. (1) "f is strict" means <span class="Apple-style-span" style="font-style: italic;">exactly </span>f _|_ = _|_. (2) "x `seq` y" means _|_ when x is _|_, y otherwise. These are precise, mathematical definitions. Use them instead of your intuition to start with, until you fix your intuition.</div>
<div><br></div><div>Now consider the right neutral monad law:<br></div><div><br></div><div><span class="Apple-style-span" style="font-family: 'courier new', monospace;"> m >>= return = m</span></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"><br>
</span></div><div><span class="Apple-style-span" style="font-size: 12px; "><span class="Apple-style-span" style="font-family: arial, helvetica, sans-serif;">This fails when m = X _|_:</span></span></div><div><span class="Apple-style-span" style="font-size: 12px;"><br>
</span></div><div><span class="Apple-style-span" style="font-size: 12px;"> <span class="Apple-style-span" style="font-family: 'courier new';">X _|_ >>= return = </span></span></div><div><span class="Apple-style-span" style="font-size: 12px;"><span class="Apple-style-span" style="font-family: 'courier new';">let X x = return _|_ in x `seq` X x =</span></span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;">let X x = _|_ `seq` X _|_ in x `seq` X x =</span></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;">let X x = _|_ in x `seq` X x = _|_</span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px; "><span class="Apple-style-span" style="font-family: arial, helvetica, sans-serif;">Because X _|_ is not _|_.</span></span></div>
<div><span class="Apple-style-span" style="font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px;">The problem here was that return was too strict; i.e. return _|_ was _|_ instead of X _|_. So let's relax return to "return = X", and then see how it goes:</span></div>
<div><span class="Apple-style-span" style="font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px;"><span class="Apple-style-span" style="font-size: 13px; "><div><span class="Apple-style-span" style="font-size: 12px; "> <span class="Apple-style-span" style="font-family: 'courier new'; ">X _|_ >>= return = </span></span></div>
<div><span class="Apple-style-span" style="font-size: 12px; "><span class="Apple-style-span" style="font-family: 'courier new'; ">let X x = return _|_ in x `seq` X x =</span></span></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px; ">let X x = X _|_ in x `seq` X x =</span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px; ">_|_ `seq` X _|_ = _|_</span></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"><br>
</span></div><div><span class="Apple-style-span" style="font-size: 12px; "><span class="Apple-style-span" style="font-family: arial, helvetica, sans-serif;">Whoops! It happened again. So we're forced to relax the definition of bind also. And then the monad isn't strict as we were attempting. Maybe the problem is somewhere else: that X _|_ and _|_ are different; let's fix that by making Strict a newtype:</span></span></div>
<div><span class="Apple-style-span" style="font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px;"><span class="Apple-style-span" style="font-family: 'courier new', monospace;">newtype Strict a = X a</span></span></div>
<div><br></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;">instance Monad Strict where</span></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"> X m >>= f = let X x = f m in x `seq` X x</span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"> return x = x `seq` X x</span></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"><br>
</span></div><div><span class="Apple-style-span" style="font-size: 12px; "><span class="Apple-style-span" style="font-family: arial, helvetica, sans-serif;">Okay, first let's prove a little lemma to show the absurdity of this definition :-) :</span></span></div>
<div><span class="Apple-style-span" style="font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px;"><span class="Apple-style-span" style="font-family: 'courier new', monospace;">Let f x = x `seq` X x, then f = X.</span></span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px;">Let's consider two cases: </span></div><div>
<span class="Apple-style-span" style="font-size: 12px;">(1) x is not _|_: then f x = x `seq` X x. But the definition of seq is that seq x y is _|_ when x is _|_, and y otherwise. So in this case f x = X x.</span></div><div>
<span class="Apple-style-span" style="font-size: 12px;">(2) x is _|_: then f _|_ = _|_ `seq` X _|_ = _|_. But X _|_ = _|_ because of the semantics of newtypes, so f x = X x here also.</span></div><div><span class="Apple-style-span" style="font-size: 12px;">Qed.</span></div>
<div><span class="Apple-style-span" style="font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px;">So now we know we can replace x `seq` X x with simply X x without changing semantics:</span></div>
<div><span class="Apple-style-span" style="font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px;"><span class="Apple-style-span" style="font-size: 13px; "><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px; ">instance Monad Strict where</span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px; "> X m >>= f = let X x = f m in X x</span></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px; "> return x = X x</span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px; "><span class="Apple-style-span" style="font-family: arial, helvetica, sans-serif;">And performing some obvious rewrites:</span></span></div>
<div><span class="Apple-style-span" style="font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px;"><span class="Apple-style-span" style="font-size: 13px; "><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px; ">instance Monad Strict where</span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px; "> X m >>= f = f m</span></div><div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px; "> return = X</span></div>
<div><span class="Apple-style-span" style="font-family: 'courier new'; font-size: 12px;"><br></span></div><div><span class="Apple-style-span" style="font-size: 12px; "><span class="Apple-style-span" style="font-family: arial, helvetica, sans-serif;">And there you have your Strict monad. Oh, but it's the same as Identity. :-)</span></span></div>
<div><span class="Apple-style-span" style="font-size: 12px;"><br></span></div><div>So that's the answer: there already is a Strict monad. And an attempt to make a lazier one strict just results in breaking the monad laws.</div>
<div><br></div><div>There's another answer though, regarding your question for why we don't just use StrictT State instead of a separate State.Strict. This message is already too long, and I suspect this will be the popular reply anyway, but the short answer is that Strict State is called that because it is strict in its <span class="Apple-style-span" style="font-style: italic;">state</span>, not in its value. StrictT wouldn't be able to see that there even is a state, so it wouldn't be able to change semantics. And as we saw, an attempt to be overly strict in your value just results in law breaking.</div>
<div><br></div><div>Luke</div></span></span></div></span></span></div></span></span></div></div>