This is a corecursive algorithm, because with each iteration it calls itself on data that is greater then what it had before:
iterate f x = x : iterate f (f x)
It is similar to tail recursion accumulator style, but its accumulator is implicit instead of being passed as an argument. And it would be infinite if it weren't for lazyness. So is codata just the result of a value constructor in WHNF, kind of like (a, thunk)
? Or is codata rather a mathematical term from category theory, which hasn't a useful representation in the programming domain?
Follow-up question: Is value recursion just a synonym for corecursion?
I think answering your questions requires a lot of explanation, so here's a big long answer with specific answers to your questions at the end.
Data and codata have formal mathematical definitions in terms of category theory, so it's not just a matter of how they are used in a program (i.e., not just the "application context" you mentioned in the comments). It may seem this way in Haskell because the language's features (specifically, non-termination and laziness) end up blurring the distinction, so in Haskell, all data is also codata and vice versa, but it doesn't have to be this way, and there are languages that make the distinction clearer.
Both data and codata do have useful representations in the programming domain, and those representations give rise to natural relationships to recursion and corecursion.
It's quite hard to explain these formal definitions and representations without quickly getting technical, but roughly speaking, a data type for, say, a list of integers, is a type
L
together with a constructor function:that is somehow "universal" in that it can fully represent any such construction. (Here, you want to interpret the LHS type
Either () (Int, L)
to mean that a listL
is either the empty listLeft ()
or a pairRight (h, t)
consisting of the head elementh :: Int
and a tail listt :: L
.)To start with a counterexample,
L = Bool
is not the data type we're looking for, because even though you could write:to "construct" a
Bool
, this can't fully represent any such construction. For example, the two constructions:give the same
Bool
value, even though they used different integers, so thisBool
value is insufficient to fully represent the construction.In contrast, the type
[Int]
is an appropriate data type because the (almost trivial) constructor function:fully represents any possible construction, creating a unique value for each one. So, it's somehow the "natural" construction for the type signature
Either () (Int, L) -> L
.Similarly, a codata type for a list of integers would be a type
L
together with a destructor function:that is somehow "universal" in the sense that it can represent any possible destruction.
Again, starting with a counterexample, a pair
(Int, Int)
is not the codata type we're looking for. For example, with the destructor:we can represent the destruction:
but we can't represent the destruction:
On the other hand, in Haskell, the list type
[Int]
is an appropriate codata type for a list of integers, because the destructor:can represent any possible destruction (including both finite or infinite destructions, thanks to Haskell's lazy lists).
(As evidence that this isn't all hand-waving and in case you want to relate it back to the formal math, in technical category theory terms, the above is equivalent to saying that the list-like endofunctor:
gives rise to a category whose objects are constructor functions (AKA F-algebras)
1 + Int*A -> A
. A data type associated with F is an initial F-algebra in this category. F also gives rise to another category whose objects are destructor functions (AKA F-coalgebras)A -> 1 + Int*A
. A codata type associated with F is a final F-coalgebra in this category.)In intuitive terms, as suggested by @DanielWagner, a data type is a way of representing any construction of a list-like object, while a codata type is a way of representing any destruction of a list-like object. In languages where data and codata are different, there's a fundamental asymmetry -- a terminating program can only construct a finite list, but it can destruct (the first part of) an infinite list, so data must be finite, but codata can be finite or infinite.
This leads to another complication. In Haskell, we can use
makeL
to construct an infinite list like so:Note that this would not be possible if Haskell didn't allow lazy evaluation of non-terminating programs. Because we can do this, by the formal definition of "data", a Haskell list-of-integer data type must also include infinite lists! That is, Haskell "data" can be infinite.
This probably conflicts with what you might read elsewhere (and even with the intuition that @DanielWagner provided), where "data" is used to refer to finite data structures only. Well, because Haskell is a little weird and because infinite data isn't allowed in other languages where data and codata are distinct, when people talk about "data" and "codata" (even in Haskell) and are interested in drawing a distinction, they may use "data" to refer to finite structures only.
The way recursion and corecursion fit in to this is that the universality properties naturally give us "recursion" to consume data and "corecursion" to produce codata. If
L
is a list-of-integer data type with constructor function:then one way of consuming a list
L
to produce aResult
is to define a (non-recursive) function:Here,
makeResult (Left ())
gives the intended result for an empty list, whilemakeResult (Right (h, t_result))
gives the intended result for a list whose head element ish :: Int
and whose tail would give the resultt_result :: Result
.By universality (i.e., the fact that
makeL
is an initial F-algebra), there exists a unique functionprocess :: L -> Result
that "implements"makeResult
. In practice, it will be implemented recursively:Conversely, if
L
is a list-of-integer codata type with destructor function:then one way of producing a list
L
from aSeed
is to define a (non-recursive) function:Here,
unfoldSeed
should produce aRight (x, nextSeed)
for each desired integer, and produceLeft ()
to terminate the list.By universality (i.e., the fact that
eatL
is a final F-coalebra), there exists a unique functiongenerate :: Seed -> L
that "implements"unfoldSeed
. In practice, it will be implemented corecursively:So, with all that said, here are the answers to your original questions:
Technically,
iterate f
is corecursive because it's the unique codata-producing functionInt -> [Int]
that implements:by means of
generate
as defined above.In Haskell, corecursion that produces codata of type
[a]
relies on laziness. However, strict codata representations are possible. For example, the following codata representation works fine in Strict Haskell and can be safely fully evaluated.The following corecursive function produces a
CoList
value (and I made it finite just for fun -- it's easy to produce infinite codata values, too):So, no, codata isn't just the result of values in WHNF with form
(a, thunk)
or similar and corecursion is not synonymous with value recursion. However, WHNF and thunks provide one possible implementation and are the implementation-level reason that a "standard" Haskell list data type is also a codata type.