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!

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.

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

And don’t depend on x at all, still

`foo undefined`

will throw an error. Contrast this with: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 to42, 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

threeinhabitants: ⊥, 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.

I understand now. Thank you for taking the time to clarify that for me.

I wonder whether a type system under which Monad laws can be expressed exists.

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):

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.