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.
Replying to
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
Show replies