Curious: from what I can see, a type system is really just an embedded declarative DSL for doing set algebra. So is there a technical reason why education and implementations always intertwine it with a larger client language, rather than treating it as a complete, self-contained entity in its own right? Or is that lack of decomposition just oversight?
Try it yourself. It's much more difficult than you seem to think it is.
Well, isn’t that true of everything? Being a bear of very little brain, it’s why I’m always searching for ways to decompose the larger problem into smaller, simpler, self-contained chunks. Plus, a less common perspective sometimes yields insights that the mainstream may miss.
Thanks for the inputs, folks. Will cogitate further.