Proposal: Add inductively-defined Nat to base
Jon Purdy
evincarofautumn at gmail.com
Fri Apr 6 09:58:58 UTC 2018
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 <oisin.kidney at gmail.com>
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 <chessai1996 at gmail.com>
> wrote:
> >
> > Yes, that is along the lines of something I want.
> >
> > On Mar 19, 2018 12:13 PM, "Carter Schonwald" <carter.schonwald at gmail.com>
> 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 <rae at cs.brynmawr.edu>
> 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 <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> 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> 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> 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> 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>
> 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>
> 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
> >> 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
> >>
> >> _______________________________________________
> >> Libraries mailing list
> >> Libraries at haskell.org
> >> 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
> >
> >
> >
> > _______________________________________________
> > Libraries mailing list
> > Libraries at haskell.org
> > 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
>
> _______________________________________________
> 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/20180406/40334a7c/attachment.html>
More information about the Libraries
mailing list