Skip to content

Instantly share code, notes, and snippets.

@Lysxia Lysxia/IFIF.hs
Last active Oct 5, 2019

Embed
What would you like to do?
Initial/final encodings of initial/final (co)algebras
{- Initial/final encodings of initial/final (co)algebras -}
{-# LANGUAGE GADTs, KindSignatures, RankNTypes #-}
module IFIF where
import Data.Kind (Type)
-- Initial encoding of the initial algebra of f
data IEIA (f :: Type -> Type) = IEIA (f (IEIA f))
cata1 :: Functor f => (f a -> a) -> IEIA f -> a
cata1 alg (IEIA t) = alg (fmap (cata1 alg) t)
-- Final encoding of the initial algebra of f (aka. Mu,
-- for example, as can be found in recursion-schemes)
data FEIA (f :: Type -> Type) = FEIA (forall a. (f a -> a) -> a)
cata2 :: (f a -> a) -> FEIA f -> a
cata2 alg (FEIA t) = t alg
-- Initial encoding of the final coalgebra of f (yes, it's the same definition
-- as for the initial algebra in Haskell, because it is a non-strict language)
data IEFC (f :: Type -> Type) = IEFC (f (IEFC f))
ana1 :: Functor f => (a -> f a) -> a -> IEFC f
ana1 coa x = IEFC (fmap (ana1 coa) (coa x))
-- Final encoding of the final coalgebra of f (aka. Nu)
data FEFC (f :: Type -> Type) where
FEFC :: forall f a. (a -> f a) -> a -> FEFC f
ana2 :: (a -> f a) -> a -> FEFC f
ana2 = FEFC
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.