3 ms·
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
by vorotato 9y ago
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 https://news.ycombinator.com/item?id=7567310
- vorotato 9y agoit 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.