Undo

Undo is an esoteric programming language based on Unlambda. The main differences are that Undo uses lazy evaluation instead of eager evaluation, and that the way I/O works is different; instead of using side effects, it uses a system inspried by Haskell's monadic I/O. (The "do" in the name comes from Haskell's do keyword.)

Because of what's similar and what's different, many Unlambda programs will be valid Undo programs but behave differently (e.g. not producing the proper output or terminating early), and vice versa.

Knowing Unlambda and knowing about monads will be helpful in understanding what is going on here.

Contents

• Basic syntax
• Basic combinators
• Input and output
  • Basic I/O actions
  • Combining I/O actions
  • Monad laws
  • =
  • Exiting
• Continuations
• Summary
• Interpreter

Basic syntax

A program is a single expression. An expression can be any of the following:

• One of the characters s, k, i, v, 1 (one), r, @, =, c, b, representing a built-in function.
• A dot (.) followed by any single character, representing a "print" function.
• `XY, where X and Y are valid Undo expressions, representing function application.

Whitespace is ignored (except after .) and # starts a single-line comment (again, except after .). Aside from the different set of built-in functions, this syntax is the same as Unlambda.

\ starts a single-line indication of the language version. For compatibility with future versions, programs should start with a line \undo1. Interpreters can use this to show a warning or error for unsupported versions or enter a compatibility mode, or they can treat it as another comment character.

Basic combinators

The basic combinators are s, k, i, v, and 1 (one), which satisfy the following:

• ```sXYZ = ``XZ`YZ
• ``kXY = X
• `iX = X
• `vX = v
• ``1XY = `YX (that's a one, not an ell)

s, k, i, and v are exactly the same as their Unlambda equivalents. This means that many algorithms for Unlambda will also work in Undo. In particular, abstraction elimination works the same, except that you don't need to worry about side effects or nontermination; and algorithms for working with things like numbers and data structures will continue to work as long as they don't involve I/O or the c function (or d or e).

Of these functions, 1 is the only new function. Like i and v, it's not strictly necessary; it can also be written ``s`k`si``s`kki. Its purpose will be discussed later, in the section on monad laws.

Input and output

Basic I/O actions

There are two (classes of) basic I/O actions:

• .X, for any character X, represents an action that prints a single character. Like in Unlambda, r is an alternative way of writing . followed by a newline. The result of a . action is v.
• @ represents an action that reads one character from the standard input. The result of an @ action is .X where X is the character read, or v if the end of the input has been reached.

While these look like Unlambda's I/O functions, they behave differently. Applying them to an argument doesn't perform their side effect; rather, it creates a new I/O action as described in the next section. To actually perform the action, the outermost expression in the program must evaluate to the action. For instance, the minimal program in Unlambda to print an asterisk is `.*i, whereas in Undo it's .* (which in Unlambda would do nothing). On the other hand, in Unlambda, `k`.*i would output an asterisk, whereas in Undo, it would output nothing since the expression evaluates to a partially-applied k rather than to an I/O action.

If the program evaluates to an expression that is not an I/O action or a continuation action (described in a later section), the program halts.

Note that the equivalence from lambda calculus where λx. f x = f (``s`kFi = F) does not hold when f is an I/O action; if the action is inside a partially-applied function, the interpreter will not see it.

Combining I/O actions

If I is an I/O action, then `IF is an I/O action that performs I and then evaluates `FR, where R is the result of the action, and performs the result of that as an I/O action.

This means that you can perform actions in sequence (ignoring their results) by applying the first action to `k of the second action, like this:

`.H`k`.e`k`.l`k`.l`k`.o`kr

…or, associating the other way:

`````.H`k.e`k.l`k.l`k.o`kr

For actions where you want the result (like @), you can instead put a non-constant function. For instance, `@i reads a character and interprets the result as an action and performs it; since the result of @ is a printing function, this will read one character from the input and then print it.

Monad laws

According to the Haskell documentation, monads satisfy the following properties:

1. return a >>= k = k a
2. m >>= return = m
3. m >>= (\x -> k x >>= h) = (m >>= k) >>= h

Translating these into Unlambda/Undo notation gives:

1. ``<bind>`<return>AK = `KA
2. ``<bind>M<return> = M
3. ``<bind>M^x``<bind>`K$xH = ``<bind>``<bind>MKH

As I talked about in the previous section, you can combine I/O actions simply by applying it to a function in the same way that Haskell's >>= operator works; that is, <bind> for Undo I/O actions is simply i. This means:

1. ``<return>AK = `KA
2. `M<return> = M
3. `M^x``K$xH = ``MKH

Notice that property 1 is just the definition for the 1 combinator; that means that 1 is the return function for Undo's I/O monad (this is why I defined a new combinator for that). That is, `1X behaves like an I/O action that does nothing and has the result X.

If an I/O action is applied to two arguments, then property 3 will be applied before performing the action.

If M is an I/O action, then `M1 will perform the action and then halt (because `1<anything> is not an action), so M and `M1 are the same in isolation. ``M1F simplifies to `M^x``1$xF = `M^x`F$x, so property 2 holds.

=

The = function takes two arguments and evaluates them. If the result of both arguments is an I/O action that prints a character next (as opposed to inputting or halting), and the first character printed by the actions is the same, then the result is k; otherwise it's `ki. (Or, thought of another way, ````=XYTF returns T if both X and Y output characters and output the same character, and F otherwise.)

The main intended use for this is when reading a character, where this serves the same purpose as Unlambda's ?X function. For instance, the program `@ ``s``s``s``s`k=i`k.a`k.y`k.n (`@ ^c ````=$c.a.y.n) reads a character from the input, and prints y if the character is a and n otherwise.

This can also be used for testing a boolean stored with Unlambda's i/v convention; since `i.a outputs a and `v.a doesn't, ``=`B.a.a will test if B is i or v.

Exiting

There's no exit function, unlike Unlambda 2; however, since function application is used for sequencing and `v<anything> is never an I/O action, v acts as an action that exits the program.

Continuations

I'm not sure how useful these are, since where continuations can be used is more restricted and I don't think c can be used to detect v. (Also, this hasn't been tested as much.)

The c function works similarly to Unlambda; `cF applies `F<cont>, where <cont> is the current continuation. However, both `cF and `<cont>X are treated as I/O actions and `F<cont> is expected to be an I/O action; the same rules about combining I/O actions apply here, too.

There is also a b function (bracketed continuation), which takes an expression involving continuations and evaluates it. If the result is X, then the result of the call to b is `Xi, because ``1Xi = X.

Summary

Comparison to Unlambda:

Rewrite rules: