Proposal: Add inductively-defined Nat to base

[Carter Schonwald]

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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180319/fe90d3e7/attachment.html>