# Types - Overview

Every term in every expression in a Sym document has a type assigned to it. Every object definition has a type definition as one of its components. Since type definitions can include things like type variables, Sym uses a type inferencing process to determine the explicit types assigned to each term in every expression.

A "type" is an object. Every object definition has a type definition that is used to
restricted the parameters to terms of a certain type. This helps prevent the construction of
expressions that are not type valid, like trying to add a term of type **Color** to a term
of type **Integer**.

A “type” is assigned to every term in every expression. The type assigned to each term is
also an expression. This has important consequences, primarily in that the type expression
assigned to a term also has a type assigned to it. So for example, the type **Real** is an
object which is defined as:

Real :: Type

And since types are expressions, the **Type** object also has a type. To avoid having this
process repeat indefinitely, we make the **Type** object self-referential. The type of the
**Type** object is a reference to itself.

The types in the type system can be simple names like **Real** or they can be objects with
parameters like the **To** object. In order for an object to be valid as a type for another
object, it must be defined in the **Types** namespace.

## Type Definitions

Every object definition is required to contain a type definition. The type definition is
only allowed to contain objects in the **Types** namespace.

## Simple Types

The simplest types that can be assigned to object definitions are just names in the
**Types** namespace. For example,

Pi :: Real

## Map Types

Any object that is intended to have one or more parameters when it is used in expressions
in a document will be typed using an arrow type. For example, if f[x] maps a **Real** to
another **Real**, the type definition would be:

f :: Real → Real

The “arrow” here is just another object, in this case an object in the **Types**
namespace named **To**. The type definition for the **To** object is:

To :: Type → Type → Type

## Type Variables

The type definition of an object can use type variables in addition to simple types and arrow types. For example, we can construct and object named “Fn” with the type definition:

Fn :: U → U

This type definition only restricts the type for “Fn” so that the type of Fn[x] is always inferred to be the same type as the type for “x”. So Fn[1] will have type Integer because “1” has type integer.

In cases where there is more than on possible choice for the type for an object like “Fn”, the type inferencing process will assign the most specific type from the possible choices. So in the expression:

Fn[1] + 2.0

The **Add** object at the top of the tree will be assigned the type **Real** and it
would be valid to assign either **Integer** or **Real** to “U” in the type definition
of **Fn** (assuming that Integer is a subtype of Real). But in this example, the type
inferencing will assign **Integer** to **Fn** because it’s the most specific type
choice that is allowed.

Note that type variables in type definitions are always defined in the **Variables**
namespace.

## Generic Types

Generic types defined in the type system for Sym can be thought of as polymorphic types
with restrictions. They are used in object definitions where an object needs to able to have
more than one type, but the type choices are not unlimited as they would be if a type
variable were used. For example, using the polymorphic type **AddType** for the addition
and subtraction objects allows specifying which types can be added and subtracted. The
details of the construction of generic types are described in Conditions in Type Definitions

## Subtypes

The type system used in Sym includes the concept of a "subtype". See Subtypes

## The "Top" and "Bottom" Types

The type system includes a Top type named **Object** and a Bottom type named
**Null**. Every type is a subtype of **Object** and the **Null** type is a subtype
of every type. See The Object (Top) and Null (Bottom) Types

## Undefined objects

Expressions can be created that contain terms like "*x*" and "

*y*" that don't have an object definition in any of the libraries. These objects are assigned a type definition like:

x :: U

where "U" is a type variable.

The type inferencing process resolves the type for undefined terms.
An undefined term is assigned the most general type possible that doesn't result in type
errors in the expression. So if the expression is MyFn[x] and MyFn is defined as **Real →
Real**, then "*x*" is typed as **Real**. Other types (**Integer** for
example) might also give a valid type assignment in this expression, but the type system
will select the most general type.

## Type Errors

A type error occurs when a parameter of a term can't be assigned a type that is consistent
with the type required by the type definition of the parent term. For example, for the
object **Blue** the type is the **Color** object. The expression:

| Blue |

contains a type error because the **AbsoluteValue** object is typed as **Real** →
**Real** and **Color** is not a subtype of **Real**. In expressions that contain
type errors, at least one of the terms will be highlighted (light red background) to
indicate the presence of a type error. Information about the type error is also shown in the
**Properties** pane.

An expression is "type valid" if the type of every child node in the expression tree is consistent with the corresponding type in the type definition of the parent term in the expression tree. The type of the child node is consistent if it is a subtype of the type of the parent.

Expressions that are not type valid are allowed. Expression trees containing any combination of terms can be constructed, any expression tree can be evaluated as either type valid or not. The commands used to construct expressions are designed to avoid constructing expressions with type errors where possible, but Sym doesn't completely prevent this from happening.

## Types and the autocomplete popup

The autocomplete popup normally restricts the choices displayed to only show options that
are type compatible with the parent expression. So if you type "*blu*" into an empty
box in an **Abs** object, the **Blue** object won't appear because it's not type
compatible. You can use the **Show All** button to see all options, including those that
would result in a type error.

## The Types Namespace

The **Types** namespace has a special role in the Sym system. Object defined in the
**Types** namespace with type definitions are considered to be a type in the type
system. In other words, these are objects that can be assigned as the type of an
expression.

Objects in the Types namespace must have a result type of **Type**.

Not every object with the type of **Type** defines a new type that can be assigned as
the type in a type definition. For example, objects like To[Real, Real] and Set[Real] are
types. But TypeUnion[Real, Real] does not define a new type and

Type definition: TypeUnion[Real, Real]

is not valid as the type definition in an object defintion. Note that **TypeUnion** is
in the **Core** namespace not the **Types** namespace.

Any object that is in the **Types** namespace is assumed to define a new type. This
includes objects that are maps. Any object that is not intended to define a new type should
not be in the **Types** namespace.