<div dir="ltr">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:<br><br>1. With -XDependentHaskell, one can define a pattern synonym allowing the optimisation of Peano Nats,<div>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</div><div>    of a type family.</div><div><br></div><div>Question: Can a TypeApplication be used on the LHS of an injective type family?<br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 14, 2018 at 9:05 PM, Daniel Cartwright <span dir="ltr"><<a href="mailto:chessai1996@gmail.com" target="_blank">chessai1996@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">The proposed addition is simple, add the following to base:<br><br>data Nat = Zero | Succ Nat,<div><br></div><div>i.e. Peano Nats - commonly used along with -XDataKinds.</div><div><br><div>I will list the pros/cons I see below:<br><br>Pros:<br>- This datatype is commonly defined throughout many packages throughout Hackage. It would be good for it to have a central location</div><div>- The inductive definition of 'Nat' is useful for correctness (e.g. safeHead :: Vec a (Succ n) -> a; safeHead (Cons a as) = a;)</div><div>- -XDependentHaskell is likely to bring this into base anyway</div><div>- 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)</div><div><br></div><div>Cons:</div><div>- -XDependentHaskell will most likely obviate any benefit brought about by type families defined in base that directly involve Nat</div><div>- Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange.</div><div><br></div><div>I am open to criticism concerning the usefulness of the idea, or if anyone sees a Pro(s)/Con(s) that I am missing.</div><div><br></div></div></div>
</blockquote></div><br></div></div></div>