Categorical Data Types ala Hagino in 2 different ways

haginoGen.hs

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

import Data.Functor.Identity
import Data.Functor.Product
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 l g) => f (Left f g) -> g (Left f g)
left = leftAdjunct (\lf -> L $ \fga -> rightAdjunct (fga . fmap (cata fga)) lf)
mapLeft :: (Functor f, Adjunction l 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 r, Functor g) => f (Right f g) -> g (Right f g)
right = rightAdjunct (\(R fgr r) -> leftAdjunct (fmap (ana fgr) . fgr) r)
mapRight :: (Adjunction f r, 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 (Product (Const a) Identity)
count :: Stream Int
count = ana (\(Identity n) -> Pair (Const n) (Identity (n + 1))) 0
headStr :: Stream a -> a
headStr s = case right (Identity s) of Pair (Const h) _ -> h
tailStr :: Stream a -> Stream a
tailStr s = case right (Identity s) of Pair _ (Identity t) -> t
mapStream :: (a -> b) -> Stream a -> Stream b
mapStream f = mapRight id (\(Pair (Const a) t) -> Pair (Const (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))

haginoSpec.hs

{-# 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 faa) = faa fa

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


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 (Right fa a) = _fst fa a
snd :: Prod a b -> b
snd (Right fa a) = _snd fa a
(&&&) :: (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))

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 a = Left $ \fa -> _i1 fa a
i2 :: b -> Coprod a b
i2 b = Left $ \fa -> _i2 fa b
(|||) :: (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))

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

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 ((const x *** id) 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 :: n, _s :: n -> n }
type Nat = Left NatF
z :: Nat
z = Left $ \fa -> _z fa
s :: Nat -> Nat
s (Left n) = Left $ \fa -> _s fa (n fa)
pr :: a -> (a -> a) -> Nat -> a
pr f g = leftFactorizer (Nat f g)

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

data StreamF a l = Stream { _head :: l -> a, _tail :: l -> l }
type Stream a = Right (StreamF a)
head :: Stream a -> a
head (Right fx x) = _head fx x
tail :: Stream a -> Stream a
tail (Right fx x) = Right fx (_tail fx x)
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)