Semantics of Runtime Type Testing

[DavePearce]

(see also https://github.com/Whiley/RFCs/issues/36 and https://github.com/Whiley/RFCs/pull/51)

The semantics of the runtime type test operator is remain problematic, despite potential improvements coming from RFC#51. In short, relying only on the underlying type for selection is just dumb. The following illustrates an example:

type Point is {int x, int y}
type Location is {int x, int y}

function isPoint(Point|Location pl) -> (bool r):
  if pl is Point:
        return true
    else: 
        return false

This currently fails with the error branch always taken. Realistically, I don't think this is what we want. Instead, we need a different way to manage type selection. A simple rule would be:

• Given e is T where e has type S, we require S has union type and T to select exactly one option.

Under this rule, the type test operator is simply for distinguishing type tags. Unfortunately, it does mean things like x is nat are no longer supported. This is not ideal, though perhaps we could live with it. Furthermore, we extend selection with various patterns as follows:

• (Choice) x is S | T is taken to mean either S or T are selected which, in turn, requires each to match exactly one bound.
• (Depth) x is (S & T) is taken to mean we select S from x which, in turn, is itself a union type. Then, from this union we select T.

This scheme is actually pretty neat and we could try to support different kinds of patterns. For example, patterns like (S & T) | (U & V), etc.