Re: Proposal: Add inductively-defined Nat to base

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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries