On 2008-08-26, Simon Peyton-Jones
| >> I've actually long wondered about this: why don't more functions use | >> Nat where it'd make sense? It can't be because Nat is hard to define - | >> I'd swear I've seen many definitions of Nat (if not dozens when you | >> count all the type-level exercises which include one). | > | > Because naive definitions are dog-slow and fast definitions are anything | > but easy to use?
I doubt that even GHC is going to optimise data Nat = Z | S Nat into data Nat = N Int# (with appropriate checks) anytime soon.
I think the main reason that the latter (which can easily be implemented as a library) is not more widely used is that it's tiresomely incompatible with functions that produce Ints.
(Or Integers, or Integral a => a). Definitely.
Also perhaps if length :: [a] -> Nat, then computing the difference between two lengths (length xs - length ys) could produce a runtime error.
It's not so crazy to think that the right thing to do for the subtraction of naturals overflowing is return 0. It fits in with drop and takes behaviour, and arguably zips. There are natural near homomorphisms in place between lists and numbers, and taking negatives as 0 seems to improve the matching a bit. -- Aaron Denney -><-