= 27d567bc2d48d9f40e9ccc20ea370b15)
jsalvatier comments on No coinductive datatype of integers - Less Wrong Discussion
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)
After learning a bit more about inductive and coinductive types from Robert Harper's (which I found more lucid on the topic than Types and Programming Languages), I don't quite understand why it's important for the datatype to be coinductive. You can clearly encode the integers as inductive types, why doesn't that suffice for 'explaining to a computer what a "terminating computation" is'? Are computers 'naturally coinductive' in some sense?
Actually, since computers are turing complete, perhaps it's more like 'computers are naturally recursively typed' and there is an analogous impossibility theorem for encoding some coinductive type in the same way? Perhaps I just don't understanding enough yet.