
On 2008-04-04, Neil Mitchell
What do you mean by "proper Lazy naturals"? Peano ones?
Yes
Not _strictly_ necessary. And I'd definitely like some suitable typeclass put in place. This represents positive arithmetic with a list homomorphism that forgets the elements and remembers only length. It's pretty much exactly equivalent to the function "map (const ())". This essentially unary representation isn't the only way to way to manipulate numbers by structure. You can do the same thing with many other data structures, such as trees, heaps, etc. In this case, yes, lists are the cleanest, being the underlying structure we're getting information about. (Aside: might as well just define the "less than" operation directly on the lists in this case -- or for any other arithmetic operation where we're not getting a list back. When we are, we usually can too, but it's a bit more fraught with concerns over whether that's really what we want -- we're throwing away information by replacing all elements with (), and perhaps we should have the typechecker warn us.[1]) But we can pull this trick with any container class. + corresponds to some merger or catenation, * to some cross product, zero to an empty data structure, and so forth. If you do this with Binomial heaps, out pop binary numbers. If you do this to certain types of efficient queues, "skew binary numbers" which support efficient increment and decrument pop out. This isn't surprising, as they were built using skew binary number for precisely this property. Those that haven't should take a look at Okasaki's _Purely Functional Data Structures_, particularly chapter 9: "Numerical Structures". http://books.google.com/books?id=SxPzSTcTalAC [1]: smallerThan :: [a] -> [b] -> Bool smallerThan [] [] = False smallerThan [] _ = True smallerThan _ [] = False smallerThan (_:as) (_:bs) = smallerThan as bs noGreaterThan :: [a] -> [b] -> Bool noGreaterThan [] _ = True noGreaterThan _ [] = False noGreaterThan (_:as) (_:bs) = noGreaterThan as bs are perfectly reasonable, but it's less clear that nattify = map const () (+) xs ys = (++) (nattify xs) (nattify ys) would be good universal definitions. -- Aaron Denney -><-