[Haskell-cafe] Positive integers

[Jan-Willem Maessen]

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