[richdougherty]

I agree, there's doesn't seem to be any reason why you can't use types to express something like contracts. I think the general name for these kinds of types is 'refinement types':

"a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types"

- https://en.wikipedia.org/wiki/Refinement_type

There's even some literature linking contracts and types directly:

"Traditional static type systems are effective for verifying basic interface specifications. Dynamically-checked contracts support more precise specifications, but these are not checked until run time, resulting in incomplete detection of defects. ... This paper explores the key ideas and implications of hybrid type checking, in the context of the λ-calculus extended with contract types, i.e., with dependent function types and with arbitrary refinements of base types."

- https://users.soe.ucsc.edu/~cormac/papers/toplas09.pdf