Terminology like codata in Clojure

Question

Imagine the following function to give an endless lazy fibonacci sequence in Clojure:

(def fib-seq (concat [0 1] ((fn rfib [ab] (lazy-cons (+ ab) (rfib b (+ ab)))) 0 1))) user> (take 20 fib-seq) (0 1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 4181) 

Assuming

• We accept the meaningful definition of codata as "Codata are types populated by values ​​that can be infinite."
• That this example Clojure does not use a static type system (from core.typed), and therefore any description of codata is a "working definition"

My question is: which part of the function above is "codata". Is this an anonymous function? Is this a lazy sequence?

Answer 1

Codata is dual information. You work with data through structural induction, which means that data is always finite. You work with codata through coinduction, which means codata is potentially endless (but not always).

In any case, if you cannot correctly determine the final string toString or equality, this will be codata:

• Is it possible to define toString for infinite threads? No, we need an infinite string.
• Can we always define extensional equality for two infinite flows? No, it will take a long time.

We cannot do higher for flows, because they are infinite. But even the potentially endless causes of unsolvability (i.e., we cannot give a definite yes or no for equality or definitely give a string).

So an endless stream is codata. I think your second question is more interesting, is the codata function?

Lispers says code is data, because functions like S-expressions let you manipulate a program just like data. Obviously, we already have a string representation of Lisp (i.e. source code). We can also take the program and check if it is made up of equal S-expressions (i.e. Compare AST). Data!

But stop thinking about the symbols that represent our code, and instead start thinking about the meaning of our programs. Take the following two functions:

 (fn [a] (+ aa)) (fn [a] (* a 2)) 

They give the same results for all inputs. We don’t care that one uses * , and the other uses + . It is impossible to calculate whether any two arbitrary functions are equal in magnitude unless they work only with the final data (then the equality simply compares the I / O tables). The numbers are infinite, so our example above still does not solve.

Now think about converting a function to a string. Say we had access to the original representation of functions at runtime.

 (defn plus-two [a] (+ a 2)) (defn plus-four [a] (plus-two (plus-two a))) (show-fn plus-four) ; "(plus-two (plus-two a))" 

Now, referential transparency says that we can accept function calls and replace them with function bodies, replacing variables, and the program always gives the same result. Let's do it for plus-two :

 (defn plus-four [a] (+ (+ a 2) 2)) (show-fn plus-four) ; "(+ (+ a 2) 2)" 

Oh ... The result is not the same. We have violated link transparency.

Thus, we also cannot define toString or equality for functions. This is because they are codates!

Here are some resources that I found useful for a better understanding of codata:

• Data, Codata and its implications for equity and serialization
• Codata and Comonads at Haskell
• Data and codes for the Infinity neighborhood
• Some slides from the University of Nottingham

Answer 2

My personal thought is the return value of the lazy-cons call - this is the point at which the type of thing in question can first be called infinate, and thus this is the point that I see that codata'nes starts to start.