TM012 Do notation

Motivation

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

Examples

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

Specification

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

Name

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.

Confusion with for-statements?

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

Error Messages

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.

Comparison to Haskell's do-notation

There are four pertinent differences with Haskell's do-notation:

The syntax is different: for instead of do, and from instead of <-. This syntax is good because it forms an (accurate) analogy with for statements:
```
 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

return isn'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 that bind is associative, which in Pyret's case would say that
```
 for 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.

From-notation: A radical extension

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.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly