Re: Proposal: Add inductively-defined Nat to base

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