<span id="mailbox-conversation"><div>because you haven't helped write a patch change it yet :) </div></span><div class="mailbox_signature">

<br>-Carter</div>

<br><br><div class="gmail_quote"><p>On Sat, Oct 25, 2014 at 9:53 AM, Barney Hilken <span dir="ltr"><<a href="mailto:b.hilken@ntlworld.com" target="_blank">b.hilken@ntlworld.com</a>></span> wrote:<br></p><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><p>If you define your own type level naturals by promoting

<br><br>data Nat = Z | S Nat

<br><br>you can define data families recursively, for example

<br><br>data family Power :: Nat -> * -> *

<br>data instance Power Z a = PowerZ

<br>data instance Power (S n) a = PowerS a (Power n a)

<br><br>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

<br><br>type family Power (n :: Nat) a where

<br>      Power 0 a = ()

<br>      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.

<br><br>_______________________________________________

<br>Glasgow-haskell-users mailing list

<br>Glasgow-haskell-users@haskell.org

<br>http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

<br></p></blockquote></div><br>