juvix
juvix copied to clipboard
Add applicative do notation
Applicative do notation is similar to monadic do notation with a few differences:
- Only pure expressions and bind statements are allowed. I.e., there are no let statements.
- Last statement must be of the form
pure lastExpr
. We could discuss how to handle this. Maybe thepure
could be implicit. - Variables bound in a bind statement are only in scope of the last expression in the block.
- We use a different keyword. E.g.
ado
.
ado {
opt1 <- getOpt1
opt2 <- getOpt2 -- opt1 is not in scope here
pure Options.mk@{
opt1;
opt2;
}
}