What is the difference between codata and data?

Question

There is some explanation here. Intuitively I understand how finite data structures differ from infinite data structures like streams. Nevertheless, it's interesting to see other explanations of differences, characteristics, types of codata.

I stumbled upon codata term when reading about streams.

Kori

Answer 1

This answer isn't terribly precise, but I'm going to post it anyway.

---

The real distinction...

... is between data and computations.

Data

The fundamental property of data is that it has a structure. Data can be passed as input and returned as output by computations. The structure of data can be used by computations. However, by itself, data doesn't do anything. Data just is.

Examples of data types are booleans, numbers, strings, algebraic data types (tagged unions), etc. Correspondingly, examples of values are false, 2, "pyon", SOME 2. It makes sense for computations to operate on values: for example, a computation can branch, depending on whether a number is even or odd. However, it doesn't make sense to ask what values can do: the number 2 can't do anything, it just is.

Computations

The fundamental property of computations is that they have behavior. In other words, computations do. However, computations are "too active" to be passed around or stored in variables. For example, you can't store in a variable the very act of printing "Hello, world!" to the screen.

You may object that you can store a reference to a function in a variable. But a reference to a function isn't quite the same thing as the function's behavior when it's executed! The former is data, the latter is a computation.

---

Back to codata...

What exactly is codata? Before giving a proper definition, I'll use an example:

Streams are codata

What exactly is a stream? A stream is a reference¹ to a computation that, when executed, produces either:

• The first element ("head") of a sequence, together with another stream ("tail") that is logically the remainder of the sequence. Or...

• A special symbol ("nil") indicating the end of the sequence.

Streams (and, more generally, codata) are data, because they are references to computations, rather than the computations themselves. However, what makes streams (and, more generally, codata) special is that, when the underlying computations are executed, they may produce other streams (and, more generally, codata).

Now I can finally give a proper definition:

Codata is a reference to a computation that, when executed, may produce (amongst other things) more codata.

---

¹ The correct technical term is "thunk", not "reference".

Bedsore