ML-style module systems are lots of fun haha
Conversation
it’s super useful. i also like haskell’s approach where libraries can specify an interface and the application author just specifies a module that satisfies that interface. i’ve never used it but i think it would get me 95% of the way there
2
2
also i read a fun paper a long time ago describing how to recreate the ML module system using sigma types but i can’t find it. also there’s this:
1
2
Replying to
Yeah, modules are pretty much dependent records under the hood with some extra stuff too!
Replying to
yeah one of my coworkers was actually using the ocaml module for proofs but there’s some limitations that make it impractical
Like sometimes there is a phase distinction (separating the module language from the runtime language), sometimes an ability to ‘seal’ records, and add sharing constraints as well. But yeah I like the idea of making the module language more consistent with the term language.
2