## Ambidexter tutoriallesson 3coterms

In this lesson we will begin on "or types". Along the way, you will encounter "coterms" for the first time. First class coterms are the distinguishing characteristic of Ambidexter.

#### motivation: or types

The word "or" is commonplace as a logical connective.
"Pigs fly or pigs don't fly."
Even when not applied to statements, "or" is logical. For example, "The color of the apple is red or green," is not using the phrase "red or green" as a color. It is short for the disjunction in which "or" connects two propositions, "The color of the apple is red or the color of the apple is green."

Suppose we had a proof in which `String` and `Integer` represented propositions. We need a way to say `String or Integer`. In Ambidexter that's `    | String | Integer |`
Note the leap from proofs to programs, which will be a regular occurrence in these lessons, because propositions of logic correspond to types in programs.

Any logical form, to be practical, must have not only a way to prove it, but also a way to put that form to use. Analogously, any type in a programming language must have an "introduction rule" to create a value of that type, and an "elimination rule" to put the value to use.

Let's start with the latter. How would we put `String or Integer` to use? The simplest thing would be to split the entire remainder of the proof or program into (1) what we do if we have a `String`, and (2) what we do if we have an `Integer`. But that's not actually appropriate for either a proof or a program. A proof has a particular goal, and a program forms a unified whole. And we normally would not wait until the end of the proof or program to bring unity to the two cases `String` vs. `Integer`. How do we do that? We find a much closer point at which they can be unified, some smaller goal.

#### goals and coterms

In the field of logic, Gentzen used such goals in his Sequent Calculus. In Ambidexter, coterms represent goals. A value is fed to a coterm (goal) using the `\$` operator. ```     1 \$ integer_goal     "one" \$ string_goal ```

Where do coterm names such as `integer_goal` come from? From the context. For example, in the term `    x y plus,`
"y" fills a gap between x and plus which can only be filled by a number. In Ambidexter, a name for this context may be introduced like so: `    x (integer_goal <+ ......) plus`
and then the name `integer_goal` may be used anywhere in the `......` range to pass along an integer value to the place once occupied by `y`.

Here's a trivial example. ```    (       (direct <+ "three" \$ direct)     put)```
Notice how it defines the name `direct` for the purpose of a `String` argument to `put`. Then with `"three"\$direct` it provides the string `"three"` as that argument. A more substantial example is ```    (       (direct <+ (convert <+ "three" \$ direct)               \$ ......       )     put)```
In the above, two coterm names are introduced. `direct` provides an argument to `put` and `convert` sends a value to the mysterious `......` coterm (details later). But the meat of the program does not refer to `convert`, and instead simply passes the string `"three"` to `direct`. So the complete program
```    (       (direct <+ (convert <+ "three" \$ direct)               \$ [n -> n show_integer \$ direct]       )       put     ) ``` will just print "three" regardless of the coterm
```    [n -> n show_integer \$ direct] ``` How does this coterm work? In Ambidexter, square brackets are used for coterms where parentheses are used for terms. The `n ->` part is reminiscent of a function expression, but notice the lack of backslash (`\`). `n` names the value which is supplied to this coterm. The
`    n show_integer \$ direct` just dictates that `n` is converted to a string which is then passed along to the `direct` coterm, satisfying the goal of an argument for `put`.

#### type of a coterm

The role of a coterm is to await a value, and to dictate what happens once the value is ready. Each coterm can handle a particular type of value — it is a consumer of that type, while a term produces its type. When a term and coterm share the same type, that means the value of the term could be passed along to the coterm. Term and coterm roles are opposite.

Every name introduced is either a term name, a coterm name, or a type name. If a name is used inappropriately, it is diagnosed during type checking, e.g.

`    The name is a covalue where a value is required.`

#### evaluation order

The `\$` operator always appears with a term to its left and a coterm to its right. The term is evaluated before being passed to the coterm. This explains why, when the above program is run, `"three"` is returned without `show_integer` ever being invoked.

Because `n` is passed to `show_integer`, `n` must have type `Integer`. Because `n` receives the value of the `convert` term, we see that the types of the coterm and of `convert` are both `Integer` as well. This is demonstrated by modifying `"three"\$direct` in the above program to `3\$convert`, with the result
```    (     (direct <+ (convert <+ 3 \$ convert)               \$ [n -> n show_integer \$ direct]       )     put)``` being a program that prints "3".

That's plenty for one lesson, so we will be content that "or types" have supplied a motivation for learning about goals and coterms. Details of "or types" in Ambidexter are reserved for the next lesson.

#### exercises

1. Make a program which has coterm names for the goals (1) of printing an integer or for (2) printing the length of a string. Provide variants of the program which use both coterm names.
2. Make a program which has coterm names for the goals (1) of printing a string with parentheses around it, and for (2) printing a duplicated string, e.g. "patpat". Provide variants of the program which use both coterm names.

Support open standards!