1SubMl: experimental ML-like programming language with a unified module and value language, and more
17 points by KnorrFG
17 points by KnorrFG
I think ideally a type system with this complexity should come with a mechanized formalization. This kind of thing used to be extremely difficult, and maybe it still is, but I'm hoping that Lean + the developments in AI (and agents etc.) will make this kind of thing easier and I'm dreaming of a future where every type system comes with a mechanized formalization that can parse the programs in the test suite, type check, and run, and a soundness proof (+ maybe proofs of other useful properties). In this idealized future, if a type system doesn't have the mechanization with proofs then by default we assume it's unsound.
IMHO there's just no way that you'll have a combination of all these features and just know, just by thinking hard and long enough, that it's sound.
(The same applies to the type system that I'm developing as well. It's much simpler that this one, but IMHO it's still complex enough to require a formal definition and proofs.)
(Yes I'm aware that a formalization separate from actual implementation does not prove the implementation is sound, it's still a big step forward towards formally verified language implementations.)
Edit: I think this should be tagged "plt" rather than "programming".
I think ideally a type system with this complexity should come with a mechanized formalization.
1SubML looks like it's based on 1ML (I'm struggling to find a citation (!), but it seems very similar). 1ML is an extension/implementation of a paper called F-ing Modules by Andreas Rossberg et al, and that paper comes with a Rocq formalization of the type system (see the Soundness Proof section in the link). Would love to know how this language compares to 1ML, and how it’s been changed / extended.
The structural subtyping aspect reminds me of PolySubML and some searchengineering led to https://github.com/Storyyeller/polysubml-demo by the same author, heh. And also https://blog.polybdenum.com/2025/11/13/polysubml-is-broken.html which is relevant to ~osa1’s point, and might explain the difference between PolySubML and 1subML. But I haven’t examined them in enough detail to see if the plan sketched at the end of the blog post is what is implemented by 1subML.
Another precursor is Stephen Dolan’s algebraic subtyping in MLsub.
Very neat! Looks like it compiles to JS and possibly some wasm, interesting choice of backend but it makes sense if you want a web playground.
Wish there was more theoretical discussion and citations in it though.
Very good work. Is it sound tho? I love the existential type take on modules, reminds be of TAPL from peirce