Why shouldn't I make my monads "value strict"?

#1

An observation by @jaror made me wonder: why shouldn’t I make my monads “value strict”? I don’t know if I can formally define “value strict” but it means something like “when m a has finished evaluating, a is in WHNF[1]”. (That depends on a definition of “finished evaluating”, and I don’t know that there is one in general.) Anyway, here are some examples demonstrating what I mean.

  • For a “value strict” monad, return a is the same as return $! a
  • A “value strict” State s a would be isomorphic to \s -> ValueStrictPair a s, where data ValueStrictPair a s = MkValueStrictPair !a s
  • A “value strict” Either a would be data RightStrictEither e a = Left e | Right !a

(These observations raise questions regarding whether the state itself in State and the error type in RightStrictEither should also be strict!) “Value strict” monads would have two benefits

  1. fewer space leaks due to accumulating thunks in values passed around in monadic computations.
  2. better code generation in general for those monadic computations (see, for example, State monad - memory exhausted - #13 by jaror)

There are two drawbacks

  1. They violate the monad law return a >>= f == f a, because return undefined >>= const (pure ()) == undefined. Maybe that’s OK. I don’t know that violating this law only up to strictness is a big deal.
  2. They will do unnecessary work when you really did mean to be lazy. However, I suspect the vast, vast majority of use cases don’t really want to be lazy (like the vast majority of use cases of foldl really want to be foldl'). It’s simple enough to recover lazy behaviour through data Lazy a = Lazy a (at a very small, although non-zero cost) for those cases.

Have I missed some other drawback? Have I downplayed the importance of one of the two drawbacks above? If I’m defining my own monad, why shouldn’t I make it “value strict”?

[1] weak head normal form

2 Likes
One Billion Row challenge in Hs
#2

It’s not so easy to pin this on the data representation/strict fields of m, where m could be State/Either, but I think a simple denotational characterisation would be

Monad m is value-strict iff forall a, (thing :: m a). thing = (thing >>= \res -> return $! res).

That is, = is definitional equality on the semantic domain in which we denote Haskell terms, which naturally is quite a “deep” notion. This is the usual way we tend to reason about Haskell programs…

A very similar (often more permissible) characterisation might be in terms of an operational semantics of Haskell + observational equality. That would allow you to talk about “WHNF” and “evaluated”, but it takes a bit more work to formalise it and actually implies the denotational characterisation above (well, as always it’s a bit troublesome that you want to observe “different kinds of ⊥”, so it’s tricky to find the right semantic domain).

If a monad is value-strict in the above sense (perhaps “result-strict” is a more fitting term) and we’d expose that fact in in a type class class Monad m => StrictMonad m that the compiler is aware of, there’s potential for an optimisation here:

The compiler could insert a (>>= \res -> return $! res) continuation everywhere it sees a thing :: m a. That could reasonably done during Specialisation, where we can still see that some piece of code implements an action in a strict monad.

Then strictness analysis would have a lot more to chew on. Quite nice!

Actually, one could try and simply write a RULE

{-# RULES "strict monad" forall (thing :: m a). thing = thing >>= \res -> return $! res #-}

Alas, that RULE would have to be builtin because I don’t see how to express the StrictMonad constraint and also make sure that this RULE just applies once. And of course we wouldn’t want to apply it in situations such as replicateM 13 thing, where it introduces additional thunks. So a RULE might not be a good idea after all.

Note that this change to the Specialiser replaces the need for a strict data type which would normally encode the evaluatedness invariant.

Actually, inserting >>= \res -> return $! res is only part of the story: At every expr of the form _ >>= \arg -> _ we can also mark arg as “definitely evaluated” and use a call-by-value calling convention in the sense of -fworker-wrapper-cbv or #23890: Use unlifted types in Core to replace the STG tag-invariant-rewrite pass · Issues · Glasgow Haskell Compiler / GHC · GitLab.

This seems an optimisation worth discussing, but of course it needs library support through the StrictMonad class.

5 Likes
#3

Also, rules must start with a top level function on the left hand side.

1 Like
#4

Very interesting, thanks! Yes, I agree that “return strict” is a better name. I also like your specification for the property in question.

I think I may start by adding a StrictT type to strict-wrapper, like

newtype StrictT m a = HiddenMkStrictT m a
  deriving Monad

strictT :: m a -> StrictT m a
strictT act = HiddenMkStrictT (do a <- act; pure $! a)

runStrictT :: StrictT m a -> m a
runStrictT (HiddenMkStrictT act) = act

Then at least we can start trying this approach.

2 Likes
#5

I expect no type could be an instance of both StrictMonad and MonadFix. That may or may not count as a drawback.

2 Likes
#6

Interesting. For me it’s not a drawback because I’ve never wanted to use MonadFix. People who do want to use MonadFix could recover that functionality in a return-strict Monad by avoiding mfix :: (a -> m a) -> m a and instead using mfixLazy :: (a -> m (Lazy a)) -> m (Lazy a) (where data Lazy a = MkLazy a). wrapping in data Lazy a = MkLazy a.

[EDIT: corrected, you don’t need a new combinator]

#7

This is often out of user’s control: mfix is inserted by GHC when desugaring recursive do-notation.

#8

Users can still call mfix and wrap MkLazy manually. No problem, I think.

1 Like
#9

Thanks, yes, I was mistaken that you need to introduce a special, lazy, version of mfix to recover the desired behaviour. It’s sufficient to use the standard mfix with Lazy/MkLazy.

#10

For the record, I think the equivalent of the monad laws for return-strict monads are

  1. f >=> (g >=> h) == (f >=> g) >=> h (associativity, unchanged)
  2. f >=> pure == f (right identity, unchanged)
  3. pure >=> f == (f $!) (left identity, strictified)

(I’d be grateful if someone could double check that.)

So the important question is whether the weakening in 3 is too big a price to pay for the benefit we get from “return strict” monads making invalid laziness unrepresentable.

#11

There are two historical precedents for “result-strict” monadic types that I’m aware of:

As to your question of weakening: both articles address it, but the second (being the more recent one) is more concise - see page 27 again.

But more generally…every “proclamation of monadicity” for some imperative language I’ve seen in my search results thus far seems to completely ignore this detail. And in Haskell itself, there’s something of an “underground movement” towards banishing laziness from effect-centric code (usually driven by the desire to avoid space leaks too). But there’s also a historical precedent for that: see the remarks about update on page 15 of 31 in Monads for functional programming (1995).

1 Like
#12

When I want to use a strict monad, I’m willing to pay a semantic price: namely, to accept that every f I bind with behaves the same as f $!, or at least I’m fine with the compiler playing fast and loose. If I’m not willing to pay that price, then I can’t use a strict monad.

Under this assumption, all the monad laws hold. I.e., I have turned f == (f $!) into a precondition on the use of >>= rather than coping with it in a weird left identity law. I’m basically proposing a … wide subcategory of Hask, I think, one that keeps all the objects (types) but loses a few arrows (lazy functions). Although I’m doubtful whether the ominous Hask is actually a category that can express the difference between a lazy and a strict function… So maybe this was not helpful.

Either way, of course I can still call >>= with a lazy f, but then I lose left identity. That’s OK, IMO, and even the intention of the user.

1 Like
#13

Exactly! I typically want to work in return strict monads so that I don’t have to add strictness annotations manually. I’d love to hear from people who would find this an impediment. There are some in a related GitHub discussion and I’ve invited them to comment here.