Anamorphisms in functional programming
InExample: Potentially infinite lists
As an example, the type of potentially infinite lists (with elements of a fixed type ''value'') is given as the fixed point '' alue= ν X . value × X + 1'', i.e. a list consists either of a ''value'' and a further list, or it is empty. A (pseudo-)F value
, where:
alue/code> is isomorphic to F value alue/code>, and thus alue/code> is the fixed point.
(Also note that in Haskell, least and greatest fixed points of functors coincide, therefore inductive lists are the same as coinductive, potentially infinite lists.)
The ''anamorphism'' for lists (then usually known as ''unfold'') would build a (potentially infinite) list from a state value. Typically, the unfold takes a state value x
and a function f
that yields either a pair of a value and a new state, or a singleton to mark the end of the list. The anamorphism would then begin with a first seed, compute whether the list continues or ends, and in case of a nonempty list, prepend the computed value to the recursive call to the anamorphism.
A Haskell definition of an unfold, or anamorphism for lists, called ana
, is as follows:
ana :: (state -> Maybe (value, state)) -> state -> alueana f stateOld = case f stateOld of
Nothing -> []
Just (value, stateNew) -> value : ana f stateNew
We can now implement quite general functions using ''ana'', for example a countdown:
f :: Int -> Maybe (Int, Int)
f current = let oneSmaller = current - 1
in if oneSmaller < 0
then Nothing
else Just (oneSmaller, oneSmaller)
This function will decrement an integer and output it at the same time, until it is negative, at which point it will mark the end of the list. Correspondingly, ana f 3
will compute the list ,1,0/code>.
Anamorphisms on other data structures
An anamorphism can be defined for any recursive type, according to a generic pattern, generalizing the second version of ''ana'' for lists.
For example, the unfold for the tree data structure
data Tree a = Leaf a , Branch (Tree a) a (Tree a)
is as follows
ana :: (b -> Either a (b, a, b)) -> b -> Tree a
ana unspool x = case unspool x of
Left a -> Leaf a
Right (l, x, r) -> Branch (ana unspool l) x (ana unspool r)
To better see the relationship between the recursive type and its anamorphism, note that Tree
and List
can be defined thus:
newtype List a = List
newtype Tree a = Tree
The analogy with ana
appears by renaming b
in its type:
newtype List a = List
anaList :: (list_a -> Maybe (a, list_a)) -> (list_a -> List a)
newtype Tree a = Tree
anaTree :: (tree_a -> Either a (tree_a, a, tree_a)) -> (tree_a -> Tree a)
With these definitions, the argument to the constructor of the type has the same type as the return type of the first argument of ana
, with the recursive mentions of the type replaced with b
.
History
One of the first publications to introduce the notion of an anamorphism in the context of programming was the paper ''Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire'', by Erik Meijer ''et al.'', which was in the context of the Squiggol programming language.
Applications
Functions like zip
and iterate
are examples of anamorphisms. zip
takes a pair of lists, say a','b','c'and ,2,3and returns a list of pairs 'a',1),('b',2),('c',3) Iterate
takes a thing, x, and a function, f, from such things to such things, and returns the infinite list that comes from repeated application of f, i.e. the list , (f x), (f (f x)), (f (f (f x))), ...
zip (a:as) (b:bs) = if (as[]) , , (bs []) -- , , means 'or'
then [(a,b)]
else (a,b):(zip as bs)
iterate f x = x:(iterate f (f x))
To prove this, we can implement both using our generic unfold, ana
, using a simple recursive routine:
zip2 = ana unsp fin
where
fin (as,bs) = (as[]) , , (bs [])
unsp ((a:as), (b:bs)) = ((a,b),(as,bs))
iterate2 f = ana (\a->(a,f a)) (\x->False)
In a language like Haskell, even the abstract functions fold
, unfold
and ana
are merely defined terms, as we have seen from the definitions given above.
Anamorphisms in category theory
In category theory
Category theory is a general theory of mathematical structures and their relations. It was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Category theory ...
, anamorphisms are the categorical dual
In category theory, a branch of mathematics, duality is a correspondence between the properties of a category ''C'' and the dual properties of the opposite category ''C''op. Given a statement regarding the category ''C'', by interchanging the so ...
of catamorphisms (and catamorphisms are the categorical dual of anamorphisms).
That means the following.
Suppose (''A'', ''fin'') is a final
Final, Finals or The Final may refer to:
*Final examination or finals, a test given at the end of a course of study or training
*Final (competition), the last or championship round of a sporting competition, match, game, or other contest which d ...
''F''-coalgebra for some endofunctor ''F'' of some category
Category, plural categories, may refer to:
General uses
*Classification, the general act of allocating things to classes/categories Philosophy
* Category of being
* ''Categories'' (Aristotle)
* Category (Kant)
* Categories (Peirce)
* Category ( ...
into itself.
Thus, ''fin'' is a morphism
In mathematics, a morphism is a concept of category theory that generalizes structure-preserving maps such as homomorphism between algebraic structures, functions from a set to another set, and continuous functions between topological spaces. Al ...
from ''A'' to ''FA'', and since it is assumed to be final we know that whenever (''X'', ''f'') is another ''F''-coalgebra (a morphism ''f'' from ''X'' to ''FX''), there will be a unique homomorphism
In algebra, a homomorphism is a morphism, structure-preserving map (mathematics), map between two algebraic structures of the same type (such as two group (mathematics), groups, two ring (mathematics), rings, or two vector spaces). The word ''homo ...
''h'' from (''X'', ''f'') to (''A'', ''fin''), that is a morphism ''h'' from ''X'' to ''A'' such that ''fin . h = Fh . f''.
Then for each such ''f'' we denote by ana ''f'' that uniquely specified morphism ''h''.
In other words, we have the following defining relationship, given some fixed ''F'', ''A'', and ''fin'' as above:
*
*
Notation
A notation for ana ''f'' found in the literature is