| >> 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. Also perhaps if length :: [a] -> Nat, then computing the difference between two lengths (length xs - length ys) could produce a runtime error. But these are all matters of taste, software engineering, and inertia (legacy code). It'd be a worthwhile exercise to try making a version of the standard libs using Nat where it's appropriate, and see how convenient or otherwise it turns out to be. Simon