Recursion on TypeNats

[Barney Hilken]

> No, there's not another way to do this with built-in Nats, and there probably won't ever be.

I do hope you're wrong.

> There are two advantages to the built-in Nats over hand-rolled ones: 1) Better syntax / error messages. 2) Built-in Nats are much more efficient than hand-rolled ones, because the hand-rolled ones are unary and take up space linear in the value of the number. If you re-hash your proposal for a Successor constructor down to the term level, it looks juts like (n+k)-patterns, which were discarded as a bad idea.

(n+k) patterns are clearly a bad idea on integers, because the integers don't have the inductive structure, but they're a good idea on natural numbers, which is why they were in the language originally.

> The reason that the type-level numbers are natural numbers and not integers is because natural numbers have a simpler theory to solve for. I'm personally hoping for proper type-level integers at some point, and the type-checker plugins approach may make that a reality sooner than later.

Type-level integers could well be useful, but they shouldn't replace type-level naturals, because they have completely different uses. At the value level, you can fudge the differences, because you can always return bottom, but at the type level you have to take correctness much more seriously if your type system is to be any use at all.

The fact that Carter (and I) are forced to define hand-rolled nats on top of the built in ones demonstrates a clear need for this feature. It seems to me a valuable extension, whether the syntax uses Successor or (n+k). Why can't we combine the advantages of built-in Nats and hand-rolled ones?

Barney.