Add inductively-defined Nat to base
The proposed addition is simple, add the following to base:
data Nat = Zero | Succ Nat
I will list the pros/cons I see below. Pros:
- Commonly defined throughout many packages, e.g. vinyl
- The inductive definition of 'Nat' is useful for correctness
(e.g.
safeHead :: Vec a (S n) -> a; safeHead (Cons a as) = a
)
Cons:
- '-XDependentHaskell' will most likely obviate any benefit brought about by type families involving 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.