"Cale Gibbard"
Another thing to note is that all the natural literals are not, as one might initially think, plain values, but actually represent the embedding of that natural number into the ring (instance of Num), by way of 0 and 1.
Excellent point, and good categorical thinking. The morphisms are more
important than the objects.
Jón Fairbairn
I think the present design is wrong because we don't have a type for naturals.
Meh. Naturals are reasonably useful sometimes, but not often enough, in my opinion. Any sort of numeric hierarchy designed to deal with them would be totally broken from my point of view -- if you don't at least have inverses, it's not a number, just some sort of weird algebraic structure. And if it's not in the numeric hierarchy, and so you can't do arithmetic syntactically nicely with it, what's the point? Is it better to make (^^), (^), and "take" partial functions, or to make (-) and "negate" partial functions? Hmm, here's an idea: have a Nat type, but no arithmetic defined on it besides Succ, and isZero. Of course, that makes the fastexp algorithm unfeasible, and is essentially isomorphic to [()]. Hmm. That gives
length = map (const ()) take = zipWith (flip const)
Feel free to consider this a strawman, but it *is* kind of elegant. There's no scaling loss, as these are inherently O(N). And it even means length and take can handle infinite lists. What's not to like? Of course, there's always a typeclass, where we could add all sorts of other encodings of the Peano axioms, such as binary trees,, but I don't see that that buys us much if we don't also get access to operations beyond them, such as (an _efficient_) `div` for fastexp. (Taking every n'th element (Peano encoded, of course) is _not_ good enough). -- Aaron Denney -><-