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
And these kinds of tweets remind how much more I still need to learn about PL. Though I do plan to include OCaml modules in my next video (after the interview coming out shortly).
1
3
I think module systems are fascinating! But also the way they are presented is often rather confusing, with bewildering set of terminology to learn. I hope we can make this stuff more approachable in the future!
1
1
I think Futhark's syntax for modules is really good in this regard, in terms of simplifying things: futhark-book.readthedocs.io/en/latest/lang
1
2
Also worth checking out 1ML, which uses records as first-class modules: mpi-sws.org/~rossberg/1ml/
1
1
Why3 has some really cool features around 'cloning' modules: why3.lri.fr/doc/syntaxref.
1
2
Ultimately I would love to see us upgrade term-languages to support the same sort of stuff we enjoy in module systems, so that we don't need separate terminology and language features for the module level vs the term level.
Eg. 'functors' in ML modules should just be 'functions'. 😊
2
1
Note that you might need to add something else to allow for separate compilation and phase separation - this is what interests me about things like two-level type theory, multistage programming, and projects like