Dependent types in practical programming

We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint dom...