Recursion on TypeNats

[Carter Schonwald]

you want the following (which doesnt require undediable instances)

data Nat = Z | S Nat

type family U (x :: Nat) where
  U  0 = Z
  U n = S (U (n-1))

this lets you convert type lits into your own peanos or whatever

hat tip to richard eisenburg for showing me this trick on the mailing list
a while ago


On Sat, 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20141025/73fec7d0/attachment.html>