Correct 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.
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.