SMLFamily / Successor-ML

A version of the 1997 SML definition with corrections and some proposed Successor ML features added.
191 stars 10 forks source link

definitions and sequencing #11

Open RobertHarper opened 8 years ago

RobertHarper commented 8 years ago

I would say that one thing we've learned is that combining two aspects of a val binding into one is a mistake. On one hand val is used as a definition mechanism that induces polymorphism in accordance with the substitution principle. On the other hand val is a "monadic bind" that enforces sequencing of evaluation, which is particularly important when using effects. The two coincide when the rhs is a value, but we know that this simple-minded criterion is just that, especially in the presence of data abstraction. A classic example is to do with an abstract type of parsers, which are "in reality", functions, but abstractly are not, and this screws up the "value restriction" greatly.

Why not separate the two roles? We could have "val" for sequencing, and "def" for polymorphism. The semantics is clear, and never ambiguous, and you never have to fight the value restriction.

A related point is to change the syntax from "let dec in exp end" to "dcl dec in exp end". People hate "let val x = ...", which I find quite nice, but maybe "dcl" is better, especially now that we have "do" as a possible form of declaration, which I also find quite nice. "dcl" stands for "declare", and it's first argument is indeed a declaration.

YawarRaza7349 commented 7 months ago

I like separating those two aspects of val, but I don't see how it helps with the value restriction. You still need to prevent def r = ref nil (unless you were going to make uses of nilary defs call-by-name, which could be confusing...). The rules to do that would also ban def l = nil @ nil or whatever use of combinators you were thinking for your abstractly-typed parsers example. I'm not sure if you were thinking of having separate def specs in signatures as well, but I don't think that helps with this.