wow, comprehensive! I personally think type systems are most useful for their more reliable feedback loops (compared to value-level programming), and they only have such reliable feedback loops because they are restricted and simple.
i think things like dependent types and multi-stage programming are good lines of research because types become first-class constructs with full tool support, but complex second-class type languages seem like a dead end to me.
Ah yeah, these are a lot of the same projects I've been following 😊
I think Julia and Terra are interesting too, approaching similar ideas by starting with a dynamic language and then adding type-checking stages in.
