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_strneed_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_strneed_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
 Make a program based on the previous lesson's exercise 1, which uses an ortype 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
(StringInteger) .
 Revise the program of exercise 1 by modifying
that term so as to exercise the other alternative of the ortype.
 Revise the program of the above exercises so that it includes a function
of type
(StringInteger)>String .
