Ambidexter tutorial
lesson 3
coterms

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.