TypeChoice

From OpenCog
Jump to: navigation, search

The TypeChoice is a kind of link, specifically, a kind of ChoiceLink, that allows a type to be polymorphic. It lists a set of types that a VariableNode may have, or that might occur in a SignatureLink. It is a type constructor.

Examples

Thus, for example,

TypedVariableLink
   VariableNode $G
   TypeChoice
      TypeNode "ConceptNode"
      TypeNode "PredicateNode"

The TypeChoice link is interpreted as an ChoiceLink, specifying that the variable $G can be either a ConceptNode or a PredicateNode.

A TypeChoice link can enclose a SignatureLink if more complex polymorphic types are needed. Thus, for example,

TypeChoice
   SignatureLink
      TypeNode "ListLink"
      TypeNode "ConceptNode"
      TypeNode "ConceptNode"
   SignatureLink
      TypeNode "ListLink"
      TypeNode "ConceptNode"
      TypeNode "ConceptNode"
      TypeNode "ConceptNode"

defines the signature of a ListLink that can have either two or three arguments, but not one, nor four or more.

Theory

In type theory, the TypeChoice Link corresponds to the sum type, and thus is a form of disjoint union; it is the coproduct in the category of sets. The product, of course, corresponds the product type. The AtomSpace allows both of these, when working with types: use the TypeChoice link for sum types, and the SignatureLink for product types.

Note that, currently, the AtomSpace does not define an explicit TypeProduct Link. It has to be hacked together by using a SignatureLink together with an AndLink. This may change.

See also