Recursion on TypeNats

[Richard Eisenberg]

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

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.

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.

I hope this helps!

Richard

On Oct 25, 2014, at 9:53 AM, Barney Hilken <b.hilken at ntlworld.com> wrote:

> If you define your own type level naturals by promoting
> 
> data Nat = Z | S Nat
> 
> you can define data families recursively, for example
> 
> data family Power :: Nat -> * -> *
> data instance Power Z a = PowerZ
> data instance Power (S n) a = PowerS a (Power n a)
> 
> But if you use the built-in type level Nat, I can find no way to do the same thing. You can define a closed type family
> 
> type family Power (n :: Nat) a where
> 	Power 0 a = ()
> 	Power n a = (a, Power (n-1) a)
> 
> but this isn't the same thing (and requires UndecidableInstances).
> 
> Have I missed something? The user guide page is pretty sparse, and not up to date anyway.
> 
> If not, are there plans to add a "Successor" constructor to Nat? I would have thought this was the main point of using Nat rather than Int.
> 
> Barney.
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users