Proposal: Add inductively-defined Nat to base

[Richard Eisenberg]

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.

Perhaps my hesitation is mostly because I favor a smaller `base`, in general.

Happy to defer to others here.

Richard

> On Mar 15, 2018, at 1:05 PM, Edward Kmett <ekmett at gmail.com> wrote:
> 
> Er, by that I mean the type level nats, not the value-level ones.
> 
> On Thu, Mar 15, 2018 at 6:05 PM, Edward Kmett <ekmett at gmail.com <mailto:ekmett at gmail.com>> wrote:
> AFAIK, the existing naturals in base don't have any useful internal structure permitting this sort of thing.
> 
> -Edward
> 
> On Thu, Mar 15, 2018 at 3:48 PM, Carter Schonwald <carter.schonwald at gmail.com <mailto:carter.schonwald at gmail.com>> wrote:
> Could we provide a pattern synonym for treating naturals as in base already as being peano encoded ?
> 
> On Wed, Mar 14, 2018 at 11:51 PM Daniel Cartwright <chessai1996 at gmail.com <mailto:chessai1996 at gmail.com>> wrote:
> I just realised I made a typo. For full clarity, the function 'f' should be:
> 
> f : D -> N -> R
> where
> D = Data Structure isomorphic to Nat (or any numeric type)
> N = Number System Encoding
> R = Representation of the numeric type in N.
> 
> For Nats, the simplest example would be:
> 
> f : List () -> Binary -> BinaryEncodingOfNat
> 
> 
> On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <chessai1996 at gmail.com <mailto:chessai1996 at gmail.com>> wrote:
> I prefer Z and S, but wrote Zero and Succ for clarity (though the likelihood of being at all misunderstood was small).
> 
> Most recent definitions I see use Z and S.
> 
> On Wed, Mar 14, 2018 at 9:41 PM, David Feuer <david.feuer at gmail.com <mailto:david.feuer at gmail.com>> wrote:
> 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.
> 
> On Mar 14, 2018 9:06 PM, "Daniel Cartwright" <chessai1996 at gmail.com <mailto:chessai1996 at gmail.com>> wrote:
> The proposed addition is simple, add the following to base:
> 
> data Nat = Zero | Succ Nat,
> 
> i.e. Peano Nats - commonly used along with -XDataKinds.
> 
> I will list the pros/cons I see below:
> 
> Pros:
> - This datatype is commonly defined throughout many packages throughout Hackage. It would be good for it to have a central location
> - The inductive definition of 'Nat' is useful for correctness (e.g. safeHead :: Vec a (Succ n) -> a; safeHead (Cons a as) = a;)
> - -XDependentHaskell is likely to bring this into base anyway
> - 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)
> 
> Cons:
> - -XDependentHaskell will most likely obviate any benefit brought about by type families defined in base that directly involve Nat
> - Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange.
> 
> I am open to criticism concerning the usefulness of the idea, or if anyone sees a Pro(s)/Con(s) that I am missing.
> 
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
> 
> 
> 
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
> 
> 
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180315/b53de8ab/attachment.html>