Proposal: Add inductively-defined Nat to base

[Edward Kmett]

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