Skip to content

Instantly share code, notes, and snippets.

@xgrommx

xgrommx/hiso.hs

Created September 11, 2019 00:31
Show Gist options
  • Save xgrommx/e035fe6c478e56a1aad9ebb3c0506594 to your computer and use it in GitHub Desktop.
Save xgrommx/e035fe6c478e56a1aad9ebb3c0506594 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment