Skip to content

Instantly share code, notes, and snippets.

@yuga
Created May 12, 2015 23:37
Show Gist options
  • Save yuga/ac639f542b64cd9cddf6 to your computer and use it in GitHub Desktop.
Save yuga/ac639f542b64cd9cddf6 to your computer and use it in GitHub Desktop.
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Fix where
-- Definitions:
--
-- If (μF,inF) is the initial F-algebra for some endofunctor F
-- and (X,φ) is an F-algebra, then there is an unique F-algebra
-- homomorphism from (μF,inF) to (X,φ), which is denoted (|φ|)F.
--
-- inF
-- FμF -----> μF <= initial F-algebra cata <- ana ->
-- | | | ^
-- F(|φ|) | | (|φ|) <= catamorphism v |
-- | | -> <-
-- v v
-- FX -----> X <= F-algebra
-- φ
--
-- Laws:
--
-- Rule: Haskell
-- cata-cancel cata phi . InF = phi . fmap (cata phi)
-- cata-refl cata InF = id
-- cata-fusion f . phi = phi . fmap f => f . cata phi = cata phi
-- cata-compose eps :: f :~> g => cata phi . cata (In . eps) = cata (phi . eps)
--
type Algebra f a = f a -> a
newtype Mu f = InF { outF :: f (Mu f) } -- μF ≅ FμF, so Mu f = f (Mu f) expresses it.
instance Show (f (Mu f)) => Show (Mu f) where
show x = "(" ++ show (outF x) ++ ")"
cata :: Functor f => Algebra f a -> Mu f -> a -- Algebra f a is the type of φ. For lifting φ, f must be a Functor.
cata f = f . fmap (cata f) . outF -- (of course, f is an endofunctor according to the presupposition)
-- cata f = hylo f outF
-- cata f = para (f . fmap fst)
type CoAlgebra f a = a -> f a
ana :: Functor f => CoAlgebra f a -> a -> Mu f
ana f = InF . fmap (ana f) . f
hylo :: Functor f => Algebra f b -> CoAlgebra f a -> (a -> b)
hylo phi psi = cata phi . ana psi
-------------------------------------------------------------------------------------
data StrF x = Cons Char x | Nil
type Str = Mu StrF
nil :: Str
nil = InF Nil
cons :: Char -> Str -> Str
cons x xs = InF (Cons x xs)
instance Functor StrF where
fmap f (Cons a as) = Cons a (f as)
fmap _f Nil = Nil
length :: Str -> Int
length = cata phi where
phi (Cons _a b) = 1 + b -- phi :: Mu StrF -> Int
phi Nil = 0
-------------------------------------------------------------------------------------
data NatF a = S a | Z deriving (Eq,Show)
type Nat = Mu NatF
instance Functor NatF where
fmap _f Z = Z
fmap f (S z') = S (f z')
z :: Nat
z = InF Z
s :: Nat -> Nat
s = InF . S
plus :: Nat -> Nat -> Nat
plus n = cata phi where
phi Z = n
phi (S m) = s m
times :: Nat -> Nat -> Nat
times n = cata phi where
phi Z = z
phi (S m) = plus n m
-------------------------------------------------------------------------------------
-- Mendler Style
type MendlerAlgebra f c = forall a. (a -> c) -> f a -> c
mcata :: MendlerAlgebra f c -> Mu f -> c
mcata phi = phi (mcata phi) . outF
-- mcata phi
-- = {- definition -}
-- phi (mcata phi) . outF
-- = phi (phi (mcata phi) . outF) . outF
cata' :: Functor f => Algebra f c -> Mu f -> c
cata' phi = mcata (\f -> phi . fmap f)
-------------------------------------------------------------------------------------
-- Mendler and the Yoneda Lemma
-- The definition of a Mendler-sytle algebra above can be seen as the
-- application of Yoneda lemma to the functior in question.
--
-- In type theoretic terms, the Yoneda lemma states that there is an
-- isomorphism between (f a) and ∃b. (b -> a, f b), which can be witnessed
-- by the following definitions.
data CoYoneda f a = forall b. CoYoneda (b -> a) (f b)
toCoYoneda :: f a -> CoYoneda f a
toCoYoneda = CoYoneda id
fromCoYoneda :: Functor f => CoYoneda f a -> f a
fromCoYoneda (CoYoneda f v) = fmap f v
-- Note that in Haskell using an existential requires the use of data, so
-- there is an extra bottom that can inhabit this type that prevents this
-- from being a true isomorphism.
--
-- However, when used in the context of a (CoYoneda f)-Algebra we can
-- rewrite this to use universal quantification because the functor f only
-- occurs in negative position, eliminating the spurious bottom.
--
-- Algebra (CoYoneda f) a
-- = {- by definition -}
-- CoYoneda f a -> a
-- ~ {- by definition -}
-- (exists b. (b -> a, f b)) -> a
-- ~ {- lifting the existential -}
-- forall b. (b -> a, f b) -> a
-- ~ {- by currying -}
-- forall b. (b -> a) -> f b -> a
-- = {- by definition -}
-- MendlerAlgebra f a
-------------------------------------------------------------------------------------
-- Generalized Catamorphisms
-- Most more advanced recursion schemas for foling structures, such as
-- paramorphisms and zygomorphisms can be seen in a common framework as
-- "generalized" catamorphisms. A generalized catamorphism is defined in
-- terms of an F-W-algebra and a distributive law for the comonad W over
-- the functor F which preserves the structure of the comonad W.
class Functor w => Comonad w where
extract :: w a -> a
duplicate :: w a -> w (w a)
duplicate = extend id
extend :: (w a -> b) -> w a -> w b
extend f = fmap f . duplicate
liftW :: Comonad w => (a -> b) -> w a -> w b
liftW f = extend (f . extract)
type Dist f w = forall a. f (w a) -> w (f a)
type FWAlgebra f w a = f (w a) -> a
g_cata :: (Functor f, Comonad w)
=> Dist f w -> FWAlgebra f w a -> Mu f -> a
g_cata k g = extract . c where
c = liftW g . k . fmap (duplicate . c) . outF
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment