Testing monads with plated

plate.hs

-- run with
-- stack ghci --package lens --ghci-options="-XDeriveDataTypeable" plate.hs

{-# LANGUAGE DeriveDataTypeable #-}

import Data.Data
import Data.Data.Lens
import Control.Lens.Plated

data E
  = Add E E
  | Mul E E
  | Val Int
  | Var String
  deriving (Show, Data)

instance Plated E where
  plate = uniplate

data Modify a
  = Changed a
  | Unchanged a
  deriving Show

-- Functor laws are satisfied by inspection.
-- fmap id  ==  id
-- fmap (f . g)  ==  fmap f . fmap g
instance Functor Modify where
  fmap f (Changed e) = Changed (f e)
  fmap f (Unchanged e) = Unchanged (f e)

-- Identity: pure id <*> v = v
-- Proof: Equations 3 and 4 imply LHS is Changed iff v is Changed.
--
-- Composition: pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
-- Proof: The LHS will have a Changed iff one of u, v, w are like Changed f.
-- Similarly for the RHS.
--
-- Homomorphism: pure f <*> pure x = pure (f x)
-- Proof: equations 4 and 5.
--
-- Interchange: u <*> pure y = pure ($ y) <*> u
-- Proof: Equations 2 and 4 imply LHS is Changed iff u is Changed.
-- Equations 3 and 4 imply that RHS is Changed iff u is Changed.
instance Applicative Modify where
  Changed f <*> Changed e = Changed (f e)       -- (1)
  Changed f <*> Unchanged e = Changed (f e)     -- (2)
  Unchanged f <*> Changed e = Changed (f e)     -- (3)
  Unchanged f <*> Unchanged e = Unchanged (f e) -- (4)
  pure = Unchanged                              -- (5)

-- pure a >>= k = k a
-- Proof: Equation 2
--
-- m >>= return =  m
-- Proof: Equation 1.1 and 2 imply that LHS is Changed iff m is Changed.
--
-- m >>= (\x -> k x >>= h) = (m >>= k) >>= h
-- Proof:
--   If m is Changed, then m >>= f is Changed for all f.
--   If m = Unchanged x, then RHS is (m >>= h) >>= k = h x >>= k.
--   LHS becomes Unchanged x >>= (\y -> h y >>= k) = h x >>= k
instance Monad Modify where
  Changed x >>= f = case f x of
    Unchanged a -> Changed a -- (1.1)
    Changed a   -> Changed a -- (1.2)
  Unchanged x >>= f = f x    -- (2)

simplify :: E -> Modify E
simplify (Add (Val i) (Val j)) = Changed $ Val (i + j)
simplify (Mul (Val i) (Val j)) = Changed $ Val (i * j)
simplify e = Unchanged e

tf = transformM simplify

e0 = Add (Val 0) (Mul (Val 10) (Val 7))

e1 = Mul (Var "x") (Add (Val 1) (Val 2))

e2 = Add (Var "x") (Val 2)

e3 =
  Add
   (Add (Var "x") (Val 1))
   (Mul
    (Var "y")
    (Mul (Val 0) (Val 0)))