> A type that proves that all values that inhabit it are sorted would also be nice. But if either the language doesn’t support dependent types or it is too difficult to prove then a contract could be used instead (again: not as a replacement).
This is really easy in a dependently typed language. If something is hard to prove by construction you can do
sort: List -> List
which sorts a list without proving it to be sorted, and then write a function
isSorted: List -> Maybe SortedList
then just get your safe sort function
safeSort: List -> SortedList
safeSort l = case sort l of { Nothing -> panic; Just x -> x }
Of course, you don't even need dependent typing to do this. If SortedList is a new nominal type and you trust your issorted function, everything works out.
The not-so-easy part arises when you need to operate on a SortedList and want to enforce that it remains sorted after said operation. Maybe in the specific case of SortedList it's not that bad, but my (limited) experience is that the complexity in such cases can accumulate surprisingly high and surprisingly quickly.
I have frequently found myself out of my depth when trying to write what I thought should be straightforward dependently-typed code. I got the hang of it after a lot of practice (as well as a lot of reading, note-taking, and outside help). But now you're asking programmers to learn an entirely new set of skills on top of everything else they're expected to know.
I love the idea of dependent types, and I've had a lot of fun messing around with Idris 2, but I think dependently-typed languages have a lot of work to do in order to bridge the ergonomics gap.
I'm not convinced that, for garden-variety software development, dependent types are substantially safer than extensive use of contracts and property-based testing.
That's exactly what my framework does. As long as you're okay with runtime panics (which would happen anyway in a non-dependently typed language), you just have any function you don't know how to prove go from SortedList -> List. Then you have a check List -> Maybe SortedList. And finally a function with a panic that lets you write the SortedList -> SortedList version.
This is really easy in a dependently typed language. If something is hard to prove by construction you can do
which sorts a list without proving it to be sorted, and then write a function then just get your safe sort function Of course, you don't even need dependent typing to do this. If SortedList is a new nominal type and you trust your issorted function, everything works out.