Proposal: Add inductively-defined Nat to base

[Daniel Cartwright]

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