I'm very much a newbie when it comes to F# but as far as I can tell this isn't an example of what's traditionally called dependent types, but rather is a way of providing a set of helper functions and types for "smart" constructors, that is providing a validation/verification function that takes in some raw type and gives back an option of either the type you want or none.
As a litmus test (and I'd be happy if either the OP or someone else chimes in), as an example of dependent types, I'd expect to be able to compose constraints, e.g. having a type called
And<'A, 'B>
and
Or<'A, 'B>
that would then let me compose constraints e.g.
And<GreaterThan3, IsEven>
and crucially have their verification functions automatically compose as well, instead of having to invent a whole new type
GreaterThan3AndIsEven
with a whole new verification function.
As far as I can tell right now, that's not possible with this library and I need to go down the route of making the custom GreaterThan3AndIsEven type.
Another good litmus test is whether literals also need to be passed through the verification function or not (or whether you have to pass them through the verification, get an option, and then unwrap the option with a comment indicating that it's safe to do so); for a usage of dependent types I would expect the answer to be no usage of the verification function would be required.
The crucial thing that dependent types let you do is that you can manipulate types and values with many of the same tools. Composition (the and and or from above) is one hallmark of this ability. Another is being able to call a value-level function in a type signature. For example a type signature that looks like
x : if (a + b == c) then Boolean else Int
FWIW I don't mean to take away from this library; the practice of using smart constructors is something I'd love all expressively statically typed languages embrace wholeheartedly.
Since Martin-Löf type theory has introduced dependent types through the dependent function. No one I am aware of has improved on this approach, or even attempted a different way of introducing dependent types. And I think theory is very important.
In Practice I think https://en.wikipedia.org/wiki/Dependent_type gets it right in that dependent types exist independently of dependent functions. [A] dependent type is a type whose definition depends on a value. I think ordinary programmers solving ordinary problems benefit far more from the type safety dependent types provide than dependent functions or compile time creation checks. In ordinary programming most data is independent of the code. There are notable exceptions, of course.
If in practical programming we may only ever use a term from computer science when it meets the CS definition in every way, I invite the reader to start a list of all the terms where this is already not the case.
Also ordinary programmers are more likely to gain at least a superficial understanding of dependent types when every implementation of smart constructors does not call the resulting types something specific to that programming language, but otherwise unconnected to most anything else.
Constructor composition is a neat idea and merits investigation. The idea of course springs from function (dependent function) composition. Not exactly what you are thinking, but I think somewhat related, take a look at the section Converting between dependent types in the tutorial https://jackfoxy.github.io/DependentTypes/tutorial.html
I agree with I think what you're hinting at with regards to practicality. It is definitely the case that using this library or the practices that it espouses is far more practical for the working programmer than to try to get people to rework rewriting their codebase in Coq.
That being said, if I understand this library correctly, I strongly disagree with the choice to call it "Dependent Types." There's certainly no inherent reason that a cabal of type theorists should have a monopoly on the word "dependently typed," but I think describing this library as dependently typed dilutes the meaning of this word beyond usefulness. The crucial idea behind this library can be implemented in every statically typed language I know of (essentially anything that supports hiding certain constructors and exposing alternate ones and using some sort of optional type to represent failure rather than blow up at runtime). The specific implementation details of storing all the functions together can certainly be approximated in every statically typed FP language I've used (which is not to say it isn't valuable or a unique take on the problem!). Under what I think is your definition of dependent types, Java is a dependently typed language, which really starts muddying the waters for programmers trying to learn this stuff. This has two main drawbacks.
1. It obfuscates what this library is doing to programmers who have not used dependent types before. The mix of questions in this very HN thread, some of which are more appropriately directed at a language like Idris, is a testament to that. Once again depending on whether I understand this library correctly, this library seems to be an extension of the idea of having separate public and private constructors for types and codifying the public constructors for a type. This is something that I would wager most working programming have some familiarity with and can immediately understand its usefulness instead of having to ask around (and get irrelevant answers) about what dependent types are.
2. It disappoints and confuses people who have used dependent types. Honestly it comes off as buzzword marketing. An analogy would be if someone took the C language and added a new word "class" that was a synonym for "struct," did absolutely nothing else, then proclaimed that C was object-oriented (a term which is far less well-defined than dependently typed). "Ah so do your new C OO classes support inheritance?" "Nope." "Hmmm... so do you have methods?" "Nope." "Well then they aren't really classes and it feels disingenuous to call them such... (unlike e.g. how C++ extends the semantics of struct)."
If what you're talking about RE Martin-Löf type theory and the dependent function are pi and sigma types sure that's the formal treatment of dependent types, but I'd argue that there's a simpler working definition that suffices for most cases. A dependently typed language is simply a language where expressions not only can have a type, but can evaluate to a type. Hence my "if ... then ..." example from earlier.
I think the most accurate, widely-used term that describes what's going on here is the factory pattern. Simple as that and I think that's familiar enough to most programmers.
Upon re-reading this comment, I want to say that I don't think this library is trivial (it's not "just" the factory pattern) and that it is definitely a valuable way of structuring a given pattern! I know putting something on HN is a great way of getting crowds of know-it-alls to heckle and discourage you so I hope I haven't done that, just wanted to point out something that was bothering me.
As a litmus test (and I'd be happy if either the OP or someone else chimes in), as an example of dependent types, I'd expect to be able to compose constraints, e.g. having a type called
and that would then let me compose constraints e.g. and crucially have their verification functions automatically compose as well, instead of having to invent a whole new type with a whole new verification function.As far as I can tell right now, that's not possible with this library and I need to go down the route of making the custom GreaterThan3AndIsEven type.
Another good litmus test is whether literals also need to be passed through the verification function or not (or whether you have to pass them through the verification, get an option, and then unwrap the option with a comment indicating that it's safe to do so); for a usage of dependent types I would expect the answer to be no usage of the verification function would be required.
The crucial thing that dependent types let you do is that you can manipulate types and values with many of the same tools. Composition (the and and or from above) is one hallmark of this ability. Another is being able to call a value-level function in a type signature. For example a type signature that looks like
FWIW I don't mean to take away from this library; the practice of using smart constructors is something I'd love all expressively statically typed languages embrace wholeheartedly.