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.
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.