-
Notifications
You must be signed in to change notification settings - Fork 110
TM012 Do notation
Consider this piece of code in store-passing style:
data Expr:
| num(n :: Number)
| add(left :: Expr, right :: Expr)
end
fun eval(expr, s):
cases(Expr) expr:
| num(n) => {v: n, s: s}
| add(expr1, expr2) =>
v-s1 = eval(expr1, s)
v-s2 = eval(expr2, v-s1.s)
{v: v-s1.v + v-s2.v,
s: v-s2.s}
end
end
The style of passing the ss around is repetitious and error-prone (it would be easy to pass the wrong store into one of the calls to 'eval'). It would be useful to have something akin to Haskell's do-notation to help with situations like this. It can already be approximated using Pyret's for statements:
fun with-store(body, evaluation):
fun(s):
v-s = evaluation(s)
body(v-s.v)(v-s.s)
end
end
fun return-val(val):
fun(s): {v: val, s: s};
end
fun eval(expr):
cases(Expr) expr:
| num(n) => return-val(n)
| add(expr1, expr2) =>
for with-store(n1 from eval(expr1)):
for with-store(n2 from eval(expr2)):
return-val(n1 + n2)
end
end
end
end
Now all of the store-passing is implicit, so this code is less error-prone. It is still repetitious, though: see that with-store appears multiple times. And the nested indentation is syntactically ugly.
This proposal is to add a new for-notation syntax that would let you instead write:
fun eval(expr):
cases(Expr) expr:
| num(n) => return-val(n)
| add(expr1, expr2) =>
for with-store:
n1 from eval(expr1)
n2 from eval(expr2)
return-val(n1 + n2)
end
end
end
for with-prompt:
first-name from "What's your first name?"
last-name from "What's your last name?"
full-name = first-name + " " + last-name
print("Hello, " + full-name)
end
# The original motivating example, from unification in my (Justin's) resugarer:
for try-unify(r-head from unify-list(head, q0.head)):
for try-unify(r-upper from unify-list(upper, q-upper)):
for try-unify(r-body from unify(p0.rep, q0.rep)):
for try-unify(r-lower from unify-list(lower, q-lower)):
for try-unify(r-tail from unify-list(tail, q0.tail)):
p-rep(r-head + r-upper, r-body, r-lower + r-tail)
end
end
end
end
end
# ...becomes...
for try-unify:
r-head from unify-list(head, q0.head)
r-upper from unify-list(upper, q-upper)
r-body from unify(p0.rep, q0.rep)
r-lower from unify-list(lower, q-lower)
r-tail from unify-list(tail, q0.tail)
p-rep(r-head + r-upper, r-body, r-lower + r-tail)
end
contents = for with-option: # `contents` gets an option
f from file.open("config") # say that `open` returns an option
s = f.read()
some(s.strip-whitespace())
end
There would be a new syntactic form for statements:
for <expr>:
X
Y
...
where X, Y, ... (collectively called a for-block) would be either regular statements or from-statements:
v from <expr>
There could be an additional piece of syntax for from-statements whose result is discarded:
do <expr> ==> _ from <expr>
It would be a well-formedness error for the last statement in a for-block to be a from-statement, but not for it to be a do-statement. For-blocks may not be empty.
The desugaring would be defined as follows:
for A:
v from B ==> B
end
for A: for A(v from B):
v from B ==> for A:
REST... REST...
end end
end
for A: X
X ==> for A:
REST... REST...
end end
Remember that regular for-statements desugar by
for A(v from B):
REST... ==> A(B, fun(v): REST...;)
end
For-notation will not play well with nullary functions. e.g.,
for trace:
1 + 2
end
is equivalent to
1 + 2
which is very different from what the author probably intended:
for trace():
1 + 2
end
which is equivalent to
trace(fun(): 1 + 2;)
This suggests making it a well-formedness error for a for-block to contain no from-statements (since otherwise it's equivalent to just inlining the statements.).
With an appropriate type-annotation, error messages should at least be reasonable. In the store-passing example, the body argument should be annotated to say that it always returns a {v, s} object:
fun with-store(body :: Val -> Store -> ValStore, evaluation):
fun(s):
v-s = evaluation(s)
body(v-s.v)(v-s.s)
end
end
If a user then made a mistake such as writing n1 + n2 instead of return-val(n1 + n2), an exception would be raised that pointed to the application site of with-store, which would include the problematic n1 + n2 expression.
There are four pertinent differences with Haskell's do-notation:
-
The syntax is different:
forinstead ofdo, andfrominstead of<-. This syntax is good because it forms an (accurate) analogy withforstatements:for M: v from X f(v) end
is equivalent to
for M(v from X):
f(v)
end
-
By default, statements inside a for-block are non-monadic, whereas in Haskell they are by default monadic. For instance, you can write
for with-store: n1 from eval(expr1) print("hello") n2 from eval(expr2) return-val(n1 + n2) end
even though print("hello") doesn't return a {v, s} object. The equivalent code in Haskell wouldn't type-check. If instead you wanted to put a monadic piece of code in the middle, like eval(expr3), you could use a 'do' statement:
for with-store:
n1 from eval(expr1)
do expr3
n2 from eval(expr2)
return-val(n1 + n2)
end
-
returnisn't built-in. Instead, each function used in a for-notation may have its own return function (or many such functions, or none at all). This also allows each return function to have a more appropriate name than "return". -
The monad laws need not be obeyed. Without a required
return, the only remaining law is thatbindis associative, which in Pyret's case would say thatfor M: X for M: Y Z end end
is always equivalent to
for M:
for M:
X
Y
end
Z
end
The Haskell wiki gives a good summary of why these laws are useful in the first place: "Whether compilers exploit the laws or not, you still want the laws for your own sake, just so you can avoid pulling your hair for counter-intuitive program behaviour that brittlely depends on how many redundant returns you insert or how you nest your do-blocks.".
Since the compiler can't verify the laws, I (Justin) would suggest it be considered best-practice to only use for-notation with functions that obey the laws, but not make any hard assumptions in the compiler, and let users know that the above equivalence is not guaranteed.