Ambidexter tutorial
lesson 4
or 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.