It turns out that it's quite possible to express almost all of the invariants you describe in a type system, and we've done it in Typed Racket. Vincent St-Amour

It turns out that it's quite possible to express almost all of the invariants you describe in a type system, and we've done it in Typed Racket. Vincent St-Amour wrote a paper about it: http://www.ccs.neu.edu/racket/pubs/padl12-stff.pdf http://www.ccs.neu.edu/racket/pubs/padl12-stff.pdf It can express that 2^2 is positive and an integer, that 2^-2 is positive and a rational, and that 2-3 is an integer but not necessarily positive.