<div dir="ltr">Er, by that I mean the type level nats, not the value-level ones.</div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 15, 2018 at 6:05 PM, Edward Kmett <span dir="ltr"><<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">AFAIK, the existing naturals in base don't have any useful internal structure permitting this sort of thing.<span class="HOEnZb"><font color="#888888"><div><br></div><div>-Edward</div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 15, 2018 at 3:48 PM, Carter Schonwald <span dir="ltr"><<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div dir="auto">Could we provide a pattern synonym for treating naturals as in base already as being peano encoded ?</div><div><div class="m_-3379528805270109257h5"><br><div class="gmail_quote"><div>On Wed, Mar 14, 2018 at 11:51 PM Daniel Cartwright <<a href="mailto:chessai1996@gmail.com" target="_blank">chessai1996@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>I just realised I made a typo. For full clarity, the function 'f' should be:<div><br></div><div>f : D -> N -> R<br></div><div>where</div><div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">D = Data Structure isomorphic to Nat (or any numeric type)</div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">N = Number System Encoding</div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">R = Representation of the numeric type in N.</div></div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><br></div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">For Nats, the simplest example would be:<br><br>f : List () -> Binary -> BinaryEncodingOfNat</div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <span><<a href="mailto:chessai1996@gmail.com" target="_blank">chessai1996@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>I prefer Z and S, but wrote Zero and Succ for clarity (though the likelihood of being at all misunderstood was small).<div><br></div><div>Most recent definitions I see use Z and S.</div></div><div class="m_-3379528805270109257m_2272561796430452094m_5228945314180559036HOEnZb"><div class="m_-3379528805270109257m_2272561796430452094m_5228945314180559036h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 14, 2018 at 9:41 PM, David Feuer <span><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><div>Another problem: different people like to call the constructors by different names. I personally prefer Z and S, because they're short. Some people like Zero and Succ or Suc.<br><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="m_-3379528805270109257m_2272561796430452094m_5228945314180559036m_-6069599319899534346h5">On Mar 14, 2018 9:06 PM, "Daniel Cartwright" <<a href="mailto:chessai1996@gmail.com" target="_blank">chessai1996@gmail.com</a>> wrote:<br type="attribution"></div></div><blockquote class="m_-3379528805270109257m_2272561796430452094m_5228945314180559036m_-6069599319899534346m_-6490028401051854802quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="m_-3379528805270109257m_2272561796430452094m_5228945314180559036m_-6069599319899534346h5"><div>The proposed addition is simple, add the following to base:<br><br>data Nat = Zero | Succ Nat,<div><br></div><div>i.e. Peano Nats - commonly used along with -XDataKinds.</div><div><br><div>I will list the pros/cons I see below:<br><br>Pros:<br>- This datatype is commonly defined throughout many packages throughout Hackage. It would be good for it to have a central location</div><div>- The inductive definition of 'Nat' is useful for correctness (e.g. safeHead :: Vec a (Succ n) -> a; safeHead (Cons a as) = a;)</div><div>- -XDependentHaskell is likely to bring this into base anyway</div><div>- I believe that it might be possible to eliminate a Peano Nat at some stage during/after typechecking. I'm not well-versed in GHC implementation, but something along the lines of possibly converting an inductive Nat to a GMP Integer using some sort of specialisation (Succ -> +1)? Another interesting, related approach (and this is a very top-level view, and perhaps not totally sensical) would be something like a function 'f', that given a data structure and a number system, outputs the representation of that data structure in that number system (Nat is isomorphic to List (), so f : List () -> Binary -> BinaryListRep)</div><div><br></div><div>Cons:</div><div>- -XDependentHaskell will most likely obviate any benefit brought about by type families defined in base that directly involve Nat</div><div>- Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange.</div><div><br></div><div>I am open to criticism concerning the usefulness of the idea, or if anyone sees a Pro(s)/Con(s) that I am missing.</div><div><br></div></div></div>
<br></div></div>______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div></div></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>
______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div></div>
<br>______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>
</div></div></blockquote></div><br></div>