Types
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.