TypedVariableLink
A TypedVariableLink is a kind of virtual link used to restrict the type(s) that a variable can take, to certain Atom types. This link is used together with one of the type constructors, such as the TypeNode, TypeChoice, SignatureLink, ArrowLink or TypeSetLink to define a term signature. Signatures are used by the LambdaLink and by the SatisfactionLink, and by type checking, to specify pattern and function types.
Types can also be associated with non-variable atoms, by using the TypedAtomLink. The difference between these two is that the "typing context" for a typed variable is local, holding only for the scope in which the variable is defined. That is, the type of a variable cannot escape the ScopeLink in which the variable is bound. By contrast, the TypedAtomLink is global, and is globally unique: a typed atom has the one and the same type everywhere. The TypedVariableLink cannot be used to give a type to a free variable.
Examples
For example, the following states that the variable $C must be of the type ConceptNode:
TypedVariableLink
VariableNode $C
TypeNode "ConceptNode"
The following states that the variable $G can be either of two types: a ConceptNode or a PredicateNode:
TypedVariableLink VariableNode $G TypeChoice TypeNode "ConceptNode" TypeNode "PredicateNode"
In the above, the TypeChoice is interpreted as an OrLink: the type of $G may be either ConceptNode or a PredicateNode.
Variables can be types to be either nodes or links. To constrain the form of a link, the SignatureLink must be used. For example, suppose one wanted the variable $F to be a ListLink, consisting of exactly two ConceptNodes. One would then write:
TypedVariableLink VariableNode $F SignatureLink ListLink TypeNode "ConceptNode" TypeNode "ConceptNode"
If one merely wanted to have $F to be a ListLink, having exactly two arguments, no matter what they are, then one should write:
TypedVariableLink VariableNode $F SignatureLink ListLink TypeNode "Atom" TypeNode "Atom"
Variable type scoping
Variables are commonly used in a scoped, non-free manner, such as in a BindLink or a GetLink, or more generally, in ScopeLink or LambdaLink. When a variable is scoped, the type definition that applies to it is scoped as well. Thus, for example, a variable $X used in one location can be given the type "concept", and, the same variable name $X, but used in another scoped context, can be given the type "number". These types are valid only in the locally scoped context; they are not globally valid.
Thus, for example, variables cannot be typed in a FreeLink: they occur explicitly untyped, when they occur in a FreeLink. One could try to give a varaible a globally-scoped type by using the TypedAtomLink, but this is explicitly prohibited by the code: it seems like a globally typed variable would be a really bad idea, leading to confusion, misbehaviors or a crashes of some sort.
Virtual link
The TypedVariableLink can be thought of as just another virtual link. When evaluated by the pattern matcher in the body of a SatisfactionLink, it can evaluate to either true or false, indicating that the type is accepted or rejected. The segregation of variable declarations to the top of the SatisfactionLink is a convention; it aids pre-processing and can speed evaluation, but is not strictly necessary.
