Proof of equivalence for van Laarhoven lenses

Lenses.hs

-- Example from http://arxiv.org/pdf/1103.2841v1.pdf
-- "Functor is to Lens as Applicative is to Biplate"

-- NOTE: Proof of equivalence here _IMPLIES_ proof of equivalence for
-- van Laarhoven lenses (Section 4)

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}

{-------------------------------------------------------------------------------
  Concrete
-------------------------------------------------------------------------------}

data Concrete b a = Store {
    peek :: b -> a
  , pos  :: b
  }

instance Functor (Concrete b) where
  fmap f Store{..} = Store {
      peek = f . peek
    , pos  = pos
    }

type Lens a b = a -> Concrete b a

first :: Lens (a, b) a
first (x, y) = Store { peek = \z -> (z, y) , pos = x }

idLens :: Lens a a
idLens x = Store { peek = \z -> z , pos = x }

{-------------------------------------------------------------------------------
  Abstract
-------------------------------------------------------------------------------}

type Abstract b a = forall f. Functor f => (b -> f b) -> f a

{-------------------------------------------------------------------------------
  Translation
-------------------------------------------------------------------------------}

-- this is what they call iso1 in the paper
abstract :: Concrete b a -> Abstract b a
abstract Store{..} f = fmap peek (f pos)

-- this is what they call iso2 in the paper
concrete :: Abstract b a -> Concrete b a
concrete s = s idLens

{-------------------------------------------------------------------------------
  Proof of equivalence
-------------------------------------------------------------------------------}

-- iso2 . iso1
leftIdentity :: Concrete b a -> [Concrete b a]
leftIdentity s@Store{..} = [
    concrete (abstract s)
      -- expand abstract
  , concrete (\f -> fmap peek (f pos))
      -- expand concrete
  , (\f -> fmap peek (f pos)) idLens
      -- expand idLens
  , (\f -> fmap peek (f pos)) (\x -> Store { peek = \z -> z , pos = x })
      -- apply
  , fmap peek ((\x -> Store { peek = \z -> z , pos = x }) pos)
      -- again
  , fmap peek (Store { peek = \z -> z , pos = pos })
      -- apply fmap
  , Store { peek = peek . (\z -> z) , pos = pos }
      -- apply
  , Store { peek = peek, pos = pos }
      -- done
  , s
  ]

newtype ReifiedAbstract b a = R (Abstract b a)

-- iso1 . iso2
rightIdentity :: Abstract b a -> [ReifiedAbstract b a]
rightIdentity s = [
    R $ abstract (concrete s)
     -- expand concrete
  , R $ abstract (s idLens)

     -- s == Store { peek s, pos s }
  , R $ abstract Store { peek = peek (s idLens), pos = pos (s idLens ) }
     -- inline abstract
  , R $ \f -> fmap (peek (s idLens)) (f (pos (s idLens)))
     -- definition of eta
  , R $ \f -> eta f (s idLens)
     -- parametricity (applied to `eta f`)
  , R $ \f -> s (eta f . idLens)
     -- expand eta
  , R $ \f -> s ((\s' -> fmap (peek s') (f (pos s'))) . idLens)
     -- expand idLens
  , R $ \f -> s ((\s' -> fmap (peek s') (f (pos s'))) . (\x -> Store { peek = \z -> z , pos = x }))
     -- simplify
  , R $ \f -> s (\x -> fmap (\z -> z) (f x))
     -- fmap id = id
  , R $ \f -> s (\x -> f x)
     -- simplify
  , R $ \f -> s f
     -- simplify
  , R $ s
  ]

eta :: Functor f => (b -> f b) -> Concrete b a -> f a
eta f s = fmap (peek s) (f (pos s))