[Haskell-cafe] Stupid question #852: Strict monad

[Luke Palmer]

On Thu, Jan 1, 2009 at 12:25 PM, Brian Hurt <bhurt at spnz.org> wrote:

>
> 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.
>
> So today's question is: why isn't there a Strict monad?  Something like:
>
> data Strict a = X a
>
> instance Monad Strict where
>    ( >>= ) (X m) f = let x = f m in x `seq` (X x)
>    return a = a `seq` (X a)


First, the error is:  f :: a -> Strict b, so you have to unpack the result
first.

  X m >>= f = let X x = f m in x `seq` X x

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 exactly 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.

Now consider the right neutral monad law:

 m >>= return = m

This fails when m = X _|_:

 X _|_ >>= return =
let X x = return _|_ in x `seq` X x =
let X x = _|_ `seq` X _|_ in x `seq` X x =
let X x = _|_ in x `seq` X x = _|_

Because X _|_ is not _|_.

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:

 X _|_ >>= return =
let X x = return _|_ in x `seq` X x =
let X x = X _|_ in x `seq` X x =
_|_ `seq` X _|_ = _|_

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:

newtype Strict a = X a

instance Monad Strict where
    X m >>= f = let X x = f m in x `seq` X x
    return x = x `seq` X x

Okay, first let's prove a little lemma to show the absurdity of this
definition :-) :

Let f x = x `seq` X x, then f = X.

Let's consider two cases:
(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.
(2) x is _|_: then f _|_ = _|_ `seq` X _|_ = _|_.  But X _|_ = _|_ because
of the semantics of newtypes, so f x = X x here also.
Qed.

So now we know we can replace x `seq` X x with simply X x without changing
semantics:

instance Monad Strict where
    X m >>= f = let X x = f m in X x
    return x = X x

And performing some obvious rewrites:

instance Monad Strict where
    X m >>= f = f m
    return = X

And there you have your Strict monad.  Oh, but it's the same as Identity.
 :-)

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.

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 state, 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.

Luke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090101/df6cfc0d/attachment.htm