Catamorphisms
From HaskellWiki
m 
m (→Alternate Definitions) 

(3 intermediate revisions by 2 users not shown)  
Line 10:  Line 10:  
== Notation == 
== Notation == 

−  A catamorphism for some Falgebra (X,f) is denoted ( f )F. When the functor F can be determined unambiguously, it is usually written (φ) or cata φ. Due to this choice of notation, a catamorphism is sometimes called a banana and the (.) notation is sometimes referred to as banana brackets. 
+  A catamorphism for some Falgebra (X,f) is denoted ( f )F. When the functor F can be determined unambiguously, it is usually written (φ) or <b>cata φ</b>. Due to this choice of notation, a catamorphism is sometimes called a banana and the (.) notation is sometimes referred to as banana brackets. 
== Haskell Implementation == 
== Haskell Implementation == 

+  <haskell> 

type Algebra f a = f a > a 
type Algebra f a = f a > a 

newtype Mu f = InF { outF :: f (Mu f) } 
newtype Mu f = InF { outF :: f (Mu f) } 

cata :: Functor f => Algebra f a > Mu f > a 
cata :: Functor f => Algebra f a > Mu f > a 

cata f = f . fmap (cata f) . outF 
cata f = f . fmap (cata f) . outF 

−  Alternate Definitions 
+  </haskell> 
+  
+  == Alternate Definitions == 

+  <haskell> 

cata f = hylo f outF 
cata f = hylo f outF 

cata f = para (f . fmap fst) 
cata f = para (f . fmap fst) 

−  Duality 
+  </haskell> 
+  
+  == Duality == 

A catamorphism is the categorical dual of an anamorphism. 
A catamorphism is the categorical dual of an anamorphism. 

Line 30:  Line 31:  
== Laws == 
== Laws == 

−  Rule Haskell 
+  { class="wikitable" style="textalign: center 
−  catacancel cata phi . InF = phi . fmap (cata phi) 
+   
−  catarefl cata InF = id 
+  ! Rule !! Haskell 
−  catafusion f . phi = phi . fmap f => 
+   
−  f . cata phi = cata phi 
+  ! catacancel 
−  catacompose eps :: f :~> g => 
+   <hask>cata phi . InF = phi . fmap (cata phi)</hask> 
+   

+  ! catarefl 

+   <hask>cata InF = id</hask> 

+   

+  ! catafusion 

+   <hask>f . phi = phi . fmap f => 

+  f . cata phi = cata phi</hask> 

+   

+  ! catacompose 

+   <hask>eps :: f :~> g => 

cata phi . cata (In . eps) = 
cata phi . cata (In . eps) = 

−  cata (phi . eps) 
+  cata (phi . eps)</hask> 
−  +  } 

== Examples == 
== Examples == 

The underlying functor for a string of Chars and its fixed point 
The underlying functor for a string of Chars and its fixed point 

+  <haskell> 

data StrF x = Cons Char x  Nil 
data StrF x = Cons Char x  Nil 

type Str = Mu StrF 
type Str = Mu StrF 

Line 48:  Line 50:  
fmap f (Cons a as) = Cons a (f as) 
fmap f (Cons a as) = Cons a (f as) 

fmap f Nil = Nil 
fmap f Nil = Nil 

+  </haskell> 

+  
The length of a string as a catamorphism. 
The length of a string as a catamorphism. 

+  <haskell> 

length :: Str > Int 
length :: Str > Int 

length = cata phi where 
length = cata phi where 

phi (Cons a b) = 1 + b 
phi (Cons a b) = 1 + b 

phi Nil = 0 
phi Nil = 0 

+  </haskell> 

+  
The underlying functor for the natural numbers. 
The underlying functor for the natural numbers. 

+  <haskell> 

data NatF a = S a  Z deriving (Eq,Show) 
data NatF a = S a  Z deriving (Eq,Show) 

type Nat = Mu NatF 
type Nat = Mu NatF 

Line 59:  Line 67:  
fmap f Z = Z 
fmap f Z = Z 

fmap f (S z) = S (f z) 
fmap f (S z) = S (f z) 

+  </haskell> 

+  
Addition as a catamorphism. 
Addition as a catamorphism. 

+  <haskell> 

plus :: Nat > Nat > Nat 
plus :: Nat > Nat > Nat 

plus n = cata phi where 
plus n = cata phi where 

phi Z = n 
phi Z = n 

phi (S m) = s m 
phi (S m) = s m 

+  </haskell> 

+  
Multiplication as a catamorphism 
Multiplication as a catamorphism 

+  <haskell> 

times :: Nat > Nat > Nat 
times :: Nat > Nat > Nat 

times n = cata phi where 
times n = cata phi where 

Line 73:  Line 87:  
s :: Nat > Nat 
s :: Nat > Nat 

s = InF . S 
s = InF . S 

+  </haskell> 

Line 78:  Line 93:  
A somewhat less common variation on the theme of a catamorphism is a catamorphism as a recursion scheme a la Mendler, which removes the dependency on the underlying type being an instance of Haskell's Functor typeclass [6]. 
A somewhat less common variation on the theme of a catamorphism is a catamorphism as a recursion scheme a la Mendler, which removes the dependency on the underlying type being an instance of Haskell's Functor typeclass [6]. 

+  <haskell> 

type MendlerAlgebra f c = forall a. (a > c) > f a > c [8] 
type MendlerAlgebra f c = forall a. (a > c) > f a > c [8] 

mcata :: MendlerAlgebra f c > Mu f > c 
mcata :: MendlerAlgebra f c > Mu f > c 

mcata phi = phi (mcata phi) . outF 
mcata phi = phi (mcata phi) . outF 

+  </haskell> 

From which we can derive the original notion of a catamorphism: 
From which we can derive the original notion of a catamorphism: 

+  <haskell> 

cata :: Functor f => Algebra f c > Mu f > c 
cata :: Functor f => Algebra f c > Mu f > c 

cata phi = mcata (\f > phi . fmap f) 
cata phi = mcata (\f > phi . fmap f) 

+  </haskell> 

This can be seen to be equivalent to the original definition of cata by expanding the definition of mcata. 
This can be seen to be equivalent to the original definition of cata by expanding the definition of mcata. 

Line 95:  Line 114:  
In type theoretic terms, the contravariant 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. 
In type theoretic terms, the contravariant 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. 

+  <haskell> 

data CoYoneda f a = forall b. CoYoneda (b > a) (f b) 
data CoYoneda f a = forall b. CoYoneda (b > a) (f b) 

toCoYoneda :: f a > CoYoneda f a 
toCoYoneda :: f a > CoYoneda f a 

Line 100:  Line 120:  
fromCoYoneda :: Functor f => CoYoneda f a > f a 
fromCoYoneda :: Functor f => CoYoneda f a > f a 

fromCoYoneda (CoYoneda f v) = fmap f v 
fromCoYoneda (CoYoneda f v) = fmap f v 

+  </haskell> 

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. 
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. 
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. 

+  <haskell> 

Algebra (CoYoneda f) a 
Algebra (CoYoneda f) a 

= (by definition) CoYoneda f a > a 
= (by definition) CoYoneda f a > a 

Line 109:  Line 131:  
~ (by currying) forall b. (b > a) > f b > a 
~ (by currying) forall b. (b > a) > f b > a 

= (by definition) MendlerAlgebra f a 
= (by definition) MendlerAlgebra f a 

−  Generalized Catamorphisms 
+  </haskell> 
+  
+  == Generalized Catamorphisms == 

Most more advanced recursion schemes for folding structures, such as paramorphisms and zygomorphisms can be seen in a common framework as "generalized" catamorphisms[7]. A generalized catamorphism is defined in terms of an FWalgebra and a distributive law for the comonad W over the functor F which preserves the structure of the comonad W. 
Most more advanced recursion schemes for folding structures, such as paramorphisms and zygomorphisms can be seen in a common framework as "generalized" catamorphisms[7]. A generalized catamorphism is defined in terms of an FWalgebra and a distributive law for the comonad W over the functor F which preserves the structure of the comonad W. 

+  <haskell> 

type Dist f w = forall a. f (w a) > w (f a) 
type Dist f w = forall a. f (w a) > w (f a) 

type FWAlgebra f w a = f (w a) > a 
type FWAlgebra f w a = f (w a) > a 

Line 118:  Line 141:  
g_cata k g = extract . c where 
g_cata k g = extract . c where 

c = liftW g . k . fmap (duplicate . c) . outF 
c = liftW g . k . fmap (duplicate . c) . outF 

+  </haskell> 

However, a generalized catamorphism can be shown to add no more expressive power to the concept of a catamorphism. That said the separation of a number of the "book keeping" concerns by isolating them in a reusable distributive law can ease the development of FWalgebras. 
However, a generalized catamorphism can be shown to add no more expressive power to the concept of a catamorphism. That said the separation of a number of the "book keeping" concerns by isolating them in a reusable distributive law can ease the development of FWalgebras. 

We can transform an FWalgebra into an Falgebra by including the comonad in the carrier for the algebra and then extracting after we perform this somewhat more stylized catamorphism: 
We can transform an FWalgebra into an Falgebra by including the comonad in the carrier for the algebra and then extracting after we perform this somewhat more stylized catamorphism: 

+  <haskell> 

lowerAlgebra :: (Functor f, Comonad w) => 
lowerAlgebra :: (Functor f, Comonad w) => 

Dist f w > FWAlgebra f w a > Algebra f (w a) 
Dist f w > FWAlgebra f w a > Algebra f (w a) 

Line 128:  Line 153:  
Dist f w > FWAlgebra f w a > Mu f > a 
Dist f w > FWAlgebra f w a > Mu f > a 

g_cata k phi = extract . cata (lowerGAlgebra k phi) 
g_cata k phi = extract . cata (lowerGAlgebra k phi) 

+  </haskell> 

and we can trivially transform an Algebra into an FWAlgebra by mapping the counit of the comonad over F. Then using the trivial identity functor, we can represent every catamorphism as a generalizedcatamorphism. 
and we can trivially transform an Algebra into an FWAlgebra by mapping the counit of the comonad over F. Then using the trivial identity functor, we can represent every catamorphism as a generalizedcatamorphism. 

+  <haskell> 

liftAlgebra :: (Functor f, Comonad w) => 
liftAlgebra :: (Functor f, Comonad w) => 

Algebra f a > FWAlgebra f w a 
Algebra f a > FWAlgebra f w a 

Line 138:  Line 165:  
cata :: Functor f => Algebra f a > Mu f > a 
cata :: Functor f => Algebra f a > Mu f > a 

cata f = g_cata (Identity . fmap runIdentity) (liftAlgebra f) 
cata f = g_cata (Identity . fmap runIdentity) (liftAlgebra f) 

+  </haskell> 

Between these two definitions we can see that a generalized catamorphism does not increase the scope of a catamorphism to encompass any more operations, it simply further stylizes the pattern of recursion. 
Between these two definitions we can see that a generalized catamorphism does not increase the scope of a catamorphism to encompass any more operations, it simply further stylizes the pattern of recursion. 

Revision as of 00:44, 31 July 2011
Contents 
1 Folding data structures
An overview and derivation of the categorytheoretic notion of a catamorphism as a recursion scheme, and an exploration of common variations on the theme.
2 Description
Catamorphisms are generalizations of the concept of a fold in functional programming. A catamorphism deconstructs a data structure with an Falgebra for its underlying functor.
3 History
The name catamorphism appears to have been chosen by Lambert Meertens [1]. The category theoretic machinery behind these was resolved by Grant Malcolm [2][3], and they were popularized by Meijer, Fokkinga and Paterson[4][5]. The name comes from the Greek 'κατα' meaning "downward or according to". A useful mnemonic is to think of a catastrophe destroying something.
4 Notation
A catamorphism for some Falgebra (X,f) is denoted ( f )F. When the functor F can be determined unambiguously, it is usually written (φ) or cata φ. Due to this choice of notation, a catamorphism is sometimes called a banana and the (.) notation is sometimes referred to as banana brackets.
5 Haskell Implementation
type Algebra f a = f a > a newtype Mu f = InF { outF :: f (Mu f) } cata :: Functor f => Algebra f a > Mu f > a cata f = f . fmap (cata f) . outF
6 Alternate Definitions
cata f = hylo f outF cata f = para (f . fmap fst)
7 Duality
A catamorphism is the categorical dual of an anamorphism.
8 Derivation
If (μF,inF) is the initial Falgebra for some endofunctor F and (X,φ) is an Falgebra, then there is a unique Falgebra homomorphism from (μF,inF) to (X,φ), which we denote ( φ )F.
That is to say, the following diagram commutes:
9 Laws
Rule  Haskell 

catacancel  cata phi . InF = phi . fmap (cata phi) 
catarefl  cata InF = id 
catafusion  f . phi = phi . fmap f => f . cata phi = cata phi 
catacompose  eps :: f :~> g => cata phi . cata (In . eps) = cata (phi . eps) 
10 Examples
The underlying functor for a string of Chars and its fixed point
data StrF x = Cons Char x  Nil type Str = Mu StrF instance Functor StrF where fmap f (Cons a as) = Cons a (f as) fmap f Nil = Nil
The length of a string as a catamorphism.
length :: Str > Int length = cata phi where phi (Cons a b) = 1 + b phi Nil = 0
The underlying functor for the natural numbers.
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)
Addition as a catamorphism.
plus :: Nat > Nat > Nat plus n = cata phi where phi Z = n phi (S m) = s m
Multiplication as a catamorphism
times :: Nat > Nat > Nat times n = cata phi where phi Z = z phi (S m) = plus n m z :: Nat z = InF Z s :: Nat > Nat s = InF . S
11 Mendler Style
A somewhat less common variation on the theme of a catamorphism is a catamorphism as a recursion scheme a la Mendler, which removes the dependency on the underlying type being an instance of Haskell's Functor typeclass [6].
type MendlerAlgebra f c = forall a. (a > c) > f a > c [8] mcata :: MendlerAlgebra f c > Mu f > c mcata phi = phi (mcata phi) . outF
From which we can derive the original notion of a catamorphism:
cata :: Functor f => Algebra f c > Mu f > c cata phi = mcata (\f > phi . fmap f)
This can be seen to be equivalent to the original definition of cata by expanding the definition of mcata.
The principal advantage of using Mendlerstyle is it is independent of the definition of the Functor definition for f.
12 Mendler and the Contravariant Yoneda Lemma
The definition of a Mendlerstyle algebra above can be seen as the application of the contravariant version of the Yoneda lemma to the functor in question.
In type theoretic terms, the contravariant 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
13 Generalized Catamorphisms
Most more advanced recursion schemes for folding structures, such as paramorphisms and zygomorphisms can be seen in a common framework as "generalized" catamorphisms[7]. A generalized catamorphism is defined in terms of an FWalgebra and a distributive law for the comonad W over the functor F which preserves the structure of the comonad W.
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
However, a generalized catamorphism can be shown to add no more expressive power to the concept of a catamorphism. That said the separation of a number of the "book keeping" concerns by isolating them in a reusable distributive law can ease the development of FWalgebras.
We can transform an FWalgebra into an Falgebra by including the comonad in the carrier for the algebra and then extracting after we perform this somewhat more stylized catamorphism:
lowerAlgebra :: (Functor f, Comonad w) => Dist f w > FWAlgebra f w a > Algebra f (w a) lowerAlgebra k phi = liftW phi . k . fmap duplicate g_cata :: (Functor f, Comonad w) => Dist f w > FWAlgebra f w a > Mu f > a g_cata k phi = extract . cata (lowerGAlgebra k phi)
and we can trivially transform an Algebra into an FWAlgebra by mapping the counit of the comonad over F. Then using the trivial identity functor, we can represent every catamorphism as a generalizedcatamorphism.
liftAlgebra :: (Functor f, Comonad w) => Algebra f a > FWAlgebra f w a liftAlgebra phi = phi . fmap extract cata :: Functor f => Algebra f a > Mu f > a cata f = g_cata (Identity . fmap runIdentity) (liftAlgebra f)
Between these two definitions we can see that a generalized catamorphism does not increase the scope of a catamorphism to encompass any more operations, it simply further stylizes the pattern of recursion.
14 References
 L. Meertens. First Steps towards the theory of Rose Trees. Draft Report, CWI, Amsterdam, 1987.
 G. Malcolm. PhD. Thesis. University of Gronigen, 1990.
 G. Malcolm. Data structures and program transformation. Science of Computer Programming, 14:255279, 1990.
 E. Meijer. Calculating Compilers, Ph.D Thesis, Utrecht State University, 1992.
 E. Meijer, M. Fokkinga, R. Paterson, Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, 5th ACM Conference on Functional Programming Languages and Computer Architecture.
 T. Uustalu, V. Vene. Coding Recursion a la Mendler. Proceedings 2nd Workshop on Generic Programming, WGP'2000, Ponte de Lima, Portugal, 6 July 2000
 T. Uustalu, V. Vene, A. Pardo. Recursion schemes from Comonads. Nordic Journal of Computing. Volume 8 , Issue 3 (Fall 2001). 366390, 2001 ISSN:12366064
 E. Kmett. Catamorphism. The Comonad.Reader, 2008.