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
Replying to
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’):
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
Show replies