On Mar 26, 2006, at 4:35 PM, Daniel McAllansmith wrote:
[Discussion of positive integers and Words]
I was thinking about several things in this thread, torsors, overflow semantics, bounds checking... I wonder if there would be any merit in being able to define constrained subsets of integers and the semantics when/if they overflow.
Oddly, I've just finished coding this up, with type-level bounds (represented by type-level ints). It's a big pile of modules on top of John Meacham's type-level Nats library, which add type-level Ints (as non-normalized Nat pairs), unknown endpoints (permitting Integer to fit in the same framework), and the actual bounded ints themselves. Naturally, I needed to define my own versions of the functionality in Eq, Ord, and Num. These resolve statically as much as possible (including some possibly dubious behavior with singleton intervals). That said, I don't try to do everything at the type level---it became too tiring, with not enough plausible benefit. Any and all: Drop me a line if you are interested, it's a stack of 3-4 modules and at best half-baked. I'd just gotten a mostly- complete version. -Jan-Willem Maessen