|
|
|
|
|
|
by typish
4067 days ago
|
|
|
Liquid Haskell might be what you are looking for: http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf An example from that paper: type Nat = {v:Int | 0 <=v }
type Pos = {v:Int | 0 < v }
div :: Nat -> d:Pos -> {v:Nat | v <= n}
The ATS programming language (http://www.ats-lang.org) is more ML-like than Haskell-like but can have ranged integer types. Something like: fun slice {n:int | n >= 1} (a:int n, b:list)
|
|
|