Your argument here is compelling. I have wanted type-level integers from the beginning and saw Nats as just a step toward integers. But, of course, this is silly -- you're right that Nats deserve their own place.
Perhaps make a feature request for this. It may be related to type-level pattern synonyms, as proposed in #8828, comment:2. Richard On Oct 27, 2014, at 10:39 AM, Barney Hilken <b.hil...@ntlworld.com> wrote: >> 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. > > > > _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
