In imperative code I would write it like: odd := {hd: 1} even := {hd: 0, tail: odd} odd.tail := even blink x := x ? odd : even I guess the cof

In imperative code I would write it like: odd := {hd: 1} even := {hd: 0, tail: odd} odd.tail := even blink x := x ? odd : even I guess the cofixpoint does that loop tying sort of like this? fix({odd, even} => { odd: {hd: 1, tail: even}, even: {hd: 0, tail: odd} }) Is there something like a co-Y combinator to do this in pure languages? Is the productivity condition sort of like the dual of the positivity restriction on inductive types?