Proposal: Add inductively-defined Nat to base

[Edward Kmett]

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