Algebra for a profunctor

ProAlg.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

import Data.Profunctor
import Data.Profunctor.Composition
import Data.Functor.Const
import Data.Kind (Type)


type ProAlg p x = p x x -- x is the carrier
type ProAlgArr x y = x -> y -- a carrier map phi, s.t. rmap phi algX == lmap phi algY

class HasInitialAlg p where
  type InitCarrier p :: Type
  initAlg :: ProAlg p (InitCarrier p)
  isInit :: ProAlg p y -> ProAlgArr (InitCarrier p) y
  -- s.t. rmap (isInit algY) initAlg == lmap (isInit algY) algY

class HasTerminalAlg p where
  type TermCarrier p :: Type
  termAlg :: ProAlg p (TermCarrier p)
  isTerm :: ProAlg p x -> ProAlgArr x (TermCarrier p)
  -- s.t. rmap (isTerm algX) algX == lmap (isTerm algX) termAlg


newtype Fix f = Fix { runFix :: f (Fix f) }
cata :: Functor f => (f x -> x) -> Fix f -> x
cata alg = alg . fmap (cata alg) . runFix

ana :: Functor f => (x -> f x) -> x -> Fix f
ana coalg = Fix . fmap (ana coalg) . coalg

instance Functor f => HasInitialAlg (Costar f) where
  type InitCarrier (Costar f) = Fix f
  initAlg = Costar Fix
  isInit (Costar alg) = cata alg
  -- rmap (isInit algY) initAlg == lmap (isInit algY) algY
  -- => cata alg . Fix == fmap (cata alg) . alg

instance Functor f => HasTerminalAlg (Star f) where
  type TermCarrier (Star f) = Fix f
  termAlg = Star runFix
  isTerm (Star coalg) = ana coalg
  -- rmap (isTerm algX) algX == lmap (isTerm algX) termAlg
  -- => fmap (ana coalg) . coalg == runFix . ana coalg


data Nat = Z | S Nat
primRec :: a -> (a -> a) -> Nat -> a
primRec z _ Z = z
primRec z s (S n) = s (primRec z s n)

data NatAlg a b = NatAlg b (a -> b)
instance Profunctor NatAlg where
  dimap l r (NatAlg z s) = NatAlg (r z) (r . s . l)
instance HasInitialAlg NatAlg where
  type InitCarrier NatAlg = Nat
  initAlg = NatAlg Z S
  isInit (NatAlg z s) = primRec z s
  -- rmap (isInit algY) initAlg == lmap (isInit algY) algY
  -- => NatAlg (primRec z s Z) (primRec z s . S) == NatAlg z (s . primRec z s)
  -- => primRec z s Z == z && primRec z s . S = s . primRec z s

data ListAlg x a b = ListAlg b (x -> a -> b)
instance HasInitialAlg (ListAlg x) where
  type InitCarrier (ListAlg x) = [x]
  initAlg = ListAlg [] (:)
  isInit (ListAlg n c) = foldr c n


data Stream x = Cons { hd :: x, tl :: Stream x }
data StreamCoalg x a b = StreamCoalg (a -> x) (a -> b)
instance Profunctor (StreamCoalg x) where
  dimap l r (StreamCoalg h t) = StreamCoalg (h . l) (r . t . l)
instance HasTerminalAlg (StreamCoalg x) where
  type TermCarrier (StreamCoalg x) = Stream x
  termAlg = StreamCoalg hd tl
  isTerm (StreamCoalg h t) = go where
    go y = Cons (h y) $ go (t y)
  -- rmap (isTerm algX) algX == lmap (isTerm algX) termAlg
  -- => StreamCoAlg h (go . t) == StreamCoalg (hd . go) (tl . go)
  -- => h == hd . go && go . t == tl . go



-- Based on https://ncatlab.org/nlab/show/algebra+for+a+profunctor#coalgebras_in_prof
-- This doesn't seem to go anywhere
type CoAlgInPro p c = c :-> Procompose c p
proAlgAsCoAlgInPro :: Profunctor p => ProAlg p x -> CoAlgInPro p (Star (Const x))
proAlgAsCoAlgInPro p (Star f) = Procompose (Star Const) (lmap (getConst . f) p)

newtype FixP p a b = FixP { runFixP :: Procompose (FixP p) p a b }
termProAlg :: CoAlgInPro p (FixP p)
termProAlg = runFixP
fixPIsTerm :: Profunctor p => CoAlgInPro p c -> c :-> FixP p
fixPIsTerm coalg = FixP . (\(Procompose c p) -> Procompose (fixPIsTerm coalg c) p) . coalg