Laziness and the monad laws

Recently on haskell-cafe, the rather trivial module OneTuple was announced. I looked over the source and saw something that bugged me.

data OneTuple a = OneTuple { only :: a }

instance Functor OneTuple where
  fmap f (OneTuple x) = OneTuple (f x)

I never write functor instances this way. This is too strict; I would have written it like this instead:

instance Functor OneTuple where
  fmap f = OneTuple . f . only

Because it’s lazier. As I was composing a message explaining to the author why his instance was incorrect and why mine was correct, I realized something: his instance is correct and mine is incorrect! To see why, observe the functor laws:

  fmap id = id
  fmap (f.g) = fmap f . fmap g

My implementation satisfies the second law, but violates the first: fmap id ⊥ = OneTuple ⊥!

The same thing happens with the monad laws; I would have written the monad instance this way:

  instance Monad OneTuple where
    return = OneTuple
    m >>= f = f (only m)

But this violates the right unit law:

  m >>= return = m

Since ⊥ >>= return = return (only ⊥) = OneTuple ⊥ /= ⊥

So, in summary: most Haskell hackers know not to make their functions too strict. But we have to be careful not to make our functions too lazy either, and not just from an efficiency standpoint!

About these ads

5 thoughts on “Laziness and the monad laws

  1. Hello, I am new to haskell. Could you explain what makes your Functor instance “lazier” ? Also why does the original Functor instance (ie … = OneTuple (f x)) not violate the first functor law as well? Sorry if the question is basic. i am just puzzled.

  2. Pattern matches in Haskell are by default strict, so even if you have:

    foo (OneTuple x) = 42
    

    And don’t depend on x at all, still foo undefined will throw an error. Contrast this with:

    foo' x = 42
    

    In which foo' undefined will happily evaluate to 42.

    So my fmap, call it bad_fmap, always returns the OneTuple constructor, regardless of the definedness of its value. Thus foo (bad_fmap id undefined) will evaluate to 42, whereas the correct behavior (because of the functor laws) is foo (fmap id undefined) = undefined.

    The way the cool kids talk about this is with domain theory. For example, it seems as though the type () is inhabited by only one value: (). But this is not true; in fact it is inhabited by two: () and ⊥. These can be distinguished using pattern matching:


    isBottom () = False

    (isBottom ⊥ = ⊥, it would be illegal for isBottom ⊥ = True, since all functions are required to be “monotone”; and in practice for it to do this would require solving the halting problem)

    So OneTuple adds an extra ⊥ to whatever type you give it. OneTuple () has three inhabitants: ⊥, OneTuple ⊥, and OneTuple ().

    So, the functor law bad_fmap id x = x is violated because it is incorrect when x is ⊥. On the other hand, the correct fmap is correct because it pattern matches, and thus if you give it ⊥ it will immediately return ⊥.

    Did that help? Sorry if it was a bit rushed.

  3. Absolutely it does, and I’ve been falling in love with it for the past month or so. It’s the CIC, the Calculus of Inductive Constructions, the type system of Coq. Epigram’s and Agda’s also have type systems powerful enough to express the monad laws.

    For example, here is how you might write Monad in Coq (I’ve done this a few times):

    Set Implicit Arguments.
    
    Record Monad (M:Type):Type := mkMonad {
      unit : forall a, a -> M a;
      bind : forall a b, (a -> M b) -> M a -> M b;
    
      prop_leftunit : forall f x, bind f (unit x) = f x;
      prop_rightunit : forall x, bind unit x = x;
      prop_assoc : forall m f g,
        bind g (bind f m) = bind (fun x => bind g (f x)) m
    }.
    

    Then to correctly instantiate Monad, you must provide implementations for each of these five methods. Any implementation of the prop_* methods which typechecks is a proof of that property.

    However, the discussion in this article is rather moot in Coq, because Coq doesn’t have any bottoms.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s