Proposal: Add inductively-defined Nat to base

[Daniel Cartwright]

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