MagnetoHydroDynamics comments on No coinductive datatype of integers - Less Wrong

4 Post author: cousin_it 04 May 2011 04:37PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (138)

You are viewing a single comment's thread.

Comment author: [deleted] 07 January 2015 02:46:41PM 0 points [-]

Encoding is not definition. While it is true that we cannot decide the integer value of "1111..." as you describe, the reason behind it is obvious: you are trying to use an inductive algorithm on a co-inductive data structure.

Clearly, your proposed bits-to-ints encoding scheme is isomorphic to lists of unit, and it so happens that there is a one-to-one mapping between list-of-unit and inductively defined natural numbers, exactly so long as the lists in question are inductive and thefore finite. This isomorphism is made up of length :: list unit -> int and repeat unit :: int -> list unit, according to their usual definition. Proof of that this is isomorphic is left as an exercise to the reader.