News for hackers. Stuff that matters.

A comment on Dependent Types for F#. Parent comment

Re:Dependent Types for F# by vorotato on Tuesday December 05, 2017 @12:32PM (#15853469)
Basically when you take some value the user gives you and cast it to the dependent type, you can then cover the case where you got some result because the cast was successful or you got none. You can't have dependent types at compile time, at least not completely so, though you could use something like fslint to catch any data being entered in code.

https://news.ycombinator.com/item?id=7567310

[ Parent | on HN ]
Re:Dependent Types for F# by vorotato on Tuesday December 05, 2017 @12:39PM (#15853585)
it would seem that in practice you can go even further, essentially writing exhaustive proofs. However F* already supports this and compiles to F#, so I would say if you want that level of correctness you should probably use a language which is better at describing the totality of a function.
[ Parent | on HN ]