What is Expressiveness in a Computer Language

[Andreas Rossberg]

Chris Uppal wrote:
> 
> I have never been very happy with relating type to sets of values (objects,
> whatever).

Indeed, this view is much too narrow. In particular, it cannot explain 
abstract types, which is *the* central aspect of decent type systems. 
There were papers observing this as early as 1970. A type system should 
rather be seen as a logic, stating invariants about a program. This can 
include operations supported by values of certain types, as well as more 
advanced properties, e.g. whether something can cause a side-effect, can 
diverge, can have a deadlock, etc.

(There are also theoretic problems with the types-as-sets view, because 
sufficiently rich type systems can no longer be given direct models in 
standard set theory. For example, first-class polymorphism would run 
afoul the axiom of foundation.)

> It's worth noting, too, that (in some sense) the type of an object can change
> over time[*].

No. Since a type expresses invariants, this is precisely what may *not* 
happen. If certain properties of an object may change then the type of 
the object has to reflect that possibility. Otherwise you cannot 
legitimately call it a type.

Taking your example of an uninitialised reference, its type is neither 
"reference to nil" nor "reference to object that understands message X", 
it is in fact the union of both (at least). And indeed, languages with 
slightly more advanced type systems make things like this very explicit 
(in ML for example you have the option type for that purpose).

- Andreas