3 ms·
F* + 1ml (https://people.mpi-sws.org/~rossberg/1ml/ https://people.mpi-sws.org/~rossberg/1ml/) would be the ultimate experience. I was born too early!
by unstruktured 2y ago
F* + 1ml (https://people.mpi-sws.org/~rossberg/1ml/ https://people.mpi-sws.org/~rossberg/1ml/) would be the ultimate experience. I was born too early!
- wk_end 2y agoCorrect me if I'm wrong (I've only dabbled in F* and only briefly read about 1ML) but wouldn't F*'s full dependent types make 1ML redundant? That is, once you've brought types into the value level, modules themselves become redundant - they're just records, and functors are just functions. The point of 1ML, IIUC, is to accomplish a similar unification without demanding full dependent types and the attendant complexities they bring.
- unstruktured 2y agoInteresting point. I never inferred a strong connection between dependent types and the unification of records and modules. Maybe a real PL theorist around here can provide insights on that subject.