Proposal: Add inductively-defined Nat to base

newer
Remove mtimesDefault or move it to...

Daniel Cartwright

14 Mar 2018 14 Mar '18

9:05 p.m.

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.

Attachments:

attachment.html (text/html — 1.7 KB)

Show replies by date

David Feuer

14 Mar 14 Mar

9:41 p.m.

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

Daniel Cartwright

9:47 p.m.

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

Daniel Cartwright

11:50 p.m.

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

Carter Schonwald

15 Mar 15 Mar

10:48 a.m.

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

Edward Kmett

1:05 p.m.

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

Edward Kmett

1:05 p.m.

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

Richard Eisenberg

10:41 p.m.

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 mailto:ekmett@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 mailto: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 mailto: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 mailto: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 mailto:david.feuer@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" mailto:chessai1996@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@haskell.org mailto:Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

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

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

Carter Schonwald

19 Mar 19 Mar

12:11 p.m.

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

Daniel Cartwright

12:53 p.m.

Yes, that is along the lines of something I want. On Mar 19, 2018 12:13 PM, "Carter Schonwald" wrote:

...

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

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

Donnacha Oisín Kidney

5 Apr 5 Apr

1:55 p.m.

I think the Agda desugaring trick is possible in Haskell currently, using view patterns: {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} import Data.Kind (Type) import Data.Coerce (coerce) import Numeric.Natural (Natural) import Data.Type.Equality ((:~:)(..),gcastWith) import Unsafe.Coerce (unsafeCoerce) data family The k :: k -> Type class Sing (a :: k) where sing :: The k (a :: k) data Nat = Z | S Nat newtype instance The Nat n = NatSing Natural instance Sing Z where sing = NatSing 0 instance Sing n => Sing (S n) where sing = (coerce :: (Natural -> Natural) -> (The Nat n -> The Nat (S n))) succ sing data Natty n where ZZy :: Natty Z SSy :: The Nat n -> Natty (S n) getNatty :: The Nat n -> Natty n getNatty (NatSing n :: The Nat n) = case n of 0 -> gcastWith (unsafeCoerce Refl :: n :~: Z) ZZy _ -> gcastWith (unsafeCoerce Refl :: n :~: S m) (SSy (NatSing (pred n))) pattern Zy :: () => (n ~ Z) => The Nat n pattern Zy <- (getNatty -> ZZy) where Zy = NatSing 0 pattern Sy :: () => (n ~ S m) => The Nat m -> The Nat n pattern Sy x <- (getNatty -> SSy x) where Sy (NatSing x) = NatSing (succ x) {-# COMPLETE Zy, Sy #-} type family (+) (n :: Nat) (m :: Nat) :: Nat where Z + m = m S n + m = S (n + m) -- | Efficient addition, with type-level proof. add :: The Nat n -> The Nat m -> The Nat (n + m) add = (coerce :: (Natural -> Natural -> Natural) -> The Nat n -> The Nat m -> The Nat (n + m)) (+) -- | Proof on efficient representation. addZeroRight :: The Nat n -> n + Z :~: n addZeroRight Zy = Refl addZeroRight (Sy n) = gcastWith (addZeroRight n) Refl

...

On 19 Mar 2018, at 12:53, Daniel Cartwright wrote:

Yes, that is along the lines of something I want.

On Mar 19, 2018 12:13 PM, "Carter Schonwald" wrote: 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 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 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 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

_______________________________________________ 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

Jon Purdy

6 Apr 6 Apr

5:58 a.m.

One thing I like about the naturals with the “linked list” representation is that they’re lazy. When I was first learning Haskell, years ago, I expected something like “length xs > 1” to only evaluate “xs” up to the second constructor—that doesn’t work with “length” and “Int”, being strict, but it does work with “genericLength” and a lazy “Nat” (and “Ord” instance I guess). So I think it would be desirable for an optimised representation to preserve this, but I dunno if it’s possible/easy, or if anyone else particularly cares—the use cases I know of are admittedly narrow, but the fault might just be in my knowledge. I suppose there could be lazy and strict versions of the “Nat” type if it seems important enough. On Thu, Apr 5, 2018, 10:56 Donnacha Oisín Kidney wrote:

...

I think the Agda desugaring trick is possible in Haskell currently, using view patterns:

{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-}

{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}

import Data.Kind (Type) import Data.Coerce (coerce) import Numeric.Natural (Natural) import Data.Type.Equality ((:~:)(..),gcastWith) import Unsafe.Coerce (unsafeCoerce)

data family The k :: k -> Type

class Sing (a :: k) where sing :: The k (a :: k)

data Nat = Z | S Nat

newtype instance The Nat n = NatSing Natural

instance Sing Z where sing = NatSing 0

instance Sing n => Sing (S n) where sing = (coerce :: (Natural -> Natural) -> (The Nat n -> The Nat (S n))) succ sing

data Natty n where ZZy :: Natty Z SSy :: The Nat n -> Natty (S n)

getNatty :: The Nat n -> Natty n getNatty (NatSing n :: The Nat n) = case n of 0 -> gcastWith (unsafeCoerce Refl :: n :~: Z) ZZy _ -> gcastWith (unsafeCoerce Refl :: n :~: S m) (SSy (NatSing (pred n)))

pattern Zy :: () => (n ~ Z) => The Nat n pattern Zy <- (getNatty -> ZZy) where Zy = NatSing 0

pattern Sy :: () => (n ~ S m) => The Nat m -> The Nat n pattern Sy x <- (getNatty -> SSy x) where Sy (NatSing x) = NatSing (succ x) {-# COMPLETE Zy, Sy #-}

type family (+) (n :: Nat) (m :: Nat) :: Nat where Z + m = m S n + m = S (n + m)

-- | Efficient addition, with type-level proof. add :: The Nat n -> The Nat m -> The Nat (n + m) add = (coerce :: (Natural -> Natural -> Natural) -> The Nat n -> The Nat m -> The Nat (n + m)) (+)

-- | Proof on efficient representation. addZeroRight :: The Nat n -> n + Z :~: n addZeroRight Zy = Refl addZeroRight (Sy n) = gcastWith (addZeroRight n) Refl

...
On 19 Mar 2018, at 12:53, Daniel Cartwright wrote:

Yes, that is along the lines of something I want.

On Mar 19, 2018 12:13 PM, "Carter Schonwald" wrote: 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

_______________________________________________ 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

Henning Thielemann

6:07 a.m.

On Fri, 6 Apr 2018, Jon Purdy wrote:

...

One thing I like about the naturals with the “linked list” representation is that they’re lazy. When I was first learning Haskell, years ago, I expected something like “length xs > 1” to only evaluate “xs” up to the second constructor—that doesn’t work with “length” and “Int”, being strict, but it does work with “genericLength” and a lazy “Nat” (and “Ord” instance I guess).

It would also work with: void xs > replicate 1 ()

Donnacha Oisín Kidney

9:48 a.m.

This solution would still keep the lazy Nat type around: the optimised version (the patterns Sy and Zy over the newtype for Natural) is just a singleton, for proofs. You don’t get the benefit of laziness for proofs, regardless (as you have to pattern match to prove), so I don’t think you lose anything with this representation. What I had in mind for it was something like this: data Tree n a where Leaf :: Tree Z a Node :: The Nat n -> a -> Tree n a -> Tree m a -> Tree (S (n + m)) a where the singleton could be efficiently compared and added, but also would provide a proof. Again, I don’t think laziness can be of benefit here.

...

On 6 Apr 2018, at 06:07, Henning Thielemann wrote:

On Fri, 6 Apr 2018, Jon Purdy wrote:

...
One thing I like about the naturals with the “linked list” representation is that they’re lazy. When I was first learning Haskell, years ago, I expected something like “length xs > 1” to only evaluate “xs” up to the second constructor—that doesn’t work with “length” and “Int”, being strict, but it does work with “genericLength” and a lazy “Nat” (and “Ord” instance I guess).

It would also work with: void xs > replicate 1 ()_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

2601

Age (days ago)

2623

Last active (days ago)

List overview

Download

13 comments

9 participants

participants (9)

Carter Schonwald
Daniel Cartwright
David Feuer
Donnacha Oisín Kidney
Donnacha Oisín Kidney
Edward Kmett
Henning Thielemann
Jon Purdy
Richard Eisenberg