## Ambidexter tutoriallesson 4or types

In the previous lesson the logical connective "or" provided some of the motivation for coterms. Effective use of "or" involves setting goals within a program or proof, and coterms represent goals.

Recall that we considered how an "or type" would be used in a program, analogous to how an "or proposition" would be used in a proof. The question led us to a discussion of goals and their embodiment as coterms.

#### or coterms

Suppose `x` is a term with type `(| String | Integer |)`, i.e. `String` or `Integer`. Then `x` can be used as follows in Ambidexter.
```    x \$ [| string_goal          | integer_goal |] ```

The bracketed coterm with the `|` notation combines the two goals so as to handle both cases of `x`. Notice that a coterm must be furnished for each of the cases `String` and `Integer`, in this example the coterms are the named coterms `string_goal` and `integer_goal`.

The previous lesson showed how various named coterms can be introduced. Combining the above with that lesson's example, we get
```    (       (direct <+ (convert <+ x \$ [| direct | convert |])               \$ [n -> n show_integer \$ direct]       )     put)``` However, this is not a valid program because it mentions `x` without defining it. So far we have dealt with making use of "or types" but now with producing them.

#### or terms

To prove "`String` or `Integer`", we would straighforwardly start off by providing a proof of `String` or a proof of `Integer`. Say for example we start with `1` as a proof of `Integer`. Then in Ambidexter a proof of "`String` or `Integer`" would be, for example,
`    (|need_str|need_int| <+ 1 \$ need_int)` This is straying rather far from conventional programming, so let's analyze it. The `<+` indicates that we're making a goal out of the context, just as we did with `direct` and `convert` above, except that since the context is an "or type" we are interested in naming each alternative goal. The `|need_str|need_int|` is a pattern which does so. The remainder, `1\$need_int`, tells what do, namely to take the `Integer` value 1 and pass it along to satisfy the `need_int` goal.

As with "and patterns", unused names may be indicated by an underscore in Ambidexter, so the above can be simplified to
`    (|_|need_int| <+ 1 \$ need_int)` This can be substituted for `x` in the above program to yield the complete program
```     (       (direct <+ (convert <+ (|_|need_int| <+ 1 \$ need_int)                           \$  [| direct | convert |])               \$  [n -> n show_integer \$ direct]       )     put)``` If you prefer to keep the name `x`, you can use a function, e.g.
```    ( ( (|_|need_int| <+ 1 \$ need_int)         (\x ->           (direct <+ (convert <+ x                               \$  [| direct | convert |])                   \$  [n -> n show_integer \$ direct]           )         )       )     put)``` And of course, the string alternative is a valid program as well.
```    ( ( (|need_str|_| <+ "one" \$ need_str)         (\x ->           (direct <+ (convert <+ x                               \$  [| direct | convert |])                   \$  [n -> n show_integer \$ direct]           )         )       )     put) ```

#### exercises

1. Make a program based on the previous lesson's exercise 1, which uses an or-type to represent both goals simultaneously, i.e. (1) of printing an integer and (2) taking a string and printing its length. The program will contain a term of type `(|String|Integer|)`.
2. Revise the program of exercise 1 by modifying that term so as to exercise the other alternative of the or-type.
3. Revise the program of the above exercises so that it includes a function of type `(|String|Integer|)->String`.

Support open standards!