3 ms·

Does this library actually allow you to express dependent types or is it just for runtime validation? I can't see any examples in the documentation of a type de

Does this library actually allow you to express dependent types or is it just for runtime validation? I can't see any examples in the documentation of a type depending on a value like the common let v : Vect 3 Int = [1,2,3] example. There aren't many types shown in the examples but it looks like let myNonEmptyIntSetOpt = [] |> Set.ofList |> NonEmptyIntSet.TryCreate would just return None at runtime rather than a compilation error?

jackfoxy 9y ago
How can you do a compile time check on data that has not entered the system? You can apply the same technique to Vect 3 [1,2,3] or any other type.
- jackfoxy 9y ago
  a dependent type is a type whose definition depends on a value https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
- 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 ago
    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.
    - lkitching 9y ago
      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.
  - 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 ago
      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.
- deleted 9y ago
  [deleted]
- cstrahan 9y ago
  > How can you do a compile time check on data that has not entered the system? You would have to supply proof that your types are correct; when you have a value who's type you'll only know at run time, you'll need to perform case analysis to bring additional info about the value's type into scope in the respective branches. To make concrete what I'm describing here, I'll use Idris's ++ (concatenation) as an example, which provides an inductive proof for the length of the resulting vector: (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) [] ys = ys (++) (x::xs) ys = x :: xs ++ ys The first line is the type signature, which claims that the length of the resulting vector is the sum of the lengths of the two argument vectors. The second line pattern matches on the null/empty constructor of the vector, and then returns ys. By pattern matching on the null constructor, we know that m == 0. We also know that n == length ys (whatever that may be). We know that 0 + x = x, so if we apply that to this case, we know that: length ([] ++ ys) == length [] + length ys == 0 + length ys == length ys == n == m + n (because we know m==0, and 0+n==n) ... so the compiler is happy here. The third and final line pattern matches on the non-empty (or cons, if you're a fan of Lisp) constructor. If this pattern applies, then we can make use of the fact that length (x::xs) == 1 + length xs. Of course, that that implies length xs < length (x::xs). That permits us to apply our induction hypothesis to the (xs ++ ys) sub expression, which tells that length (xs ++ ys) == length xs + length ys. Putting all of that together, we see that length (x :: xs ++ ys) == 1 + length (xs ++ ys) == 1 + length xs + length ys == 1 + (m - 1) + length ys == m + length ys == m + n That concludes our proof by induction[1]. Note that this proof is checked completely at compile time, and that it is still valid in the face of types which we won't know until we run our program. That's what dependent types give you. Here's an example that would not compile: (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) [] ys = ys (++) (x::xs) ys = x :: x :: xs ++ ys {- !!! note that I cons x here *twice* -} In conclusion, your library sounds like it could be an excellent way to provide smart constructors; at the same time, it's important to not conflate smart constructors with dependent types. I would urge you to continue developing your library, though I would recommend switching the name to something that's more indicative of what it actually does. That would have the additional benefit of not confusing people who read your project description and are hearing about dependent types for the first time. [1]: https://en.wikipedia.org/wiki/Mathematical_induction https://en.wikipedia.org/wiki/Mathematical_induction

jackfoxy 9y ago

How can you do a compile time check on data that has not entered the system? You can apply the same technique to Vect 3 [1,2,3] or any other type.

jackfoxy 9y ago
a dependent type is a type whose definition depends on a value https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
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 ago
  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.
  - lkitching 9y ago
    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.
- 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 ago
    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.
deleted 9y ago
[deleted]
cstrahan 9y ago
> How can you do a compile time check on data that has not entered the system? You would have to supply proof that your types are correct; when you have a value who's type you'll only know at run time, you'll need to perform case analysis to bring additional info about the value's type into scope in the respective branches. To make concrete what I'm describing here, I'll use Idris's ++ (concatenation) as an example, which provides an inductive proof for the length of the resulting vector: (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) [] ys = ys (++) (x::xs) ys = x :: xs ++ ys The first line is the type signature, which claims that the length of the resulting vector is the sum of the lengths of the two argument vectors. The second line pattern matches on the null/empty constructor of the vector, and then returns ys. By pattern matching on the null constructor, we know that m == 0. We also know that n == length ys (whatever that may be). We know that 0 + x = x, so if we apply that to this case, we know that: length ([] ++ ys) == length [] + length ys == 0 + length ys == length ys == n == m + n (because we know m==0, and 0+n==n) ... so the compiler is happy here. The third and final line pattern matches on the non-empty (or cons, if you're a fan of Lisp) constructor. If this pattern applies, then we can make use of the fact that length (x::xs) == 1 + length xs. Of course, that that implies length xs < length (x::xs). That permits us to apply our induction hypothesis to the (xs ++ ys) sub expression, which tells that length (xs ++ ys) == length xs + length ys. Putting all of that together, we see that length (x :: xs ++ ys) == 1 + length (xs ++ ys) == 1 + length xs + length ys == 1 + (m - 1) + length ys == m + length ys == m + n That concludes our proof by induction[1]. Note that this proof is checked completely at compile time, and that it is still valid in the face of types which we won't know until we run our program. That's what dependent types give you. Here's an example that would not compile: (++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem (++) [] ys = ys (++) (x::xs) ys = x :: x :: xs ++ ys {- !!! note that I cons x here *twice* -} In conclusion, your library sounds like it could be an excellent way to provide smart constructors; at the same time, it's important to not conflate smart constructors with dependent types. I would urge you to continue developing your library, though I would recommend switching the name to something that's more indicative of what it actually does. That would have the additional benefit of not confusing people who read your project description and are hearing about dependent types for the first time. [1]: https://en.wikipedia.org/wiki/Mathematical_induction https://en.wikipedia.org/wiki/Mathematical_induction