TypedVariableLink

From OpenCog
Jump to: navigation, search

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 or ArrowLink 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.

See also