Skip to content

Instantly share code, notes, and snippets.

@Lysxia Lysxia/HHFree.hs
Last active Sep 16, 2019

Embed
What would you like to do?
doubly-indexed `Free` profunctor, `lmap` using doubly-indexed recursion-schemes
{-# 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))
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.