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.hil...@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@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users