Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# yuga/Fix.hs

Created May 12, 2015
This file contains 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 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
to join this conversation on GitHub. Already have an account? Sign in to comment