Motivation

A while ago, I decided to implement comonad support into my purescript-transformerless library. Unfortunately, I’ve never had a moment where I thought “you know … this situation calls for a comonad!” Hence, since my experience with them was limited, I wasn’t sure I was providing the “correct” instances and definitions. Moreover, I definitely did NOT want to manually transform the comonads in Control.Comonad.{Env, Store, Traced} by changing w to Identity and seeing what came out – although this is in the spirit of transformerless comonads, it’s definitely not fun.

Luckily for me, there are laws for comonads (and laws for Traced), so with a little luck it should be enough to prove my implementations satisfied those laws.

Background: Logic

You may have heard that “propositions are types”, also known as the Curry-Howard isomorphism. It basically relates certain type systems used in programming with certain logics: a type can be seen as a proposition in the corresponding logic, and a value inhabiting that type can be seen as a proof of said proposition.

However, this by itself is not enough to prove that an instance is law-abiding: this is because compilers tend not to have the ability to prove instances are law-abiding, they can merely confirm an expression is well-typed or that it has the type you claim it does. Just because your custom data-type MyMonad has an instance of Monad doesn’t mean it satisfies the ap = apply law, for example.

On the other hand, we can use the same equivalent logic to (dis)prove our instances’ lawfulness.

An easy example

Let’s start with something simple: showing that the Env comonad is a lawful Functor, without delegating the instance to the compiler via derive instance.

newtype Env e a = Env (Tuple e a)

instance functorEnv :: Functor (Env e) where
  map :: forall a b. (a -> b) -> Env e a -> Env e b
  map f (Env (Tuple e a)) = Env (Tuple e (f a))

You may notice this instance is equivalent to that of the underlying Tuple one. In other words, we could have defined it as map f (Env e) = Env (map f e).

So, the Functor typeclass has two laws:

1. map id = id
2. map f <<< map g = map (f <<< g)

This is where “equational reasoning” comes in handy: it’s very powerful, while also being quite simple.

In the following proof, each line is equivalent to the one after via equality. If you wish, you can mentally insert an = after each line, linking it to the next.

Proof of 1)

1. map id – Left-hand side
2. \ (Env (Tuple e a)) -> map id (Env (Tuple e a)) – η expansion
3. \ (Env (Tuple e a)) -> Env (Tuple e (id a)) – Definition of map
4. \ (Env (Tuple e a)) -> Env (Tuple e a)) – Definition of id
5. (\ x -> x) :: forall e a. Env e a -> Env e a – Renaming
6. id – Right-hand side

Proof of 2)

1. map f <<< map g – Left-hand side
2. \ (Env (Tuple e a)) -> (map f <<< map g) (Env (Tuple e a)) – η expansion
3. \ (Env (Tuple e a)) -> map f (map g (Env (Tuple e a))) – Definition of compose
4. \ (Env (Tuple e a)) -> map f (Env (Tuple e (g a))) – Definition of map g
5. \ (Env (Tuple e a)) -> Env (Tuple e (f (g a))) – Definition of map f
6. \ (Env (Tuple e a)) -> Env (Tuple e ((f <<< g) a)) – Definition of compose
7. \ (Env (Tuple e a)) -> map (f <<< g) (Env (Tuple e a)) – Definition of map
8. map (f <<< g) – η reduction

WIP