hiso.hs

import Data.Functor.Day
import Data.Functor.Identity
import Data.Functor.Compose
import Data.Profunctor.Composition
import Data.Profunctor.Yoneda
import Data.Profunctor
import Control.Monad
import Control.Applicative
import qualified Control.Category as C
import qualified Control.Arrow as A

newtype FreeM f a = FreeM { runFreeM :: forall g. Monad g => (f ~> g) -> g a }
newtype FreeA f a = FreeA { runFreeA :: forall g. Applicative g => (f ~> g) -> g a }
newtype FreeP f a b = FreeP { runFreeP :: forall g. Profunctor g => (f ~~> g) -> g a b }
newtype FreePreArr f a b = FreePreArr { runFreePreArr :: forall g. (C.Category g, Profunctor g) => (f ~~> g) -> g a b }
newtype FreeArr f a b = FreeArr { runFreeArr :: forall g. A.Arrow g => (f ~~> g) -> g a b }

type (~>) f g = forall a. f a -> g a

class HFunctor (h :: (k -> *) -> (k -> *)) where
  hfmap :: (f ~> g) -> (h f ~> h g)

instance HFunctor (h g) => HFunctor (HFreeF h f g) where
  hfmap _ (HDoneF a) = HDoneF a
  hfmap n (HMoreF m) = HMoreF (hfmap n m)

instance Functor f => HFunctor (Compose f) where
  hfmap n (Compose fg) = Compose (fmap n fg)

instance HFunctor (Day f) where
  hfmap = trans2

newtype HFix (h :: (k -> *) -> (k -> *)) (a :: k) = HFix { unHFix :: h (HFix h) a }

hcata :: HFunctor h => (h f ~> f) -> HFix h ~> f
hcata halg = halg . hfmap (hcata halg) . unHFix

data HFreeF (h :: (k -> *) -> (k -> *) -> (k -> *)) (i :: k -> *) (f :: k -> *) (r :: k -> *) (a :: k) = HDoneF (i a) | HMoreF (h f r a)

type HFree h i f a = HFix (HFreeF h i f) a

data HFree' (h :: (k -> *) -> (k -> *) -> (k -> *)) i f a = HDone (i a) | HMore (h f (HFree' h i f) a)

type FreeMonad f a = HFix (HFreeF Compose Identity f) a 
type FreeApplicative f a = HFix (HFreeF Day Identity f) a

isoFreeMonadToFreeM :: Functor f => FreeMonad f a -> FreeM f a
isoFreeMonadToFreeM = hcata go 
  where
    go :: HFreeF Compose Identity f (FreeM f) a -> FreeM f a
    go m = case m of
      HDoneF (Identity ia) -> FreeM $ \k -> pure ia
      HMoreF (Compose hfra) -> FreeM $ \k -> (\g -> runFreeM g k) =<< k hfra

isoFreeApplicativeToFreeA :: FreeApplicative f a -> FreeA f a
isoFreeApplicativeToFreeA = hcata go 
  where
    go :: HFreeF Day Identity f (FreeA f) a -> FreeA f a
    go m = case m of
      HDoneF (Identity ia) -> FreeA $ \k -> pure ia
      HMoreF (Day x (FreeA y) z) -> FreeA $ \k -> liftA2 z (k x) (y k)

isoHFreeToHFree' :: HFunctor (h f) => HFree h i f a -> HFree' h i f a
isoHFreeToHFree' (HFix (HDoneF ia)) = HDone ia
isoHFreeToHFree' (HFix (HMoreF hfra)) = HMore (hfmap isoHFreeToHFree' hfra)

type (~~>) f g = forall a b. f a b -> g a b

class HHFunctor (h :: (k -> k -> *) -> (k -> k -> *)) where
  hhfmap :: (f ~~> g) -> (h f ~~> h g)

instance HHFunctor (h g) => HHFunctor (HHFreeF h f g) where
  hhfmap n (HHDoneF iab) = HHDoneF iab
  hhfmap n (HHMoreF m) = HHMoreF (hhfmap n m)

instance HHFunctor (Procompose h) where
  hhfmap n (Procompose p1 p2) = Procompose p1 (n p2)

newtype HHFix (h :: (k -> k -> *) -> (k -> k -> *)) (a :: k) (b :: k) = HHFix { unHHFix :: h (HHFix h) a b }

hhcata :: HHFunctor h => (h f ~~> f) -> HHFix h ~~> f
hhcata hhalg = hhalg . hhfmap (hhcata hhalg) . unHHFix

data HHFreeF (h :: (k -> k -> *) -> (k -> k -> *) -> (k -> k -> *)) (i :: k -> k -> *) (f :: k -> k -> *) (r :: k -> k -> *) (a :: k) (b :: k) = HHDoneF (i a b) | HHMoreF (h f r a b)

type HHFree h i f a b = HHFix (HHFreeF h i f) a b

data HHFree' (h :: (k -> k -> *) -> (k -> k -> *) -> (k -> k -> *)) i f a b = HHDone (i a b) | HHMore (h f (HHFree' h i f) a b)

isoHHFreeToHHFree' :: HHFunctor (h f) => HHFree h i f a b -> HHFree' h i f a b
isoHHFreeToHHFree' (HHFix (HHDoneF iab)) = HHDone iab
isoHHFreeToHHFree' (HHFix (HHMoreF hfrab)) = HHMore (hhfmap isoHHFreeToHHFree' hfrab)

type FreePreArrow f a b = HHFix (HHFreeF Procompose (->) f) a b
type FreeArrow p a b = FreePreArrow (Coyoneda p) a b

isoCoyonedaToFreeP :: Coyoneda f a b -> FreeP f a b
isoCoyonedaToFreeP (Coyoneda ax yb p1) = FreeP $ \k -> dimap ax yb (k p1)

isoFreePreArrowToFreePreArr :: FreePreArrow f a b -> FreePreArr f a b
isoFreePreArrowToFreePreArr = hhcata go 
  where
    go :: HHFreeF Procompose (->) f (FreePreArr f) a b -> FreePreArr f a b
    go m = case m of
      HHDoneF iab -> FreePreArr $ \k -> rmap iab C.id
      HHMoreF (Procompose p1 (FreePreArr p2)) -> FreePreArr $ \k -> k p1 C.<<< p2 k

isoFreeArrowToFreeArr :: FreeArrow f a b -> FreeArr f a b
isoFreeArrowToFreeArr = hhcata go where
  go :: HHFreeF Procompose (->) (Coyoneda f) (FreeArr f) a b -> FreeArr f a b
  go m = case m of
    HHDoneF iab -> FreeArr $ \k -> A.arr iab
    HHMoreF (Procompose (Coyoneda ax yb p1) (FreeArr p2)) -> FreeArr $ \k -> yb A.^<< k p1 C.<<< ax A.^<< p2 k