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