Proposal: Add inductively-defined Nat to base

[Donnacha Oisín Kidney]

This solution would still keep the lazy Nat type around: the optimised version (the patterns Sy and Zy over the newtype for Natural) is just a singleton, for proofs.

You don’t get the benefit of laziness for proofs, regardless (as you have to pattern match to prove), so I don’t think you lose anything with this representation.

What I had in mind for it was something like this:

data Tree n a where
  Leaf :: Tree Z a
  Node :: The Nat n -> a -> Tree n a -> Tree m a -> Tree (S (n + m)) a

where the singleton could be efficiently compared and added, but also would provide a proof. Again, I don’t think laziness can be of benefit here.

> On 6 Apr 2018, at 06:07, Henning Thielemann <lemming at henning-thielemann.de> wrote:
> 
> 
> On Fri, 6 Apr 2018, Jon Purdy wrote:
> 
>> One thing I like about the naturals with the “linked list” representation is that they’re lazy. When I was first
>> learning Haskell, years ago, I expected something like “length xs > 1” to only evaluate “xs” up to the second
>> constructor—that doesn’t work with “length” and “Int”, being strict, but it does work with “genericLength” and a
>> lazy “Nat” (and “Ord” instance I guess).
> 
> It would also work with:
>   void xs > replicate 1 ()_______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries