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.

a dependent type is a type whose definition depends on a value https://en.wikipedia.org/wiki/Dependent_type

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.

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

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.

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.

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.

> 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