Aren't contracts a feature of the type system? They encode a specific type that differs from the base type by a more complex predicate, like a constraint check in SQL.