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