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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
I believe that at the value level, Peano Nats can be optimised using pattern synonyms. The primary interest of Peano Nats, however, is in their use at the kind level - so I think two things are possible:
1. With -XDependentHaskell, one can define a pattern synonym allowing the optimisation of Peano Nats, 2. With type families, it _might_ be possible to define a weaker form of (1), provided it is possible to put a type synonym on the LHS of a type family. Question: Can a TypeApplication be used on the LHS of an injective type family? On Wed, Mar 14, 2018 at 9:05 PM, Daniel Cartwright <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by chessai .
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" <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Yes, that is along the lines of something I want. On Mar 19, 2018 12:13 PM, "Carter Schonwald" <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> wrote: > > Yes, that is along the lines of something I want. > > On Mar 19, 2018 12:13 PM, "Carter Schonwald" <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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" <[hidden email]> 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 >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >> >> >> >> >> _______________________________________________ >> Libraries mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >> >> _______________________________________________ >> Libraries mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >> >> >> >> _______________________________________________ >> Libraries mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > > > > _______________________________________________ > Libraries mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > > _______________________________________________ > Libraries mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> wrote: I think the Agda desugaring trick is possible in Haskell currently, using view patterns: _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
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 <[hidden email]> 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 > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Free forum by Nabble | Edit this page |