4 ms·

I think it's two things. The first one is that most people are not comfortable changing up the programming paradigm that they are most familiar with. They're

I think it's two things. The first one is that most people are not comfortable changing up the programming paradigm that they are most familiar with. They're familiar with adding some if-statements to verify at run time. They're not familiar with using the type system to prove the properties of their data. Proving non-trivial properties can be hard (and in some cases impossible), so it makes sense that few people are jumping at the opportunity to learn everything from the ground up all over again when the alternative is to just use an if-statement. The second thing is that sometimes you're going to get dynamic data at run time and you're going to have to use a run time property checker anyways. So for example if you needed to parse a bunch of text sent in by the user. You can still use dependent types to offload as much as possible to the type system, but at some point you'll have to deal with receiving user data. And if we go back to my first point, people are uncomfortable with using new things. They won't have a good idea of when to put what into the type system and what into the run time, so the default will be to just do it all at run time. Liquid types look kind of promising, but I'm not sure if it's still an active research area. The stuff rust is doing with affine types is also promising. It's not dependent, but you can make a bunch of very nifty compile time checked apis. Finally, ML style types are slowly becoming more familiar in general in the industry. Once everyone is fully familiar with type parameters, they'll start to ask about kinds and values in types. However, it may take a while.

lomnakkus 9y ago
> You can still use dependent types to offload as much as possible to the type system, but at some point you'll have to deal with receiving user data. 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.)
- jwdunne 9y ago
  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.
- pron 9y ago
  > 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. [1]: https://checkerframework.org/manual/#tainting-checker https://checkerframework.org/manual/#tainting-checker
  - catnaroek 9y ago
    It's useless if it's optional.
    - pron 9y ago
      So is F#.
      - catnaroek 9y ago
        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.
        pron 9y ago
        I meant that F# itself is optional. So are tests, by the way, and therefore also completely useless.
hinkley 9y ago
There really does seem to be a Last Mile problem with a lot of these systems for formalism. You're going to get garbage data from paying customers. With a good information architecture you'll have 'lines' in the system and all of the data that goes past a certain point is guaranteed to be sanitized, at which point all this formalism helps you avoid really bad mistakes. What ends up happening most times is a set of proprietary bespoke thunking layers that progressively sanitize the data until its usable. Everybody writes their own and they either suck or took lots of effort to get right. Or, the entire system is full of uncertainty and reads like a Choose Your Own Adventure as written by a squirrel. Maybe there's a space there between the user and the formal type system that needs a set of transformation tools. Like htmltidy, but without the html.

lomnakkus 9y ago

> You can still use dependent types to offload as much as possible to the type system, but at some point you'll have to deal with receiving user data. 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.)

jwdunne 9y ago
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.
pron 9y ago
> 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. [1]: https://checkerframework.org/manual/#tainting-checker https://checkerframework.org/manual/#tainting-checker
- catnaroek 9y ago
  It's useless if it's optional.
  - pron 9y ago
    So is F#.
    - catnaroek 9y ago
      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.
      - pron 9y ago
        I meant that F# itself is optional. So are tests, by the way, and therefore also completely useless.

hinkley 9y ago

There really does seem to be a Last Mile problem with a lot of these systems for formalism. You're going to get garbage data from paying customers. With a good information architecture you'll have 'lines' in the system and all of the data that goes past a certain point is guaranteed to be sanitized, at which point all this formalism helps you avoid really bad mistakes. What ends up happening most times is a set of proprietary bespoke thunking layers that progressively sanitize the data until its usable. Everybody writes their own and they either suck or took lots of effort to get right. Or, the entire system is full of uncertainty and reads like a Choose Your Own Adventure as written by a squirrel. Maybe there's a space there between the user and the formal type system that needs a set of transformation tools. Like htmltidy, but without the html.