Re: Proposal: Add inductively-defined Nat to base

what would be nice would be figuring out how to do something like the Agda desugaring trick, where naturals have both the inductive rep exposed AND efficient primops arithmetically On Thu, Mar 15, 2018 at 10:41 PM, Richard Eisenberg wrote:

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 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 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@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@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@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 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" 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries