Term Language?

[DavePearce]

An interesting question is whether or not it makes sense to move Whiley from a statement / expression language into a unified term language. Doing this might have some potential benefits in terms of reusing certain statements (e.g. conditionals). The key motivator here is the thought that we need conditional expressions to support better property syntax. This would presumably move Whiley closer to ML?

Pros:

• Unified support for using statements in all sorts of situations, such as properties (Improved Property Syntax #81), lambdas (Statement Syntax for Lambdas #74), matches (Match Statement #34) and specification elements.
• Relatively easy to support without significant changes to Whiley

Cons:

• Allowing arbitrary statements (e.g. loops) in properties and/or specification elements may not make sense?
• What about unstructured control-flow? For example, break and continue or early return within a loop?

Notes:

• Return statements require special handling. They must return from the enclosing method/function and, hence, cannot be used in situations where no such element exists.

Example 1

Illustrates potential conditional syntax:

property sum(int[] arr, int i) -> int:
    if i >= |arr|:
        0
    else:
        arr[i] + sum(arr,i+1)

Example 2

Illustrates potential let-syntax:

type Item is null | {int id, int data}

function lookup(item[] items, int id) -> int
requires some { i in 0..|items| | Item it = items[i] ; (it is null) || (it.id == id) }:
    ...

(this requires a separator syntax)

Example 3:

This is probably not what we want!

function to_int(null|int n) -> (int r)
ensures if n is int:
               r == n
            else:
               r == 0:
    if n is int:
        return n
    else:
        return 0

This is pretty ridiculous! Not sure what to suggest here. We could disallow certain forms in specification elements. Or, we could simply discourage this. Or, just observe that, in this case, we should be using a property?

Example 4

function abs(int x) -> int:
    if x < 0:
       x = -x
   return x

The above works out fine since the "type" of the if expression is void.

Example 5

function sum(int[] arr) -> (int r):
    int r = 0
    for i in 0..|arr|:
        r = r + arr[i]
    return r

Observe here that a loop always has type void since we can never be sure how many iterations are taken.

Example 6

function abs(int x) -> (int r):
    if x >= 0:
        return x
    x = -x
    return x

This is an interesting example as its unclear how it should be typed. For example, what type should a return statement have? For the above to be typeable, it would need the type void. This means that return has some kind of special status.

Example 7

function f(null|int x) -> (int r):
    int y = match x:
       case null:
            return 0
       case int:
            x
    //
    return y

There are two questions here. Firstly, does return 0 exit the match statement or the function? Secondly, what is the return type of the match expression?

One solution here is to have both unit and void types. The former are for non-terminating statements (e.g. assignments); the latter for terminating statements. Therefore, in the above example, we have void join int gives int. Observe, however, that unit join int does not give int (what does it give actually?).