
<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">For what it's worth, I'm ambivalent on this one until we have a way to use these Nats without the terrible performance they would naturally have. I'm not against -- this definition would be useful -- but I also don't see such a big advantage to baking these into GHC's shipped libraries.<div class=""><br class=""></div><div class="">Perhaps my hesitation is mostly because I favor a smaller `base`, in general.</div><div class=""><br class=""></div><div class="">Happy to defer to others here.</div><div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 15, 2018, at 1:05 PM, Edward Kmett <<a href="mailto:ekmett@gmail.com" class="">ekmett@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Er, by that I mean the type level nats, not the value-level ones.</div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Thu, Mar 15, 2018 at 6:05 PM, Edward Kmett <span dir="ltr" class=""><<a href="mailto:ekmett@gmail.com" target="_blank" class="">ekmett@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class="">AFAIK, the existing naturals in base don't have any useful internal structure permitting this sort of thing.<span class="HOEnZb"><font color="#888888" class=""><div class=""><br class=""></div><div class="">-Edward</div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br class=""><div class="gmail_quote">On Thu, Mar 15, 2018 at 3:48 PM, Carter Schonwald <span dir="ltr" class=""><<a href="mailto:carter.schonwald@gmail.com" target="_blank" class="">carter.schonwald@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class=""><div dir="auto" class="">Could we provide a pattern synonym for treating naturals as in base already as being peano encoded ?</div><div class=""><div class="m_-3379528805270109257h5"><br class=""><div class="gmail_quote"><div class="">On Wed, Mar 14, 2018 at 11:51 PM Daniel Cartwright <<a href="mailto:chessai1996@gmail.com" target="_blank" class="">chessai1996@gmail.com</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="">I just realised I made a typo. For full clarity, the function 'f' should be:<div class=""><br class=""></div><div class="">f : D -> N -> R<br class=""></div><div class="">where</div><div class=""><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" class="">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" class="">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" class="">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" class=""><br class=""></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" class="">For Nats, the simplest example would be:<br class=""><br class="">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" class=""><br class=""></div></div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <span class=""><<a href="mailto:chessai1996@gmail.com" target="_blank" class="">chessai1996@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="">I prefer Z and S, but wrote Zero and Succ for clarity (though the likelihood of being at all misunderstood was small).<div class=""><br class=""></div><div class="">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 class=""><div class="gmail_quote">On Wed, Mar 14, 2018 at 9:41 PM, David Feuer <span class=""><<a href="mailto:david.feuer@gmail.com" target="_blank" class="">david.feuer@gmail.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto" class=""><div class="">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 class=""><div class="gmail_extra"><br class=""><div class="gmail_quote"><div class=""><div class="m_-3379528805270109257m_2272561796430452094m_5228945314180559036m_-6069599319899534346h5">On Mar 14, 2018 9:06 PM, "Daniel Cartwright" <<a href="mailto:chessai1996@gmail.com" target="_blank" class="">chessai1996@gmail.com</a>> wrote:<br type="attribution" class=""></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 class=""><div class="m_-3379528805270109257m_2272561796430452094m_5228945314180559036m_-6069599319899534346h5"><div class="">The proposed addition is simple, add the following to base:<br class=""><br class="">data Nat = Zero | Succ Nat,<div class=""><br class=""></div><div class="">i.e. Peano Nats - commonly used along with -XDataKinds.</div><div class=""><br class=""><div class="">I will list the pros/cons I see below:<br class=""><br class="">Pros:<br class="">- This datatype is commonly defined throughout many packages throughout Hackage. It would be good for it to have a central location</div><div class="">- The inductive definition of 'Nat' is useful for correctness (e.g. safeHead :: Vec a (Succ n) -> a; safeHead (Cons a as) = a;)</div><div class="">- -XDependentHaskell is likely to bring this into base anyway</div><div class="">- 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 class=""><br class=""></div><div class="">Cons:</div><div class="">- -XDependentHaskell will most likely obviate any benefit brought about by type families defined in base that directly involve Nat</div><div class="">- Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange.</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div></div></div>

<br class=""></div></div>______________________________<wbr class="">_________________<br class="">

Libraries mailing list<br class="">

<a href="mailto:Libraries@haskell.org" target="_blank" class="">Libraries@haskell.org</a><br class="">

<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bi<wbr class="">n/mailman/listinfo/libraries</a><br class="">

<br class=""></blockquote></div><br class=""></div></div></div>

</blockquote></div><br class=""></div>

</div></div></blockquote></div><br class=""></div>

______________________________<wbr class="">_________________<br class="">

Libraries mailing list<br class="">

<a href="mailto:Libraries@haskell.org" target="_blank" class="">Libraries@haskell.org</a><br class="">

<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bi<wbr class="">n/mailman/listinfo/libraries</a><br class="">

</blockquote></div></div></div></div>

<br class="">______________________________<wbr class="">_________________<br class="">

Libraries mailing list<br class="">

<a href="mailto:Libraries@haskell.org" target="_blank" class="">Libraries@haskell.org</a><br class="">

<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bi<wbr class="">n/mailman/listinfo/libraries</a><br class="">

<br class=""></blockquote></div><br class=""></div>

</div></div></blockquote></div><br class=""></div>

_______________________________________________<br class="">Libraries mailing list<br class=""><a href="mailto:Libraries@haskell.org" class="">Libraries@haskell.org</a><br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries<br class=""></div></blockquote></div><br class=""></div></body></html>