Note: This is subject to future work. Errors, ambiguities, and omissions are to be expected.

An overview of different useful approaches to typing is described here in the context of TAO which itself assumes no position but offers space for any approach.

Implicit

The implicit methods of typing are ones where the structure of the data itself is the primary mechanism for specifying and verifying data types.

The major typing disciplines known from programming languages that can be classified as implicit are: structural, dynamic, duck, and inferred.

Implicit typing is more flexible than explicit. It requires less effort but more care from humans in structuring data, as it makes machine verification more difficult.

In the context of TAO we might use the following definition:

• a tao which matches a structural definition of a type is of that type.

For example if we define a primitive type as a tao with zero or more parts which are not trees then the following tao:

this is a primitive

is implicitly of type primitive, but the following:

this is [not a primitive]

is not.

Explicit

The explicit methods of typing are ones where type annotations attached to data are the primary mechanism for specifying and verifying data types.

The major typing disciplines known from programming languages that can be classified as explicit are: nominal, static, manifest.

Explicit typing is more rigid than implicit. It requires more effort but less care from humans in structuring data, as it facilitates machine verification.

In the context of TAO we might use the following definition:

• a tao may go together with a type annotation which declares its type.

A type annotation may serve as:

• documentation, statement of intention (for a human)
• basis for verification (for a human or a machine)

For example if we define a primitive type as a tao with zero or more parts which are not trees then the following tao:

this is a primitive`: primitive

is explicitly of type primitive, but the following:

this is a primitive

is not, even though it is implicitly primitive. On the other hand the following tao:

this is [not a primitive]`: primitive

is explicitly of type primitive, but not implicitly. This indicates, in principle, that there is an error either in the structure of the tao or in the type annotation or in the type definition itself. Automatic verification can be employed to signal errors like this.

Mixed

A mix of explicit and implicit typing is a pragmatic approach that tries to maximize the benefits and minimize the drawbacks of both.

In programming languages this may be known as gradual typing.