Proposal: Add inductively-defined Nat to base

[Daniel Cartwright]

I believe that at the value level, Peano Nats can be optimised using
pattern synonyms. The primary interest of Peano Nats, however, is in their
use at the kind level - so I think two things are possible:

1. With -XDependentHaskell, one can define a pattern synonym allowing the
optimisation of Peano Nats,
2. With type families, it _might_ be possible to define a weaker form of
(1), provided it is possible to put a type synonym on the LHS
    of a type family.

Question: Can a TypeApplication be used on the LHS of an injective type
family?

On Wed, Mar 14, 2018 at 9:05 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.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180314/92e79445/attachment.html>