The above layman's description can be stated more formally in category theory: the anamorphism of a coinductive type denotes the assignment of a coalgebra to its unique morphism to the final coalgebra of an endofunctor.
In functional programming, an anamorphism is a generalization of the concept of unfolds on coinductive lists.
The data type in question is defined as the greatest fixed point ν X .
Thus, one can define functions from a type A _into_ a coinductive datatype by specifying a coalgebra structure a on A.
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: We can now implement quite general functions using ana, for example a countdown: 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.
An anamorphism can be defined for any recursive type, according to a generic pattern, generalizing the second version of ana for lists.
To prove this, we can implement both using our generic unfold, ana, using a simple recursive routine: 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.