-
Notifications
You must be signed in to change notification settings - Fork 111
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, defined by:
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 M: for M(v from A):
v from A ==> for M:
REST... REST...
end end
end
for M: for M(_ from A):
do A ==> for M:
REST... REST...
end end
end
for M: X
X ==> for M:
REST... REST...
end end
for M:
do A ==> A
end
for M:
X ==> X
end
(where REST is non-empty in each case.)
Remember that regular for-statements desugar by
for A(v from B):
REST... ==> A(B, fun(v): REST...;)
end
In this proposal, the notation uses the keyword 'for', but this is potentially confusing, and can also be ambiguous:
for foo():
1 + 2
end
A different final keyword should probably be chosen.
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.
There's an even more radical notation possible, that would eliminate the for:
v from X
REST... ==> X(fun(v): REST...)
do X
REST... ==> X(fun(_): REST...)
This effectively allows for-notation in any block, requires you to name the "monad" in each from-statement, and allows multiple "monads" to be mixed within a block. (Of course at this point these functions don't look like monads at all, but you know what I mean.) Using this from-notation, you could improve this code (using for-notation):
fun get-pwd():
for 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)
do "Ok, now what's the password?" # prompts for a password, but there's no way to star-out the user's reply
end
end
into this (using from-notation):
fun get-pwd():
first-name from prompt("What's your first name?")
last-name from prompt("What's your last name?")
full-name = first-name + " " + last-name
print("Hello, " + full-name)
do prompt-password("Ok, now what's the password?") # prompt-password stars-out the user's reply as they type
end
Mixing monads gets messy, though, so I suspect we wouldn't actually want to use this notation. Just putting it out there as a thought experiment.