<div dir="auto">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).<div dir="auto"><br></div><div dir="auto">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.</div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Apr 5, 2018, 10:56 Donnacha Oisín Kidney <<a href="mailto:oisin.kidney@gmail.com">oisin.kidney@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I think the Agda desugaring trick is possible in Haskell currently, using view patterns:<br>
<br>
{-# LANGUAGE TypeFamilies        #-}<br>
{-# LANGUAGE TypeInType          #-}<br>
{-# LANGUAGE GADTs               #-}<br>
{-# LANGUAGE ScopedTypeVariables #-}<br>
{-# LANGUAGE TypeOperators       #-}<br>
{-# LANGUAGE PatternSynonyms     #-}<br>
{-# LANGUAGE ViewPatterns        #-}<br>
<br>
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}<br>
<br>
import Data.Kind          (Type)<br>
import Data.Coerce        (coerce)<br>
import Numeric.Natural    (Natural)<br>
import Data.Type.Equality ((:~:)(..),gcastWith)<br>
import Unsafe.Coerce      (unsafeCoerce)<br>
<br>
data family The k :: k -> Type<br>
<br>
class Sing (a :: k) where sing :: The k (a :: k)<br>
<br>
data Nat = Z | S Nat<br>
<br>
newtype instance The Nat n = NatSing Natural<br>
<br>
instance Sing Z where<br>
    sing = NatSing 0<br>
<br>
instance Sing n => Sing (S n) where<br>
    sing =<br>
        (coerce :: (Natural -> Natural) -> (The Nat n -> The Nat (S n)))<br>
            succ sing<br>
<br>
data Natty n where<br>
        ZZy :: Natty Z<br>
        SSy :: The Nat n -> Natty (S n)<br>
<br>
getNatty :: The Nat n -> Natty n<br>
getNatty (NatSing n :: The Nat n) = case n of<br>
  0 -> gcastWith (unsafeCoerce Refl :: n :~: Z) ZZy<br>
  _ -> gcastWith (unsafeCoerce Refl :: n :~: S m) (SSy (NatSing (pred n)))<br>
<br>
pattern Zy :: () => (n ~ Z) => The Nat n<br>
pattern Zy <- (getNatty -> ZZy) where Zy = NatSing 0<br>
<br>
pattern Sy :: () => (n ~ S m) => The Nat m -> The Nat n<br>
pattern Sy x <- (getNatty -> SSy x) where Sy (NatSing x) = NatSing (succ x)<br>
{-# COMPLETE Zy, Sy #-}<br>
<br>
type family (+) (n :: Nat) (m :: Nat) :: Nat where<br>
        Z + m = m<br>
        S n + m = S (n + m)<br>
<br>
-- | Efficient addition, with type-level proof.<br>
add :: The Nat n -> The Nat m -> The Nat (n + m)<br>
add = (coerce :: (Natural -> Natural -> Natural) -> The Nat n -> The Nat m -> The Nat (n + m)) (+)<br>
<br>
-- | Proof on efficient representation.<br>
addZeroRight :: The Nat n -> n + Z :~: n<br>
addZeroRight Zy = Refl<br>
addZeroRight (Sy n) = gcastWith (addZeroRight n) Refl<br>
<br>
<br>
> On 19 Mar 2018, at 12:53, Daniel Cartwright <<a href="mailto:chessai1996@gmail.com" target="_blank" rel="noreferrer">chessai1996@gmail.com</a>> wrote:<br>
><br>
> Yes, that is along the lines of something I want.<br>
><br>
> On Mar 19, 2018 12:13 PM, "Carter Schonwald" <<a href="mailto:carter.schonwald@gmail.com" target="_blank" rel="noreferrer">carter.schonwald@gmail.com</a>> wrote:<br>
> 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<br>
><br>
> On Thu, Mar 15, 2018 at 10:41 PM, Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" target="_blank" rel="noreferrer">rae@cs.brynmawr.edu</a>> wrote:<br>
> 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.<br>
><br>
> Perhaps my hesitation is mostly because I favor a smaller `base`, in general.<br>
><br>
> Happy to defer to others here.<br>
><br>
> Richard<br>
><br>
><br>
>> On Mar 15, 2018, at 1:05 PM, Edward Kmett <<a href="mailto:ekmett@gmail.com" target="_blank" rel="noreferrer">ekmett@gmail.com</a>> wrote:<br>
>><br>
>> Er, by that I mean the type level nats, not the value-level ones.<br>
>><br>
>> On Thu, Mar 15, 2018 at 6:05 PM, Edward Kmett <<a href="mailto:ekmett@gmail.com" target="_blank" rel="noreferrer">ekmett@gmail.com</a>> wrote:<br>
>> AFAIK, the existing naturals in base don't have any useful internal structure permitting this sort of thing.<br>
>><br>
>> -Edward<br>
>><br>
>> On Thu, Mar 15, 2018 at 3:48 PM, Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank" rel="noreferrer">carter.schonwald@gmail.com</a>> wrote:<br>
>> Could we provide a pattern synonym for treating naturals as in base already as being peano encoded ?<br>
>><br>
>> On Wed, Mar 14, 2018 at 11:51 PM Daniel Cartwright <<a href="mailto:chessai1996@gmail.com" target="_blank" rel="noreferrer">chessai1996@gmail.com</a>> wrote:<br>
>> I just realised I made a typo. For full clarity, the function 'f' should be:<br>
>><br>
>> f : D -> N -> R<br>
>> where<br>
>> D = Data Structure isomorphic to Nat (or any numeric type)<br>
>> N = Number System Encoding<br>
>> R = Representation of the numeric type in N.<br>
>><br>
>> For Nats, the simplest example would be:<br>
>><br>
>> f : List () -> Binary -> BinaryEncodingOfNat<br>
>><br>
>><br>
>> On Wed, Mar 14, 2018 at 9:47 PM, Daniel Cartwright <<a href="mailto:chessai1996@gmail.com" target="_blank" rel="noreferrer">chessai1996@gmail.com</a>> wrote:<br>
>> I prefer Z and S, but wrote Zero and Succ for clarity (though the likelihood of being at all misunderstood was small).<br>
>><br>
>> Most recent definitions I see use Z and S.<br>
>><br>
>> On Wed, Mar 14, 2018 at 9:41 PM, David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank" rel="noreferrer">david.feuer@gmail.com</a>> wrote:<br>
>> 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.<br>
>><br>
>> On Mar 14, 2018 9:06 PM, "Daniel Cartwright" <<a href="mailto:chessai1996@gmail.com" target="_blank" rel="noreferrer">chessai1996@gmail.com</a>> wrote:<br>
>> The proposed addition is simple, add the following to base:<br>
>><br>
>> data Nat = Zero | Succ Nat,<br>
>><br>
>> i.e. Peano Nats - commonly used along with -XDataKinds.<br>
>><br>
>> I will list the pros/cons I see below:<br>
>><br>
>> Pros:<br>
>> - This datatype is commonly defined throughout many packages throughout Hackage. It would be good for it to have a central location<br>
>> - The inductive definition of 'Nat' is useful for correctness (e.g. safeHead :: Vec a (Succ n) -> a; safeHead (Cons a as) = a;)<br>
>> - -XDependentHaskell is likely to bring this into base anyway<br>
>> - 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)<br>
>><br>
>> Cons:<br>
>> - -XDependentHaskell will most likely obviate any benefit brought about by type families defined in base that directly involve Nat<br>
>> - Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange.<br>
>><br>
>> I am open to criticism concerning the usefulness of the idea, or if anyone sees a Pro(s)/Con(s) that I am missing.<br>
>><br>
>><br>
>> _______________________________________________<br>
>> Libraries mailing list<br>
>> <a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
>><br>
>><br>
>><br>
>><br>
>> _______________________________________________<br>
>> Libraries mailing list<br>
>> <a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
>><br>
>> _______________________________________________<br>
>> Libraries mailing list<br>
>> <a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
>><br>
>><br>
>><br>
>> _______________________________________________<br>
>> Libraries mailing list<br>
>> <a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
><br>
><br>
><br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
><br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>