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