In the software verification community, it is quite common to supplement every new approach with a real-world case study. I wish this practice were more common in the PL world (and especially in the FP world) -- though I realize the cost of a case study are much higher when a new language is involved -- because here's the general problem with a language that relies so heavily on advanced type systems:
We know that verifying any property of a program has a computational complexity cost, and we know that that cost is very high (the problem is PSPACE-complete even for languages that are very far from Turing complete). When types are involved and the program's property is correct by construction, that complexity does not go away (it can't; that would violate a mathematical law), it is just transferred elsewhere: to the machine doing the constructing. So when I come up with an algorithm and decide to verify one of its properties by encoding it in the type -- in Ling, Idris or whatever -- the verification complexity is incurred by the machine performing the verification, which is composed of two parts: the compiler, which shares just a bit of the burden, and my brain, which incurs the lion's share. So coming up with a new type system (like built-in session types) is basically coming up with a new verification algorithm that is to be run by the human brain. As we know the complexity of general verification is humongous, all we can hope for -- as with any verification approach -- is that our approach would be tractable for a certain class of programs (which is why verification algorithms require case-studies). So as we run our verification algorithm not on a von Neumann machine but on a biological computer, we need to study how our approach runs on that machine; without such a study, our approach is no more than a conjecture of effectiveness. Not that raising conjectures isn't interesting, but it's a far cry from showing the way forward.
A type system that is not accompanied by results of the effectiveness of its verification algorithm on the machine that's going to run it -- namely our brains -- is an outline of an algorithm with no complexity analysis or any actual runs on a computer. A type system without a case study is no more than saying "this is an algorithm which we believe may be effective on such-and-such inputs". The only possible response is to say, "hmm, interesting!" and to move on, because we really have no way of evaluating this.
I'm going to ask these here because I don't know where to ask them. Because HNers are smart. Please don't think this is off-topic!
1) What would a database system look like that had an advanced type system that could specify user defined data types? Is this what an object-oriented db is? Is this possible with graph databases? Relational databases? Hierarchical databases?
2) What would type reusability look like? Not code reusability, not object reusability, but type reusability. Does this even make sense?
3) Would it be possible for multiple different languages to share a type system?
4) Would it be possible for the one language to have multiple type systems? (Pluggable, modular, if you see what I mean)
1. disregarding "advanced" because thats subjective, you can think of a new type in a relational database as a table, where instances of that type are rows.
2. assuming by type reusability you mean something like polymorphism, sql affords subtype polymorphism through "disjoint subtyping" which means a single table which tracks multiple sub-tables, with a single entry existing in at most 1 of these sub-tables. sql also offers a limited row polymorphism through select and views.
3. assuming you're talking about all programming languages, yes. that doesn't mean instances of those types are shareable between languages.
4. yes. several interpreted languages have competing and optional type systems.
