Lambda the Ultimate

Wadler's Views anyone?

Types: Static Properties
Predicates: Dynamic Properties

On the other hand, types can be dynamic properties if there is support for runtime casting. Maybe `cast' is just another word for `predicate dispatch'?

I tend to look at "cast" as combinator for one (value) expression of type T, and two (continuation) expressions of types T1 and T-T1, where T1 is a subtype of T.

What's the semantics? Wait for the value of (the value) expression, and then, if it's of type T1, then pass it to the first continuation, else to the second.

This obviously requires ability to check if a value satisfies a type. Some languages prefer not to deal with this, and effectively hide the second continuation from a programmer (but it's still present implicitly - if even as a possibility for core dump if the programmer guessed wrong).

In this ontological setting, types are both static properties of expressions, and dynamic properties of values (casting involves evaluating a predicate under the hood) :-)

In a Java-like PL this might look as:

T value = ...;
cast (value)
{
  case(T1 v1)
  {
    blah(v1);
  }
  case(T2 v2)
  {
    doh(v2);
  }
}

The compiler statically checks that all types in case's are subtypes of the type in cast, and probably also do not overlap, and cover all the possibilities (so T1 xor T2 must be equivalent to T). The runtime then dynamically selects the right case.

PS: Of course, the real Java^TM uses unchecked exceptions for covering the second continuation, which does not invalidate the claim that this continuation exists.