Created
January 4, 2024 00:36
-
-
Save yangzhixuan/1119345963100b9638b13febcd4a9711 to your computer and use it in GitHub Desktop.
Mixing two arbitrary functor algebras (using codensity lifting along the fibration of functor algebras)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE ImpredicativeTypes #-} | |
| {-# LANGUAGE GADTs #-} | |
| data Free f a where | |
| V :: a -> Free f a | |
| O :: f (Free f a) -> Free f a | |
| fold :: Functor f => (a -> c) -> (f c -> c) -> Free f a -> c | |
| fold k alg (V a) = k a | |
| fold k alg (O o) = alg (fmap (fold k alg) o) | |
| type Translation f g = forall x. f x -> Free g x | |
| applyT :: Functor g => Translation f g -> (g b -> b) -> (f b -> b) | |
| applyT t a2 = \fop -> fold id a2 (t fop) | |
| -- An arbitrary f-algebra `a1 :: f a -> a` and an arbitrary g-algebra `a2 :: g b -> b` | |
| -- can be combined into an algebra of both f and g. | |
| -- | |
| -- (This is a very special case of Shin-ya Katsumata et al.'s (single) codensity lifting | |
| -- applied to the fibration of algebras of functors over the category of functors, the | |
| -- monad `g + -` on the category of functors, and the parameter of initial | |
| -- functor 0 and (a2 : g b -> b) in (g+0)-Alg.) | |
| type Mix f a g b = Translation f g -> (a -> b) -> b | |
| mixalg1 :: (Functor f, Functor g) => (g b -> b) -> f (Mix f a g b) -> Mix f a g b | |
| mixalg1 a2 fop = \t h -> fold id a2 (t (fmap (\m -> m t h) fop)) | |
| mixalg2 :: (Functor f, Functor g) => (g b -> b) -> g (Mix f a g b) -> Mix f a g b | |
| mixalg2 a2 gop = \t h -> a2 (fmap (\m -> m t h) gop) | |
| -- If `Mix f a g b` is refined to be the type: | |
| -- (t : Translation f g) -> {h : a -> b | h is an f-homomorphism from `a1` to `applyT t a2`} -> b | |
| -- then in1 is a `f`-algebra homomorphism from `a1` to `mixalg1 a2` | |
| in1 :: a -> Mix f a g b | |
| in1 a = \ t h -> h a | |
| -- `in2` is always a `g`-algebra homomorphism from `a2` to `mixalg2 a2` | |
| in2 :: b -> Mix f a g b | |
| in2 b = \ _ _ -> b |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment