Suppose that we wish to define types such as

type upto[n] = {x:Int | 0 <= x & x < n}
type posArr = {f:Array[Int] | forall i:upto[f.length]. 0 <= f(i)}

var w : upto[v]
var a : posArr = new Array[10]
var i : upto[10] 
var p : upto[MAXINT]
a[i] = 4 // must prove: 0 <= i < 10, 0 <= 4
p = a[0] // must prove: 0 <= 0 < 10, 0 <= a[0] < 10

The types can then refer to values. These are dependent types. Scala has a special form of these (path-dependent types).

In general, dependent types require some form of automated theorem proving to check the implications of underlying constraints.

• more in Software Analysis and Verification