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.
1
1
Eg. 'functors' in ML modules should just be 'functions'. 😊
2
1
Can I introduce you to Scala? (Sorry, couldn't help it). I think that's a natural conclusion of that thought, unless you're willing to add stratification.
1
2
Yeah I'm a big fan of Scala, especially the DOT stuff! I want full spectrum dependent types as well though 🥺