Tg: Polymorphism in TL
It should be noted that in the TL schema of the overwhelming majority of API calls the use of polymorphic types is restricted to the Vector type. Nevertheless, having a view of the big picture is still helpful.
Ordinary inductive types
For example, let us consider the IntList, which is defined as follows:
int_cons hd:int tl:IntList = IntList;
int_nil = IntList;
The “int_cons” and “int_nil” constructors as well as the “IntList” type itself are expressions of the following types (writing A : X means that A is an expression of type X):
IntList : Type;
int_cons : int -> IntList -> IntList;
int_nil : IntList;
The keyword Type is used to denote the type of all types. Note that Type is not Object (Object is the type of all terms). Here is alternative syntax that could be used in some other functional programming language (but not in TL):
NewType IntList :=
| int_cons hd:int tl:IntList
| int_nil
EndType