PureScript by Example - 8.7 Monads and Applicatives - Exercise 6 Solution (Written Exercise)

Proof.md

Theorem

In PureScript, the expression:

lift2 f (pure a) (pure b)

is equivalent to:

pure (f a b)

for all monads m (satisfying the monad laws) and all argument types a, b in function f :: a -> b -> c.

Proof

lift2 f (pure a) (pure b)

is equivalent to (by definition of lift2):

f <$> (pure a) <*> (pure b)

which is equivalent to (by definition of <$> and <*>, taking into account m is a monad):

ap (map f (pure a)) (pure b)

which translates to the following in do notation:

do
  f' <- do
    x <- pure a
    pure (f x)
  y <- pure b
  pure (f' y)

which, by the associativity law, reduces to:

do
  x <- pure a
  f' <- pure (f x)
  y <- pure b
  pure (f' y)

which, by repeated application of the left identity law, reduces to:

do
  f' <- pure (f a)
  y <- pure b
  pure (f' y)

do
  y <- pure b
  pure (f a y) -- equivalent to pure ((f a) y)

do
  pure (f a b)

The final expression is then trivially equivalent to pure (f a b), completing the proof.