News for hackers. Stuff that matters.
Re:Dependent Types for F# by pron on Tuesday December 05, 2017 @04:58PM (#15856424)
> 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

Re:Dependent Types for F# by catnaroek on Tuesday December 05, 2017 @10:55PM (#15858337)
It's useless if it's optional.
Re:Dependent Types for F# by pron on Wednesday December 06, 2017 @03:08AM (#15859432)
So is F#.
Re:Dependent Types for F# by catnaroek on Wednesday December 06, 2017 @07:25AM (#15860555)
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.
Re:Dependent Types for F# by pron on Wednesday December 06, 2017 @10:32AM (#15861798)
I meant that F# itself is optional. So are tests, by the way, and therefore also completely useless.
Re:Dependent Types for F# by catnaroek on Wednesday December 06, 2017 @10:07PM (#15867306)
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!