Conditions in Type Definitions

Conditions in type definitions are used to further restrict the types that are valid for a type variable in a type definition. A type definition with conditions might look like Type: U → U with (condition)

The expression that appears after the "with:" in a type definition that has conditions can be either a single condition

or it can be a list of conditions

There are three expressions that are valid conditions. A condition can be an equality, it can be a subtype statement or it can be a statement like the ones shown here that uses the In object.

Equality conditions

An equality condition has the form

U = (expression)

where the left-hand side (U in the example) must be a type variable that appears in the type definition.

An equality condition like U = Real is allowed, but doesn't really serve any purpose since it's equivalent to just putting Real directly into the type definition.

The right-hand side of an equality condition can contain any expression that is valid in the type definition itself and it can also contain TypeUnion and/or TypeIntersection terms.

For example, you could create a type definition like

U → V → W with W = Set[TypeUnion[U, V]]

Subtype conditions

A subtype condition has the form

Typically, either the left-hand side or the right-hand side is just a type variable that appears in the type definition, but more complicated expressions are valid.

In conditions

These conditions have the form

U in Types

where the left-hand side (U in the example) must be a type variable that appears in the type definition or the ResultType of a type variable the appears in the type definition

This type definition condition is used to restrict a variable in a type definition to be one of the types in the list of types specified on the right-hand side of the condition. There are two ways to do this. The first is to list the types explicitly in the condition - for example:

The second way to do this is for the condition to specify the name of a function that returns a list of types - for example:

In this case, the Sym type inferencer will call the function to retrieve the list of types.

The second approach has the advantage that it's possible to extend the list of types that are included in a type definition when new libraries are created by adding the additional types as an extension to the function.

The ResultType Object

Conditions can also contain the ResultType object. The ResultType object lets you apply a condition only to the result type of an object. For example, with this type definition

U can not only be one of the types in AddTypes, but it can be any map to one of the types in AddTypes. If AddTypes includes the Real type, then a type like TypeA → Real and TypeA → TypeB → Real, and so on, are all valid types for the type variable U.

Using the ResultType object allows you, for example, to include operator types in the set of valid types for the Add object.