Your last point is interesting - I believe Idris and/or Agda in fact go out of their way to show a natural number type defined using induction as a key example. I remember being blown away by that.
Coming from dynamic languages towards appreciation of static types, this sort of thing is inspiring. I've been looking forward to writing some practical work in those languages when children and time give the chance.
> it's actually possible to do the "input verification" at one specific point in your program and then have a "proven" safe input and then never have to do any validation/verification again.
This can be done with "tainting" types, which are simple intersection types (even Java has them as one of its new pluggable type systems [1]), and doesn't require dependent types.
It's useless if it's optional.
So is F#.
Assuming you mean “dependent types in F#” rather than “F#”, after reading the article, I concluded that these are, in fact, not dependent types, but just so-called “smart constructors”. Since “dependent types in F#” don't exist, it doesn't make sense to ask whether they're useful or useless.
I meant that F# itself is optional. So are tests, by the way, and therefore also completely useless.
Yeah, F# is kind of problematic since you aren't forced to use F# to typefully use F# libraries. Things would be a lot better in a language like Standard ML, where you can either use a library correctly (assuming it exposes the right interfaces) or not use it at all. Hooray for abstraction!
Of course you have do deal with receiving data at run time, but I think very few people appreciate that it's actually possible to do the "input verification" at one specific point in your program and then have a "proven" safe input and then never have to do any validation/verification again. This even goes for things like "give me a vector of integers between 1 to 3 of size exactly 9 as input". Of course you still have to handle the invalid cases in that one specific place, but that's no different from how you'd ideally do validation anyway. That stuff already should be in a single place, and dependent types make that utterly obvious at compile time :).
(I think I may actually be agreeing with what you're saying, but I though it worth expounding on what dependent types can do for you.)
Btw, AFAIUI Liquid Types, at least as far as LiquidHaskell goes, is still a thing, though it's definitely quite "researchy" and who knows whether it'll become 'mainstream'.
Liquid Types also seem to be somewhat orthogonal to dependent types since they usually just rely on an external solver that works by "magic" (SMT) and which has built-in knowledge of e.g. arithmetic whereas most attempts at dependent types seem to want to avoid building in any of that knowledge in favor of induction + a more general "tactics" or "elaboration" type solving where the programmer guides the solver along. (Idris is an example of the latter, I think.)