Types, Sorts, and Signatures

The original purpose of types was to restrict expressions in such a way as to prevent Russel’s Paradox. Bertrand Russel discovered his paradox just before publication of his book Principles of Mathematics, and not wanting to delay publication too much, he introduced the mechanism of types as a solution in a hastily written appendix to the book (by the way, “Principles of Mathematics” is not just the English translation of “Principia Mathematica”. Principia Mathematica was a later work written by Russell and Whitehead).

Ever since that hastily-written appendix there has been some ambiguity over whether types belong to expressions or to values.The difference is not an insignificant one. Expressions are syntactic objects, part of a language. Values are the things that the language is about. So if types go with expressions then they are things that can be determined statically by examining the text of the program. If types go with values then you can’t assign types statically in any powerful language. You have to figure it out dynamically.

The ambiguity arises from the fact that a kind of type really applies to each kinds of thing. A value has a sort, which is the kind of thing that it is. A variable has a signature which describes the sorts of values that the variable can hold. Lets expand this notion of a signature to apply to any expression so that the type of a value is called a sort and the type of an expression is called a signature. We’ll let “type” retain its current ambiguous status.

There is more to the difference between a sort and a signature than just what they apply to. Consider a class fifo that is a subclass of the abstract class aggregate. An expression can have the signature fifo or the signature aggregate, but there can be no values of sort aggregate because it is abstract.

Expressions can have even more complex types. Unobtainabol has type expressions with the “or” operator, |. A type expression “int|float” would be read “the sort is either int or float”. This feature lets you implement linked lists without explicit pointers. For example:

class Link {

data: int;

next: Link|Null;

};

This says that the next element in the list is either another Link or is the special value Null. There is no need to refer to pointers, you can just use Link and let the type system handle pointer issues for you.

So in Unobtainabol we can declare a variable with any of a set of types and an expression that uses that variable can also have any of a set of types. For example in

var x: int|float;

...

y := x+1;

the expression x+1 can be either an int or a float but the value of the expression doesn’t have an ambiguous type. Whatever is in the variable x is one or the other. There are no values that are “int or float” in some undecided state (well ... maybe in advanced Unobtainabol). So the type of an expression can be broader than the type of a value can be.

Here is some new terminology for Unobtainabol:

sort: the type of a value. A sort consists of a set of possible values and set of basic operations on those values. Every non-virtual class is a sort as is every primitive type such as int and float.

signature: the type of an expression. Signature is a statically determined restriction on the sorts of values that an expression can evaluate to.

class: The type of a namespace (more on that in a future post).