Editing Corecursion (section)

==Definition==
{{technical|section|date=November 2010}}
[[Initial and terminal objects|Initial data type]]s can be defined as being the [[least fixpoint]] ([[up to isomorphism]]) of some type equation; the [[isomorphism]] is then given by an [[initial algebra]]. Dually, final (or terminal) data types can be defined as being the [[greatest fixpoint]] of a type equation; the isomorphism is then given by a final [[F-coalgebra|coalgebra]].

If the domain of discourse is the [[category of sets]] and [[total function]]s, then final data types may contain infinite, [[Non-well-founded set theory|non-wellfounded]] values, whereas initial types do not.<ref>Barwise and Moss 1996.</ref><ref>Moss and Danner 1997.</ref> On the other hand, if the domain of discourse is the category of [[complete partial order]]s and [[Scott continuity|continuous functions]], which corresponds roughly to the [[Haskell (programming language)|Haskell]] programming language, then final types coincide with initial types, and the corresponding final coalgebra and initial algebra form an isomorphism.<ref>Smyth and Plotkin 1982.</ref>

Corecursion is then a technique for recursively defining functions whose range (codomain) is a final data type, dual to the way that ordinary [[recursion]] recursively defines functions whose domain is an initial data type.<ref>Gibbons and Hutton 2005.</ref><!--G&H ascribe this definition to Barwise and Moss-->

The discussion below provides several examples in Haskell that distinguish corecursion. Roughly speaking, if one were to port these definitions to the category of sets, they would still be corecursive. This informal usage is consistent with existing textbooks about Haskell.<ref>Doets and van Eijck 2004.</ref> The examples used in this article predate the attempts to define corecursion and explain what it is.