alt Hacker NewsYeah, right now there isn't really any example of the value tradeoff being high enough that its overcome the barriers to adoption. Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them; once that's been established, I think it's a lot easier to talk about why the approach hasn't yet become mainstream.
For example, with the potential utility in having dependent types for list APIs, the barrier is that in practice, it's not always straightforward to be able to define your code in a way where you actually know the size of the list. If I read input from a user, I might be able to do an initial check that a list of items is non-empty as part of the constructor for the type, but what happens if I want to start popping off elements from it? In practice, this seems like it would either force you to go back to manually checking or only ever process things in a purely functional way to avoid defining behavior that vary based on state that isn't known. If you're willing to take this approach, having the compiler enforce it is great! You have to be willing to use this approach often enough for it to be worth picking a language with dependent types though, and in practice it doesn't seem likely that people would choose to even if they were more aware of the option.
> Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them
There's probably some truth in that (I'm probably in this camp as well), though I feel sometimes adoption of things like this can often be a communication problem, and the people who understand these technologies the most may struggle to identify what aspect of these technologies are valued more by the people they are trying to pitch them too.
Like they might even find those aspects boring and uninteresting because they are so deep into the technology, that they don't even think to emphasis them. Which feels like a similar story where a technology early to the party didn't take off until someone else came back to them later (like fat structs and data oritented design gaining some interest despite early versions of these ideas date back to Sketchpad (1963)).
> For example, with the potential utility in having dependent types for list APIs, the barrier is that in practice, it's not always straightforward to be able to define your code in a way where you actually know the size of the list
Yeah this example crossed my mind as well, it's not immediately clear how you deal with IO or data the result of inputs from the outside world. Although I have feeling this has to be a solved problem.
I guess more generally with API design, sometimes you don't really know the system you want to model yet so there's diminishing returns in being overly precise in how you model it if those things are subject to change. Not sure how substantive a concern this is when weighing up using dependent types, but it is something that crosses my mind as an outsider to all this dependent type stuff.