You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

jsalvatier comments on No coinductive datatype of integers - Less Wrong Discussion

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.

Article Navigation

Comments (138)

Comments (138)

You are viewing a single comment's thread.

Comment author: jsalvatier 04 May 2011 06:48:29PM *  0 points [-]

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).

Comment author: cousin_it 04 May 2011 08:52:16PM *  4 points [-]

Right. In fact, this phrase from Harper's blog was one of the inspirations for my post:

In Carollian style there are types called naturals and lists, but that’s only what they’re called, it’s not what they are.

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.

Comment author: jsalvatier 04 May 2011 11:35:22PM 1 point [-]

Thanks for correcting me :) I imagine there's a lot of Harper I don't understand correctly.

Powered by Reddit Powered by Reddit