Clowns to the Left of me, Jokers to the Right

clowns-jokers.hs

-- http://strictlypositive.org/CJ.pdf

{-# language DeriveFunctor          #-}
{-# language FlexibleInstances      #-}
{-# language FunctionalDependencies #-}
{-# language LambdaCase             #-}
{-# language MultiParamTypeClasses  #-}
{-# language PatternSynonyms        #-}
{-# language ScopedTypeVariables    #-}
{-# language TypeOperators          #-}
{-# language UndecidableInstances   #-}

{-# options_ghc -Wall -fno-warn-name-shadowing #-}

import Data.Bifunctor
import Data.Void

-- 1. Introduction

data Expr0
  = Val0 Int
  | Add0 Expr0 Expr0

type Stack
  = [Either Expr0 Int]

-- Tail-recursive evaluator
--
--    +
--   / \
--  1   +
--     / \
--    2   3
--
-- eval (1 + (2 + 3))
-- load (1 + (2 + 3)) []
-- load 1 [L (2 + 3)]
-- unload 1 [L (2 + 3)]
-- load (2 + 3) [R 1]
-- load 2 [L 3, R 1]
-- unload 2 [L 3, R 1]
-- load 3 [R 2, R 1]
-- unload 3 [R 2, R 1]
-- unload 5 [R 1]
-- unload 6 []
-- 6
eval0 :: Expr0 -> Int
eval0 e =
  load e []
 where
  load :: Expr0 -> Stack -> Int
  load e s =
    case e of
      Val0 i ->
        unload i s
      Add0 e1 e2 ->
        load e1 (Left e2 : s)

  unload :: Int -> Stack -> Int
  unload v s =
    case s of
      [] ->
        v
      Left e : s' ->
        load e (Right v : s')
      Right v' : s' ->
        unload (v + v') s'

-- 2. Polynomial Functors and Bifunctors

-- Functor building blocks

data K1 a x
  = K1 a
  deriving Functor

data Id x
  = Id x
  deriving Functor

data (p :+ q) x
  = L1 (p x)
  | R1 (q x)
  deriving Functor
infixr 2 :+

data (p :* q) x
  = p x :* q x
  deriving Functor
infixr 3 :*

type One1
  = K1 ()

-- Maybe, decomposed

type Maybe'
  = One1 :+ Id

pattern Nothing' :: Maybe' a
pattern Nothing' = L1 (K1 ())

pattern Just' :: a -> Maybe' a
pattern Just' x = R1 (Id x)

-- 2.1 Datatypes as Fixpoints of Polynomial Functors

-- Expr, decomposed

type ExprP
  =  K1 Int
  :+ Id :* Id

pattern ValP :: Int -> ExprP x
pattern ValP n = L1 (K1 n)

pattern AddP :: x -> x -> ExprP x
pattern AddP e1 e2 = R1 (Id e1 :* Id e2)

{-# COMPLETE ValP, AddP #-}

data Mu f
  = In (f (Mu f))

type Expr
  = Mu ExprP

pattern Val :: Int -> Expr
pattern Val n = In (ValP n)

pattern Add :: Expr -> Expr -> Expr
pattern Add e1 e2 = In (AddP e1 e2)

{-# COMPLETE Val, Add #-}

-- Catamorphism

cata :: Functor p => (p v -> v) -> Mu p -> v
cata phi (In p) =
  phi (fmap (cata phi) p)

eval :: Expr -> Int
eval =
  cata phi
 where
  phi :: ExprP Int -> Int
  phi = \case
    ValP n ->
      n
    AddP n m ->
      n + m

-- 2.2 Polynomial Bifunctors

data K2 a x y
  = K2 a

instance Bifunctor (K2 a) where
  bimap _ _ (K2 a) =
    K2 a

data Fst x y
  = Fst x

instance Bifunctor Fst where
  bimap f _ (Fst x) =
    Fst (f x)

data Snd x y
  = Snd y

instance Bifunctor Snd where
  bimap _ g (Snd y) =
    Snd (g y)

data (p :++ q) x y
  = L2 (p x y)
  | R2 (q x y)
infixr 2 :++

instance (Bifunctor p, Bifunctor q) => Bifunctor (p :++ q) where
  bimap f g = \case
    L2 p -> L2 (bimap f g p)
    R2 q -> R2 (bimap f g q)

data (p :** q) x y
  = p x y :** q x y
infixr 3 :**

instance (Bifunctor p, Bifunctor q) => Bifunctor (p :** q) where
  bimap f g (p :** q) =
    bimap f g p :** bimap f g q

type One2
  = K2 ()

-- 2.3 Nothing is Missing

type Zero1
  = K1 Void

type Zero2
  = K2 Void

-- 3. Clowns, Jokers, and Dissection

data C p c j
  = C (p c)

instance Functor p => Bifunctor (C p) where
  bimap f _ (C p) =
    C (fmap f p)

data J p c j
  = J (p j)

instance Functor p => Bifunctor (J p) where
  bimap _ g (J p) =
    J (fmap g p)

class (Functor p, Bifunctor q) => D p q | p -> q where
  right :: Either (p j) (q c j, c) -> Either (j, q c j) (p c)

instance D (K1 a) (K2 Void) where
  right = rightK

instance D Id (K2 ()) where
  right = rightId

instance (D p p', D q q') => D (p :+ q) (p' :++ q') where
  right = rightSum

instance (D p p', D q q') => D (p :* q) (p' :** J q :++ C p :** q') where
  right = rightProd

-- 4. How to Creep Gradually to the Right

rightK :: Either (K1 a j) (K2 Void c j, c) -> Either (j, K2 Void c j) (K1 a c)
rightK = \case
  Left (K1 a) ->
    Right (K1 a)
  Right (K2 void, _) ->
    absurd void

rightId :: Either (Id j) (K2 () c j, c) -> Either (j, K2 () c j) (Id c)
rightId = \case
  Left (Id j) ->
    Left (j, K2 ())
  Right (K2 (), c) ->
    Right (Id c)

rightSum
  :: (D p p', D q q')
  => Either ((p :+ q) j) ((p' :++ q') c j, c)
  -> Either (j, (p' :++ q') c j) ((p :+ q) c)
rightSum = \case
  Left (L1 p) ->
    kL (right (Left p))
  Left (R1 q) ->
    kR (right (Left q))
  Right (L2 p, c) ->
    kL (right (Right (p, c)))
  Right (R2 q, c) ->
    kR (right (Right (q, c)))
 where
  kL :: Either (j, p' c j) (p c) -> Either (j, (p' :++ q') c j) ((p :+ q) c)
  kL = bimap (over2 L2) L1

  kR :: Either (j, q' c j) (q c) -> Either (j, (p' :++ q') c j) ((p :+ q) c)
  kR = bimap (over2 R2) R1

  over2 :: (a -> b) -> (x, a) -> (x, b)
  over2 = fmap

rightProd
  :: (D p p', D q q')
  => Either ((p :* q) j) ((p' :** J q :++ C p :** q') c j, c)
  -> Either (j, (p' :** J q :++ C p :** q') c j) ((p :* q) c)
rightProd = \case
  Left (p :* q) ->
    kP q (right (Left p))
  Right (L2 (p :** J q), c) ->
    kP q (right (Right (p, c)))
  Right (R2 (C p :** q), c) ->
    kQ p (right (Right (q, c)))

 where
  kP
    :: (D p p', D q q')
    => q j
    -> Either (j, p' c j) (p c)
    -> Either (j, (p' :** J q :++ C p :** q') c j) ((p :* q) c)
  kP q = \case
    Left (j, p') ->
      Left (j, L2 (p' :** J q))
    Right p' ->
      kQ p' (right (Left q))

  kQ
    :: (D p p', D q q')
    => p c
    -> Either (j, q' c j) (q c)
    -> Either (j, (p' :** J q :++ C p :** q') c j) ((p :* q) c)
  kQ p = \case
    Left (j, q') ->
      Left (j, R2 (C p :** q'))
    Right q' ->
      Right (p :* q')

tmap :: forall a b q p. D p q => (a -> b) -> p a -> p b
tmap f ps =
  continue (right (Left ps))
 where
  continue :: Either (a, q b a) (p b) -> p b
  continue = \case
    Left (a, q) ->
      continue (right (Right (q, f a)))
    Right p ->
      p

-- Tail-recursive catamorphism

tcata :: D p q => (p v -> v) -> Mu p -> v
tcata phi t =
  load phi t []

load :: D p q => (p v -> v) -> Mu p -> [q v (Mu p)] -> v
load phi (In p) =
  next phi (right (Left p))

unload :: D p q => (p v -> v) -> v -> [q v (Mu p)] -> v
unload phi v = \case
  [] ->
    v
  q : qs ->
    next phi (right (Right (q, v))) qs

next
  :: D p q
  => (p v -> v)
  -> Either (Mu p, q v (Mu p)) (p v)
  -> [q v (Mu p)]
  -> v
next phi x s =
  case x of
    Left (p, q) ->
      load phi p (q : s)
    Right p ->
      unload phi (phi p) s

eval1 :: Expr -> Int
eval1 = tcata phi
 where
  phi (ValP n) = n
  phi (AddP n m) = n + m