Conditional Expressions

A conditional expression consists of a test and two branches. For instance, the following expression is conditional:

if (x >= 0) then x else ~x

where if, then and else are keywords in ATS. In a conditional expression, the expression following if is the test and the expressions following then and else are referred to as the then-branch and the else-branch (of the conditional expression), respectively.

In order to assign a type T to a conditional expression, we need to assign the type bool to the test and the type T to both of the then-branch and the else-branch. For instance, the type int can be assigned to the above conditional expression if the name x is given the type int.

Suppose that we have a conditional expression that is well-typed. When evaluating it, we first evaluate the test to a value, which is guaranteed to be either true or false; if the value is true, then we continue to evaluate the then-branch; otherwise, we continue to evaluate the else-branch.

It is also allowed to form a conditional expression where the else-branch is missing or truncated. For instance, we can form an expression as follows:

if (x >= 0) then print(x)

which is equivalent to the following conditional expression:

if (x >= 0) then print(x) else ()

Note that () stands for the void value (of the type void). If a type can be assigned to a conditional expression in the truncated form, then the type must be void.