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, 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 sou ...
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 (competition), the last or championship round of a sporting competition, match, game, or other contest which decides a winner for an event
** Another term for playoffs, describing a sequence of con ...
''F''-coalgebra for some endofunctor
In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) are associated to topological spaces, and ...
''F'' of some category
Category, plural categories, may refer to:
Philosophy and general uses
*Categorization, categories in cognitive science, information science and generally
* Category of being
* ''Categories'' (Aristotle)
* Category (Kant)
* Categories (Peirce) ...
into itself.
Thus, ''fin'' is a morphism 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 structure-preserving map between two algebraic structures of the same type (such as two groups, two rings, or two vector spaces). The word ''homomorphism'' comes from the Ancient Greek language: () meaning "same" ...
''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