Proposal: Add inductively-defined Nat to base

[Daniel Cartwright]

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