Type Definitions

Simple type definitions

The simplest type definitions just include a single explicit type. For example:

Type :: Real

Type definitions can also include type functions. The most commonly used type function is the To object that defines an object to be a map from one type to another. For example, an object with type definition:

Type :: Real → Bool

is a one parameter object that takes a real number as its input and returns a Boolean value.

Using variables in type definitions

Type definitions can also include type variables. For example, an object with type definition:

Type :: U → U

is a one parameter object that can take any type of object as input but always returns an object of the same type. Type definitions can include more than one type variable and can include combinations of type variables and explicit types. For example, an object definition with type definition:

Type :: U → Real → Set[U]

is a two parameter object that can take any type in the first parameter, takes a Real (or a subtype of Real) in the second parameter, and returns a set of objects that are of the type of the first parameter.

Type definition conditions

Conditions can be added to a type definition to restrict the types that are valid for a type variable in the type definition. See Conditions in Type Definitions for more information.

Defining the number of parameters of an object

The type definition of each object determines the number of parameters that object can have.

Type :: A is an object with no parameters

Type :: A → B is an object with one parameter

Type :: A → B → C is an object with two parameters

If you define MyFn as A → B → C and then type "myfn" in an expression, the autocomplete popup will show a two parameter version:

Note that a type definition like (A → B) → C → D is still a two parameter object, as is A → (B → C) → D. In these definitions, we are requiring that the first or second parameter (respectively) be a map, but both are still two parameter objects.

If you need to create an object that is a one parameter object where the return type is required to be a map from A → B, you could create the type definition as Type :: U → A → B, but Sym will want to insert new instances of this object as two parameter objects. You can get to the one parameter version in the autocomplete popup by clicking on the down arrow to the right of the object and selecting the one parameter version, but if the intent is for the object to always be a one parameter object that returns a map, then it may be better to create a type definition like

where V is a type variable. The instances of an object with this type definition can never have more than one parameter and the one parameter version will be typed as A → B.