AFAIK using dependent records-as-modules in a simpler MLTT-based type systems is tricky, because singleton types (aka. 'manifest fields') usually depend on equality reflection. Has anyone applied cubical type theory to the problem of first class module systems?
Conversation
What does 'module' mean here?
1
In the sense of an ML-style module. Where you have ‘module types’ (known in SML as a ‘signatures’), ‘module instances’ (known in SML as a ’structures’), and ‘module functions’ (known in SML as ‘functors’):
1
There's an excellent chapter about the design of module systems in Benjamin Pierce's “Advanced Topics in Types and Programming”. The design and history of Standard ML's modules are also covered in ”The History of Standard ML”:
1
1
There's been lots more work in module systems after SML though, regarding mixins, mutual recursion, combining the ideas with object oriented programming, etc. The design space can be a bit bewildering, and the nomenclature intimidating.
1
Ah, so it's very much a more specific term here than the more general use of 'module' in programming?
1
I have a conception of what a module is intuitively, but I've found it hard to pin down more formally, hence my curiosity here :)
1
Yeah, you can kind of think of these as 'fancy versions' of the modules you are normally familiar with in most PLs. You can give them types, and parameterize them, etc. They also can be extended to support typeclass style ad-hoc polymorphism.
1
But yeah, instead of a stratified module language I'd rather use dependent records, hence my question here. 🙂
1
1
If you want *really* formal, I just was just made aware of Bob Harper's recent supplement to PFPL which provides a description of an ML-style module system: cs.cmu.edu/~rwh/pfpl/supp
Replying to
Oh, cool! I've heard that PFPL is a little aged by now, but I'm assuming it's still worth reading? It's on my list.
1
Heheh, I just bought it (a few months ago), but haven't had a chance to look at it much. Tend to buy these things for my personal library so that they're on hand if I need them!
1
1
Show replies