Categorical Data Types ala Hagino in 2 different ways

haginoGen.hs

{-# LANGUAGE RankNTypes, GADTs, LambdaCase #-}
import Data.Functor.Adjunction

import Data.Functor.Identity
import Data.Functor.Product
import Data.Functor.Sum
import Data.Functor.Const


newtype Left f g = L (forall l. (f l -> g l) -> l)
cata :: (f a -> g a) -> Left f g -> a
cata fg (L h) = h fg
left :: (Functor f, Adjunction __ g) => f (Left f g) -> g (Left f g)
left = leftAdjunct (\lf -> L $ \fga -> rightAdjunct (fga . fmap (cata fga)) lf)
mapLeft :: (Functor f, Adjunction __ g)
        => (forall a. h a -> f a)
        -> (forall a. g a -> i a)
        -> Left h i -> Left f g
mapLeft f g = cata (g . left . f)

data Right f g where R :: (f r -> g r) -> r -> Right f g
ana :: (f a -> g a) -> a -> Right f g
ana = R
right :: (Adjunction f __, Functor g) => f (Right f g) -> g (Right f g)
right = rightAdjunct (\(R fgr r) -> leftAdjunct (fmap (ana fgr) . fgr) r)
mapRight :: (Adjunction f __, Functor g)
         => (forall a. h a -> f a)
         -> (forall a. g a -> i a)
         -> Right f g -> Right h i
mapRight f g = ana (g . right . f)


-- if g has a left adjoint, it is isomorphic to a |-> Left (Const a) g
fromLeft :: Adjunction l g => Left (Const a) g -> l a
fromLeft = cata (unit . getConst)
toLeft :: Adjunction l g => l a -> Left (Const a) g
toLeft = counit . fmap (left . Const)

-- if f has a right adjoint, it is isomorphic to a |-> Right f (Const a)
fromRight :: Adjunction f r => Right f (Const a) -> r a
fromRight = fmap (getConst . right) . unit
toRight :: Adjunction f r => r a -> Right f (Const a)
toRight = ana (Const . counit)



-- Some examples

type Nat = Left Maybe Identity
nat2int :: Nat -> Int
nat2int = cata (Identity . maybe 0 (+1))
z :: Nat
z = runIdentity (left Nothing)
s :: Nat -> Nat
s n = runIdentity (left (Just n))

type Stream a = Right Identity ((,) a)
count :: Stream Int
count = ana (\(Identity n) -> (n, n + 1)) 0
headStr :: Stream a -> a
headStr s = fst (right (Identity s))
tailStr :: Stream a -> Stream a
tailStr s = snd (right (Identity s))
mapStream :: (a -> b) -> Stream a -> Stream b
mapStream f = mapRight id (\(a, t) -> (f a, t))

type Exp a b = Right ((,) a) (Const b)
exp :: (a -> b) -> Exp a b
exp = ana (\(a, ab) -> Const (ab a))
unexp :: Exp a b -> (a -> b)
unexp e a = getConst (right (a, e))

type Moore i o = Right (Sum ((,) i) Identity) ((,) o)
moore :: (Sum ((,) i) Identity a -> (o, a)) -> a -> Moore i o
moore = ana
output :: Moore i o -> o
output = fst . right . InR . Identity
next :: (i, Moore i o) -> Moore i o
next = snd . right . InL


type CombineL f1 f2 g1 g2 = Left (Sum f1 f2) (Product g1 g2)
cataCL :: (f1 a -> g1 a) -> (f2 a -> g2 a) -> (f1 a -> g2 a) -> (f2 a -> g1 a) -> CombineL f1 f2 g1 g2 -> a
cataCL fg11 fg22 fg12 fg21 = cata (\case InL f1 -> Pair (fg11 f1) (fg12 f1); InR f2 -> Pair (fg21 f2) (fg22 f2))
left1 :: (Functor f1, Functor f2, Adjunction __ g1, Adjunction __ g2)
      => f1 (CombineL f1 f2 g1 g2) -> g1 (CombineL f1 f2 g1 g2)
left1 f = case left (InL f) of Pair g _ -> g
left2 :: (Functor f1, Functor f2, Adjunction __ g1, Adjunction __ g2)
      => f2 (CombineL f1 f2 g1 g2) -> g2 (CombineL f1 f2 g1 g2)
left2 f = case left (InR f) of Pair _ g -> g

type CombineR f1 f2 g1 g2 = Right (Sum f1 f2) (Product g1 g2)
anaCR :: (f1 a -> g1 a) -> (f2 a -> g2 a) -> (f1 a -> g2 a) -> (f2 a -> g1 a) -> a -> CombineR f1 f2 g1 g2
anaCR fg11 fg22 fg12 fg21 = ana (\case InL f1 -> Pair (fg11 f1) (fg12 f1); InR f2 -> Pair (fg21 f2) (fg22 f2))
right1 :: (Functor g1, Functor g2, Adjunction f1 __, Adjunction f2 __)
       => f1 (CombineR f1 f2 g1 g2) -> g1 (CombineR f1 f2 g1 g2)
right1 f = case right (InL f) of Pair g _ -> g
right2 :: (Functor g1, Functor g2, Adjunction f1 __, Adjunction f2 __)
      => f2 (CombineR f1 f2 g1 g2) -> g2 (CombineR f1 f2 g1 g2)
right2 f = case right (InR f) of Pair _ g -> g

haginoSpec.hs

-- See http://web.sfc.keio.ac.jp/~hagino/thesis.pdf page 74

{-# LANGUAGE RankNTypes, GADTs #-}
import Prelude hiding (Left, Right, fst, snd, curry, foldr, head, tail)


newtype Left f = Left (forall a. f a -> a)
data Right f where Right :: f a -> a -> Right f

leftFactorizer :: f a -> Left f -> a
leftFactorizer fa (Left f) = f fa

rightFactorizer :: f a -> a -> Right f
rightFactorizer = Right

emb :: (forall a. f a -> b -> a) -> b -> Left f
emb f b = Left $ \fa -> f fa b

prj :: (forall a. f a -> a -> b) -> Right f -> b
prj f (Right fa a) = f fa a


data UnitF v = UnitF
type Unit = Right UnitF
unit :: a -> Unit
unit = rightFactorizer UnitF

data VoidF v = VoidF
type Void = Left VoidF
absurd :: Void -> a
absurd = leftFactorizer VoidF


data ProdF a b prod = Prod { _fst :: prod -> a, _snd :: prod -> b }
type Prod a b = Right (ProdF a b)
fst :: Prod a b -> a
fst = prj _fst
snd :: Prod a b -> b
snd = prj _snd
(&&&) :: (a -> b) -> (a -> c) -> a -> Prod b c
f &&& g = rightFactorizer (Prod f g)
(***) :: (a -> b) -> (c -> d) -> Prod a c -> Prod b d
f *** g = rightFactorizer (Prod (f . fst) (g . snd))
prod :: a -> b -> Prod a b
prod a b = (const a &&& const b) ()

data CoprodF a b coprod = Coprod { _i1 :: a -> coprod, _i2 :: b -> coprod }
type Coprod a b = Left (CoprodF a b)
i1 :: a -> Coprod a b
i1 = emb _i1
i2 :: b -> Coprod a b
i2 = emb _i2
(|||) :: (a -> c) -> (b -> c) -> Coprod a b -> c
f ||| g = leftFactorizer (Coprod f g)
(+++) :: (a -> b) -> (c -> d) -> Coprod a c -> Coprod b d
f +++ g = leftFactorizer (Coprod (i1 . f) (i2 . g))


newtype ExpF a b exp = Exp { _eval :: Prod exp a -> b }
type Exp a b = Right (ExpF a b)
eval :: Prod (Exp a b) a -> b
eval p = case fst p of Right fx x -> _eval fx . prod x . snd $ p
curry :: (Prod a b -> c) -> a -> Exp b c
curry f = rightFactorizer (Exp f)
mapExp :: (a' -> a) -> (b -> b') -> Exp a b -> Exp a' b'
mapExp fa fb = rightFactorizer (Exp (fb . eval . (id *** fa)))


data NatF n = Nat { _z :: Unit -> n, _s :: n -> n }
type Nat = Left NatF
z :: Unit -> Nat
z = emb _z
s :: Nat -> Nat
s = emb $ \fa -> _s fa . leftFactorizer fa
pr :: (Unit -> a) -> (a -> a) -> Nat -> a
pr f g = leftFactorizer (Nat f g)

data ListF a l = List { _cons :: Prod a l -> l, _nil :: Unit -> l }
type List a = Left (ListF a)
cons :: Prod a (List a) -> List a
cons = emb $ \fa -> _cons fa . (id *** leftFactorizer fa)
nil :: Unit -> List a
nil = emb _nil
foldr :: (Prod a b -> b) -> (Unit -> b) -> List a -> b
foldr f g = leftFactorizer (List f g)
map :: (a -> b) -> List a -> List b
map f = leftFactorizer (List (cons . (f *** id)) nil)

data StreamF a l = Stream { _head :: l -> a, _tail :: l -> l }
type Stream a = Right (StreamF a)
head :: Stream a -> a
head = prj _head
tail :: Stream a -> Stream a
tail = prj $ \fx -> rightFactorizer fx . _tail fx
stream :: (l -> a) -> (l -> l) -> l -> Stream a
stream h t = rightFactorizer (Stream h t)
mapStream :: (a -> b) -> Stream a -> Stream b
mapStream f = rightFactorizer (Stream (f . head) tail)

data CoNatF n = CoNat { _pred :: n -> Coprod Unit n }
type CoNat = Right CoNatF
pred :: CoNat -> Coprod Unit CoNat
pred = prj $ \fx -> (id +++ rightFactorizer fx) . _pred fx
copr :: (n -> Coprod Unit n) -> n -> CoNat
copr f = rightFactorizer (CoNat f)

data MooreF i o moore = Moore { _next :: Prod moore i -> moore, _output :: moore -> o }
type Moore i o = Right (MooreF i o)
next :: Prod (Moore i o) i -> Moore i o
next p = case fst p of Right fx x -> rightFactorizer fx . _next fx . prod x . snd $ p
output :: Moore i o -> o
output = prj _output
moore :: (Prod a i -> a) -> (a -> o) -> a -> Moore i o
moore f g = rightFactorizer (Moore f g)
mapMoore :: (i' -> i) -> (o -> o') -> Moore i o -> Moore i' o'
mapMoore f g = rightFactorizer (Moore (next . (id *** f)) (g . output))


data CP f g p = P { _prl :: p -> f p, _prr :: p -> g p }
type P f g = Right (CP f g)
prl :: Functor f => P f g -> f (P f g)
prl = prj $ \fa -> fmap (rightFactorizer fa) . _prl fa
prr :: Functor g => P f g -> g (P f g)
prr = prj $ \fa -> fmap (rightFactorizer fa) . _prr fa
unfoldp :: (p -> f p) -> (p -> g p) -> p -> P f g
unfoldp f g = rightFactorizer (P f g)
mapp :: (Functor f, Functor g)
     => (forall a. f a -> h a)
     -> (forall a. g a -> i a)
     -> P f g -> P h i
mapp f g = rightFactorizer (P (f . prl) (g . prr))

data CF f g c = C { _inl :: f c -> c, _inr :: g c -> c }
type C f g = Left (CF f g)
inl :: Functor f => f (C f g) -> C f g
inl = emb $ \fa -> _inl fa . fmap (leftFactorizer fa)
inr :: Functor g => g (C f g) -> C f g
inr = emb $ \fa -> _inr fa . fmap (leftFactorizer fa)
foldc :: (f c -> c) -> (g c -> c) -> C f g -> c
foldc f g = leftFactorizer (C f g)
mapc :: (Functor f, Functor g)
     => (forall a. h a -> f a)
     -> (forall a. i a -> g a)
     -> C h i -> C f g
mapc f g = leftFactorizer (C (inl . f) (inr . g))