Very cool, I'll dig into this later. I've been meaning to gain a better understanding of dependent typing. Been working on an SML clone with first class modules

Very cool, I'll dig into this later. I've been meaning to gain a better understanding of dependent typing. Been working on an SML clone with first class modules (ala 1ML/F-ing modules), and I understand that the module language is typically modeled with dependent types. It's been challenging to try to enable modules-as-existentials without too much compiler-side hackery going on.