4 ms·
How do you express the type `Vect 3 Int` using this library? F# doesn't support it and all the example types appear to depend on other types, not on values like
by lkitching 9y ago
How do you express the type `Vect 3 Int` using this library? F# doesn't support it and all the example types appear to depend on other types, not on values like 3.
- jackfoxy 9y agoI'm pretty sure there are vector libraries available to F#. Dig around and you will find them. Then just apply dependent type to a type in that library. I don't work with them myself.
- lkitching 9y agoI'm not asking specifically about vectors, that's just a common example of a dependent type. To take another example from the documentation, can you express a type like type digits = RegexString (Regex "^[0-9]+$") where all values of type digits are strings containing only digits? Then let s1 : digits = "1234" would typecheck but let s2 : digits = "abc" would not? That would be very surprising given the F# type system.
- vorotato 9y agoBasically 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.