Pithy summary for codata (Where a comonad is a 'type for input impurity')

Question

In terms of pithy summaries - this description of Comonads seems to win - describing them as a 'type for input impurity'.

What is an equivalent pithy (one-sentence) description for codata?

Translucid

Answer 1

"Codata are types inhabited by values that may be infinite"

This contrasts with "data" which is inhabited only by finite values. For example, if we take the "data" definition of lists, it is inhabited by lists of finite length (as in ML), but if we take the "codata" definition it is inhabited also by infinite length lists (as in Haskell, e.g. x = 1 : x).

Comonads and codata are not necessarily related (although perhaps some might think so due to Kieburtz' paper Comonads and codata in Haskell).

Perihelion

Would you agree with the statement "In LISP code is data, and LISP code is codata?" – Translucid

No. LISP code is data (it is a list/S-expression), but this is not the same "data" as in "data/codata". I will put an example in the answer to try to make things more clear. – Perihelion

Ok - just so I'm clear - if I had a function in Clojure that returned a lazy list of the fibconacci series up to infinity - then the result of that function (the lazy list) would be codata, but the function itself would not. – Translucid

As far as I am aware, Clojure doesn't have a static type system (theory) so any description of things as being "codata" will be an informal/operational one. With this in mind then, an infinite list value can be thought of as the value of a codata type. Whilst the function here is finite, am I right in thinking that a Clojure/LISP program could generate an infinite code tree via macros? In which case the "type" of code is also codata, since it contains infinite syntax trees. Please clarify and maybe we can agree on a definition. – Perihelion