= 27d567bc2d48d9f40e9ccc20ea370b15)
jsalvatier comments on No coinductive datatype of integers - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (138)
As for your problem, Robert Harper (posts as 'Abstract Type') frequently notes that you cannot define the natural numbers or any inductive type in haskell because it is lazy so bottom (non-termination) is a member of all types and therefore requires coinductive types (for example see also the reddit discussion).
Right. In fact, this phrase from Harper's blog was one of the inspirations for my post:
ETA: it seems you slightly misunderstood Harper's point. The problem with defining "data Nat = Zero | Succ Nat" is not that bottom is in Nat, but rather that laziness allows you to write the circular definition "omega = Succ omega" (note that pattern-matching on omega doesn't hang), which is similar to the unary example in my post.
Thanks for correcting me :) I imagine there's a lot of Harper I don't understand correctly.