On 2008.08.23 15:48:10 -0400, "Brandon S. Allbery KF8NH"
On 2008 Aug 23, at 15:46, Gwern Branwen wrote:
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?
-- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com
While I am but a mediocre Haskell programmer at best, I can't say I find that a satisfying explanation. When I read the GHC & fusion papers (among many many other fine papers relating to Haskell), I am impressed at the optimizations the authors managed to eek out despite the difficult conditions they labor under. With that in mind, I find it hard to accept that there is no approach which is fast and easy to use - no theorems or rewrite rules or library which provides it. When I consider it, it seems to me that it's not hard to define a Nat type which does checks for < 0 at runtime, so given the Olegian feats Haskell lends itself to, why is it not easy to staticly turn Nats into Ints or similarly performant types? -- gwern CESID Security Delta d DUVDEVAN SRI composition data-haven SONANGOL World