doubly-indexed `Free` profunctor, `lmap` using doubly-indexed recursion-schemes

HHFree.hs

{-# LANGUAGE InstanceSigs, RankNTypes, PolyKinds, DataKinds, TypeOperators, TypeFamilies, FlexibleContexts, BlockArguments, ScopedTypeVariables #-}

module HHFree where

import Data.Profunctor
import Data.Profunctor.Yoneda
import Data.Profunctor.Composition

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 }

type instance HHBase (HHFix h) = h

instance (HHFunctor h) => HHRecursive (HHFix h) where
  hhproject = unHHFix

instance (HHFunctor h) => HHCorecursive (HHFix h) where
  hhembed = HHFix

type family HHBase (h :: k -> k -> *) :: (k -> k -> *) -> (k -> k -> *)

class HHFunctor (HHBase h) => HHRecursive (h :: k -> k -> *) where
  hhproject :: h ~~> (HHBase h) h

class HHFunctor (HHBase h) => HHCorecursive (h :: k -> k -> *) where
  hhembed :: (HHBase h) h ~~> h

type HHAlgebra w f = (w f ~~> f)

hhcata :: (HHRecursive h, HHFunctor (HHBase h)) => HHAlgebra (HHBase h) f -> h ~~> f
hhcata algebra = algebra . hhfmap (hhcata algebra) . hhproject

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)

type instance HHBase (HHFree' h i f) = HHFreeF h i f

instance (HHFunctor (h f)) => HHRecursive (HHFree' h i f) where
  hhproject h = case h of
    HHDone ia -> HHDoneF ia
    HHMore hfra -> HHMoreF hfra

instance (HHFunctor (h f)) => HHCorecursive (HHFree' h i f) where
  hhembed h = case h of
    HHDoneF ia -> HHDone ia
    HHMoreF hfra -> HHMore hfra 

---

newtype FA f a b = FA { unFA :: FA' f a b }

type FA' f = HHFree' Procompose (->) (Coyoneda f)

newtype LmapFA a0 b0 f b y = LmapFA { unLmapFA :: (b ~ b0) => FA' f a0 y }

instance Profunctor (FA p) where
  rmap f (FA t) = FA case t of
    HHDone i -> HHDone (f . i)
    HHMore (Procompose (Coyoneda r s w) t) -> HHMore (Procompose (Coyoneda r (f . s) w) t)
  lmap :: forall a b y. (a -> b) -> FA p b y -> FA p a y
  lmap g (FA t) = FA (unLmapFA (hhcata alg t)) where
    alg :: HHAlgebra (HHFreeF Procompose (->) (Coyoneda p)) (LmapFA a b p)
    alg (HHDoneF i) = LmapFA (HHDone (i . g))
    alg (HHMoreF (Procompose y (LmapFA t))) = LmapFA (HHMore (Procompose y t))

      {-
  lmap :: forall a b y. (a -> b) -> FA p b y -> FA p a y
  lmap g (FA t) = FA (go t) where
    go :: forall x. FA' p b x -> FA' p a x
    go (HHDone i) = HHDone (i . g)
    go (HHMore (Procompose y t)) = HHMore (Procompose y (go t))
    -}