[Haskell-cafe] Stupid question #852: Strict monad
Brian Hurt
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)
(although this code doesn't compile for reasons I'm not clear on- I keep
getting:
temp.hs:4:0:
Occurs check: cannot construct the infinite type: b = Strict b
When trying to generalise the type inferred for `>>='
Signature type: forall a b1.
Strict a -> (a -> Strict b1) -> Strict b1
Type to generalise: forall a b1.
Strict a -> (a -> Strict b1) -> Strict b1
In the instance declaration for `Monad Strict'
as a type error. Feel free to jump in and tell me what I'm doing wrong.)
Obviously, there would also be a StrictT monad transformer. The point
here is that there are some monads (State being the obvious one) that come
in both strict and lazy variants- the two variants could be eliminated,
and the strict variant would just become a StrictT (State x) a. Or
maybe a StateT x Strict a.
Hmm. Which raises the interesting question of what, if any, semantic
difference there is between a StrictT (State x) a and a StateT x Strict
a.
In any case, the idea came when I was thinking about monads being "code
regions"- that we can talk about such and such a function being "in" the
IO monad or STM monad. The idea was that one could define a "strict" code
region you could put code in.
Brian
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Stephan Friedrichs
Brian Hurt wrote:
>
> [...]
>
> 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)
unless I am mistaken, this violates the first monad law (see Prelude
documentation)
return a >>= k == k a
for k = const (return 3) and a = undefined, because
return undefined >>= _ === _|_
but
const (return 3) undefined === return 3
Generally speaking, the first monad law only holds for strict functions
in your monad.
>
> [...]
>
Happy new year,
Stephan
--
Früher hieß es ja: Ich denke, also bin ich.
Heute weiß man: Es geht auch so.
- Dieter Nuhr
Luke Palmer
>
> 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
Jonathan Cast
> 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
(Note that you can eliminate the `seq`s below by saying
data Strict a = X !a
instead, or, if X is going to be strict,
newtype 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)
>
> (although this code doesn't compile for reasons I'm not clear on- I keep
> getting:
> temp.hs:4:0:
> Occurs check: cannot construct the infinite type: b = Strict b
> When trying to generalise the type inferred for `>>='
> Signature type: forall a b1.
> Strict a -> (a -> Strict b1) -> Strict b1
> Type to generalise: forall a b1.
> Strict a -> (a -> Strict b1) -> Strict b1
> In the instance declaration for `Monad Strict'
> as a type error. Feel free to jump in and tell me what I'm doing
> wrong.)
Since you asked,
The simplest fix (that makes the code you posted compile) is to pattern
match on the result of f (to do what you want):
(>>=) (X m) f = let X x = f m in x `seq` X x
(I would write
X m >>= f = let X x = f m in X $! x)
But unless you export the X constructor (and don't make it strict), then
f should never return (X undefined), so the above is equivalent, for all
f in practice, to
X m >>= f = f m
I think what you really want to say is
newtype Strict alpha = X alpha
instance Monad Strict where
return = X
X x >>= f = f $! x
jcc
David Menendez
>
> 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 is at least one transformer that will make a strict monad out of
a non-strict monad.
newtype CPS m a = CPS { unCPS :: forall b. (a -> m b) -> m b }
instance Monad (CPS m) where
return x = CPS (\k -> k x)
m >>= f = CPS (\k -> unCPS m (\a -> unCPS (f a) k))
toCPS :: Monad m => m a -> CPS m a
toCPS m = CPS (\k -> m >>= k)
fromCPS :: Monad m => CPS m a -> m a
fromCPS m = unCPS m return
Contrast:
> runIdentity $ undefined >>= \_ -> return ()
()
> runIdentity . fromCPS $ undefined >>= \_ -> return ()
*** Exception: Prelude.undefined
> 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.
No, Control.Monad.State.Strict and Control.Monad.State.Lazy never
force evaluation of their states.
Control.Monad.State.Strict> evalState (put undefined) '0'
()
The difference is in the strictness of (>>=).
The same is true of the other Strict/Lazy pairs.
--
Dave Menendez <da...@zednenem.com>
<http://www.eyrie.org/~zednenem/>
Luke Palmer
> 2009/1/1 Luke Palmer <lrpa...@gmail.com>:
> >
> > 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 is at least one transformer that will make a strict monad out of
> a non-strict monad.
>
> newtype CPS m a = CPS { unCPS :: forall b. (a -> m b) -> m b }
I have heard this called the "codensity monad" (and it appears under that
name in category-extras). Good observation.
In my reply I missed the important consideration of the strictness of (>>=),
irrsepective of the values. While you can not force values to be strict in
a monad without breaking a law, (>>=) is "up for grabs", and that's what
people are referring to when they refer to strict and lazy monads.
So I guess "strict monad" means (>>= f) is strict for all f. Right?
Luke
> > 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.
>
> No, Control.Monad.State.Strict and Control.Monad.State.Lazy never
> force evaluation of their states.
>
> Control.Monad.State.Strict> evalState (put undefined) '0'
> ()
My mistake.
Luke
David Menendez
> On Thu, Jan 1, 2009 at 1:31 PM, David Menendez <da...@zednenem.com> wrote:
>>
>> newtype CPS m a = CPS { unCPS :: forall b. (a -> m b) -> m b }
>
> I have heard this called the "codensity monad" (and it appears under that
> name in category-extras). Good observation.
Interesting. I hadn't heard that name for it before.
In my own monad library, I called it CPS, since it transforms a monad
into continuation-passing style. It's handy for monads with an
expensive (>>=), as discussed in Janis Voigtlander's "Asymptotic
Improvement of Computations over Free Monads".
> In my reply I missed the important consideration of the strictness of (>>=),
> irrsepective of the values. While you can not force values to be strict in
> a monad without breaking a law, (>>=) is "up for grabs", and that's what
> people are referring to when they refer to strict and lazy monads.
>
> So I guess "strict monad" means (>>= f) is strict for all f. Right?
That's my understanding.
As a consequence, strict monads in Haskell also have the property that
"return undefined" never equals "undefined". Otherwise, they wouldn't
satisfy the monad laws.
>> No, Control.Monad.State.Strict and Control.Monad.State.Lazy never
>> force evaluation of their states.
>>
>> Control.Monad.State.Strict> evalState (put undefined) '0'
>> ()
>
> My mistake.
I made that mistake myself, once. It doesn't help that the
documentation just says "Lazy state monads" and "Strict state monads"
without any further explanation.
Jonathan Cast
> On Thu, Jan 1, 2009 at 1:31 PM, David Menendez <da...@zednenem.com>
> wrote:
> 2009/1/1 Luke Palmer <lrpa...@gmail.com>:
> >
> > 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 is at least one transformer that will make a strict
> monad out of
> a non-strict monad.
>
> newtype CPS m a = CPS { unCPS :: forall b. (a -> m b) -> m b }
>
> I have heard this called the "codensity monad" (and it appears under
> that name in category-extras). Good observation.
>
> In my reply I missed the important consideration of the strictness of
> (>>=), irrsepective of the values. While you can not force values to
> be strict in a monad without breaking a law, (>>=) is "up for grabs",
Is it? By the second monad law, (>>= return) is required to be strict.
return must not be strict, as observed above. Are there monads which
satisfy both laws, but have undefined >>= f /= undefined, for some f? I
suspect (although I don't seem to have the source on my computer atm)
that Control.Monad.State.{Lazy,Strict} both cheat on the second monad
law anyway, though...
jcc
Luke Palmer
> On Thu, 2009-01-01 at 13:44 -0700, Luke Palmer wrote:
> > On Thu, Jan 1, 2009 at 1:31 PM, David Menendez <da...@zednenem.com>
> > wrote:
> > 2009/1/1 Luke Palmer <lrpa...@gmail.com>:
> > >
> > > 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 is at least one transformer that will make a strict
> > monad out of
> > a non-strict monad.
> >
> > newtype CPS m a = CPS { unCPS :: forall b. (a -> m b) -> m b }
> >
> > I have heard this called the "codensity monad" (and it appears under
> > that name in category-extras). Good observation.
> >
> > In my reply I missed the important consideration of the strictness of
> > (>>=), irrsepective of the values. While you can not force values to
> > be strict in a monad without breaking a law, (>>=) is "up for grabs",
>
> Is it? By the second monad law, (>>= return) is required to be strict.
> return must not be strict, as observed above. Are there monads which
> satisfy both laws, but have undefined >>= f /= undefined, for some f? I
> suspect (although I don't seem to have the source on my computer atm)
> that Control.Monad.State.{Lazy,Strict} both cheat on the second monad
> law anyway, though...
ghci> import Control.Monad.Writer
ghci> head . getDual . execWriter $ undefined >> tell (Dual [42])
42
Luke
David Menendez
> On Thu, 2009-01-01 at 13:44 -0700, Luke Palmer wrote:
>>
>> In my reply I missed the important consideration of the strictness of
>> (>>=), irrsepective of the values. While you can not force values to
>> be strict in a monad without breaking a law, (>>=) is "up for grabs",
>
> Is it? By the second monad law, (>>= return) is required to be strict.
> return must not be strict, as observed above. Are there monads which
> satisfy both laws, but have undefined >>= f /= undefined, for some f? I
> suspect (although I don't seem to have the source on my computer atm)
> that Control.Monad.State.{Lazy,Strict} both cheat on the second monad
> law anyway, though...
How about the Identity monad?
ghci> (return undefined :: Identity Char) `seq` ()
*** Exception: Prelude.undefined
ghci> runIdentity $ undefined >>= \_ -> return ()
()
"return" is strict and (>>=) is non-strict.
--
Dave Menendez <da...@zednenem.com>
<http://www.eyrie.org/~zednenem/>
Jonathan Cast
> On Thu, Jan 1, 2009 at 4:30 PM, Jonathan Cast <jonath...@fastmail.fm> wrote:
> > On Thu, 2009-01-01 at 13:44 -0700, Luke Palmer wrote:
> >>
> >> In my reply I missed the important consideration of the strictness of
> >> (>>=), irrsepective of the values. While you can not force values to
> >> be strict in a monad without breaking a law, (>>=) is "up for grabs",
> >
> > Is it? By the second monad law, (>>= return) is required to be strict.
> > return must not be strict, as observed above. Are there monads which
> > satisfy both laws, but have undefined >>= f /= undefined, for some f? I
> > suspect (although I don't seem to have the source on my computer atm)
> > that Control.Monad.State.{Lazy,Strict} both cheat on the second monad
> > law anyway, though...
>
> How about the Identity monad?
>
> ghci> (return undefined :: Identity Char) `seq` ()
> *** Exception: Prelude.undefined
> ghci> runIdentity $ undefined >>= \_ -> return ()
> ()
>
> "return" is strict and (>>=) is non-strict.
Sure, that works.
jcc