Dependent Types for F#

Re:Dependent Types for F# by jackfoxy on Tuesday December 05, 2017 @12:30PM (#15853445)

I'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.

[ Parent | on HN ]

Re:Dependent Types for F# by lkitching on Tuesday December 05, 2017 @12:56PM (#15853826)

I'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.

[ Parent | on HN ]