Make Product Instances Explicitly Lazy

[BebeSparkelSparkel]

Summary

Product from Data.Functor.Product has problematic strictness in its instances due to pattern matching. This causes:

• recursive uses to be non-terminal
• out of order failure

Problematic Instances:

• Applicative
• Alternative
• MonadPlus
• MonadZip
• Semigroup - impossible to create infinite data structures

For example using Applicative

-- pattern matching causes strictness
Pair f g <*> Pair x y = Pair (f <*> x) (g <*> y)

-- should be defined with explicit laziness
~(Pair f g) <*> ~(Pair x y) = Pair (f <*> x) (g <*> y)

Steps to reproduce

ghci
import Data.Functor.Product
import Control.Applicative
-- x demonstrates out of order failure
x = empty *> undefined :: Product Maybe Maybe ()
x
-- *** Exception: Prelude.undefined

-- y demonstrates non-termination
y = empty *> y :: Product Maybe Maybe ()
y
-- does not terminate

Expected behavior

x should produce Pair Nothing Nothing

y should terminate and produce Pair Nothing Nothing.

[treeowl]

Does this type have other instances that are lazy the way you want? If not, I think it would be much better to make a new type to do what you want. If so, there's a (very subtle) discussion to be had around consistency vs. backwards compatibility.

[mixphix]

Can increasing the laziness of the pattern match make any programs "less correct"? I find it hard to believe that making this change would limit, rather than broaden, the scope of correctly-evaluated programs.

[BebeSparkelSparkel]

@treeowl Could you elaborate on how adding explicit laziness would break backwards compatibility?

[tomjaguarpaw]

Can increasing the laziness of the pattern match make any programs "less correct"?

Could you elaborate on how adding explicit laziness would break backwards compatibility?

It can lead to space leaks

[mixphix]

I'll file that under "feature". Strictness can easily be reintroduced in user-land, I think we should provide the most accurate definition we can.

[BebeSparkelSparkel]

@tomjaguarpaw Thanks for pointing out space leaks.

I have tried:

 pure () `mplus` Pair undefined undefined :: Product Maybe Maybe ()

Which works as expected. It seems to me that the only difference in space is the unpacking of the Pair constructor because both of its contents are still lazily evaluated.

Is there a case where this could cause a major space leak?

[BebeSparkelSparkel]

It was pointed out by @Lysxia in

Lysxia/generic-data#68 (comment)

that GHC.Generics.(:*:) has the same strictness problem. Should I include (:*:) in this proposal or create a new proposal?

[tomjaguarpaw]

Actually, I shouldn't have said it can lead to a space leak, just that it can lead to different memory usage patterns. I suspect the memory usage of the lazy version is likely to be better. I don't see, however, how it's possible to recover the strict behaviour from the lazy one "in user-land".

[BebeSparkelSparkel]

Why one would want to recover the strictness of unpacking Pair?

[mixphix]

The kind of user-land fix could be a newtype wrapper that would reimplement the stricter instance, or possibly an unpacked data declaration that addresses other concerns like working with unlifted types, should performance be of such concern. These kinds of applications are not universal and should not govern the domain of correctness for the (categorically) universal Product's instances.

[rhendric]

If it helps the committee, note that this is in part a lawfulness issue: the documentation for Applicative states that (*>) should equal (>>) when the applicative functor is also a Monad, but the example in the OP demonstrates that this law only holds up to strictness.

(This law would be upheld by making only the RHS of <*> lazy, but for non-Monad purposes both sides ought to be equally lazy—consider that <*> at Product (Backwards Maybe) (Backwards Maybe) would want to reduce the RHS before reducing the LHS.)

[tomjaguarpaw]

The kind of user-land fix could be a newtype wrapper that would reimplement the stricter instance

Oh, are you thinking of a newtype wrapper around Product itself?

[treeowl]

I have determined that the current Applicative and Monad instances (which were added at the same time) are indeed inconsistent. The Monad instance is

instance (Monad f, Monad g) => Monad (Product f g) where
    Pair m n >>= f = Pair (m >>= fstP . f) (n >>= sndP . f)
      where
        fstP (Pair a _) = a
        sndP (Pair _ b) = b

We can reason thus:

liftA2 f (Pair m n) q

= -- Monad/Applicative and Monad/Functor consistency laws

Pair m n >>= \x -> f x <$> q

= -- Definition of >>=

Pair
  (m >>= \x -> fstP (f x <$> q))
  (n >>= \x -> sndP (f x <$> q))

= -- Definitions of fmap and the helper functions, and case reduction

Pair
  (m >>= \x -> case q of Pair q1 _ -> f x <$> q1)
  (n >>= \x -> case q of Pair _ q2 -> f x <$> q2)

= -- Presumed strictness of underlying fmaps. EDIT: this is a bad assumption! See my comment below.

Pair
  (m >>= \x -> f x <$> fstP q)
  (n >>= \x -> f x <$> sndP q)

= -- Monad/Applicative/Functor consistency for underlying monads

Pair
  (liftA2 f m (fstP q))
  (liftA2 f n (sndP q))

Furthermore, it seems to be impossible to write a Monad instance compatible with the current behavior of liftA2, at least without some additional ad hoc constraint. That leads to several options:

1. Change liftA2 to be lazy in its second Product argument (but still strict in its first). Edit: This will only produce a lawful Applicative from strict underlying ones.
2. Change liftA2 to be lazy in both Product arguments as proposed, change >>= to be lazy in its first argument, and change fmap to be lazy in its second argument. This will produce a Functor that is not strictly lawful (fmap id undefined ≠ undefined).
3. Leave the Applicative instance alone and remove the Monad instance.
4. Do nothing.

My personal bias for basic types is always strict lawfulness, which narrows the options to 1 and 3. Of those, 1 is less intrusive (doesn't stop working code from compiling). Those who like to make loops will prefer 2, of course.

The real solution: offer all three reasonable options (1, 2, and 3) in different types, from modules with names like Strict (no Monad instance, strictly lawful Applicative), LeftStrict (liftA2 strict in its first Product argument, strictly lawful Applicative and Monad. Edit: lawful with the modification of my comment below), and Lazy (everything totally relaxed, not strictly lawful but useful).

[treeowl]

I just remembered that the strictness of underlying fmaps I assumed above is not valid for every lawful Monad. In particular, it doesn't apply to Identity! So the only way I see to match the Monad instance precisely is

instance (Monad m, Monad n) => Applicative (Product m n) where 
  liftA2 f (Prod m n) q =
    Pair
      (m >>= \x -> case q of Pair q1 _ -> f x <$> q1)
      (n >>= \x -> case q of Pair _ q2 -> f x <$> q2)

Ouch!

[mixphix]

I don't like requiring Monad superclasses for an Applicative instance of their product, but ideally the Monad behaviour should not contradict the Applicative. @treeowl, how does your definition of liftA2 here conceptually differ from the (<*>) with lazy pattern matching as defined above?

[treeowl]

@mixphix There are too many different things running around now for me to know what exactly you're asking me to compare to what 😕. That's mostly my fault.

[Lysxia]

If we care that the laws hold even with strictness in mind, the identity law pure id <*> v = v implies some amount of strictness pure id <*> _|_ = _|_. The current strict instance is the more correct one as far as that law is concerned.

Is there actually a consensus, if not a policy, that type class laws in base should hold even with undefined?

[rhendric]

This has the feel of swallowing a spider to catch a fly, but now I wonder if the fields on Product should be strict, which would allow for lazy patterns in <*> without violating the identity law. (Does that break other laws?)

Edit: Hm, on second thought that may have appreciable performance implications for the Monad instance, because fstP and sndP want to be able not to force the other side of the pair.

[treeowl]

This has the feel of swallowing a spider to catch a fly, but now I wonder if the fields on Product should be strict, which would allow for lazy patterns in <*> without violating the identity law. (Does that break other laws?)

It's no good (legally) when one of the underlying functors is Identity.

[BebeSparkelSparkel]

What I am gathering from the above is that the current implementation of Product is not lawful, but there actually no way to make it a lawful Applicative and Monad. Is this correct?

[phadej]

I find it always confusing to figure out how strictly (sorry for the pun) laws like fmap id x ≡ x should be interpreted in regard to strictness. I.e. what kind of relation the ≡ is. If fmap id undefined = undefined is required, then for all product types strict pattern match is required. OTOH, there is bimap id id ≡ id law, and it's not "stricltly" true for tuples, In fact, it's documented to be Class laws for tuples hold only up to laziness.

So given that, I consider that laws re-strictness can be interpreted as authors seems best. Whether there should be lazy or strict pattern match is arbitrary.

Until there is some policy&guideline, there will be endless debates. (IIRC the Bifunctor discussion ended up with "we won't do anything, let's just document the case", e.g. now second is not fmap)

[Bodigrim]

Stuff like

~(Pair f g) <*> ~(Pair x y) = Pair (f <*> x) (g <*> y)

is often prone to be a source of space leaks, because forcing result to WHNF evaluates exactly nothing: it does not trigger evaluation of any of arguments. E. g., putting such Pair as a value into Data.Map.Strict is of no use.