It's not a question of whether you can do it in principle or not. My point was that I don't think it's an effective approach for creating such specifications compared to the alternatives such as runtime contracts.
Why is that? In fact, I would argue you want both. You want to use a contract to check the incoming data, but once it's been checked, you'd want to wrap it in a type that guarantees the property is set.
Otherwise, you have to iterate over a potentially very large set of data to check if it's sorted every time you want to use a function that has that contract.
