Deep types

See also type signature and type checking. The SignatureLink implements a form of "deep types" for the pattern matcher. The FuzzyLink implements a "deep type" that is imprecise, allowing approximate matches. The current, primary use of deep types is to control the type of a VariableNode during pattern matching, either strictly, or in a fuzzy manner.

The general theory for deep types is discussed in the wiki page on type constructors. It is not exactly clear what this page is proposing, that is not already done ... is the proposal here to somehow integrate with PLN? Use them more widely in .. some new situation?

Deep Types for Atoms

We can associate additional type info (constituting what I’ll call a “Deep Type”) with any Atom using the TypedAtomLink.

The term “Deep Type” is used to distinguish the types we’re talking about here, namely, all of the types built with the type constructors, from the predefined “atom types”. Two instances of the PredicateNode type both have the same Atom type, “PredicateNode.” But they may have different deep types if they represent predicates taking different sorts of arguments.

So for example, if we have

ExecutionLink

GroundedSchemaNode “py:plus” ListLink NumberNode “2” NumberNode “3” NumberNode “5”

then the GSN labeled “py:plus” would have the function signature

ArrowLink
   ListLink
       TypeNode "NumberNode"
       TypeNode "NumberNode"
   TypeNode "NumberNode"

This indicates that it takes, as input, two NumberNodes, and returns a single NumberNode.

The ArrowLink is used to specify functions in this manner. The SignatureLink is used to declare input and output signatures. The TypedAtomLink is used to declare "global" signatures for functions. The declaration of variable-length lists is being explored with a combination of IntervalLink and TypeSetLink.

Or if we have

EvaluationLink

PredicateNode “eat” ListLink ConceptNode “Ben” ConceptNode “steak”

Then the PredicateNode labeled “eat” would have deep type

ArrowLink
   ListLink
       TypeNode "ConceptNode"
       TypeNode "ConceptNode"
   TypeNode "TruthValue"

which represents the mapping the PredicateNode actually carries out.

If we had

EvaluationLink

PredicateNode “quickly” ListLink ConceptNode “eat_101”

Then the PredicateNode labeled “quickly” would have deep type

ArrowLink
   ArrowLink
       ListLink
           TypeNode "ConceptNode"
           TypeNode "ConceptNode"
       TypeNode "TruthValue"
   TypeNode "TruthValue"

That is, “quickly” is represented as mapping (mappings from pairs of ConceptNodes into TruthValues) into TruthValues.

The real power of using types here is seen with ExecutionOutputLinks. Suppose for instance we have the fragment

ExecutionOutputLink

GroundedSchemaNode “py:deduction” ListLink InheritanceLink $X $Y InheritanceLink $Y $Z

(note that this fragment must exist within a larger Atom construct that contains other Atoms quantifying $X, $Y and $Z, but we don’t need to write that out for the point we’re making at the moment).

Associating the type

ArrowLink
    ListLink
        TypeNode "InheritanceLink"
        TypeNode "InheritanceLink"
    TypeNode "InheritanceLink"

with the GSN “py:deduction” makes it clear what type of output to expect from the ExecutionOutputLink. This can be very useful if e.g. one wants to do backward chaining from the ExecutionOutputLink.

The value of assigning deep types to ListLinks comes when one has GSNs whose output are ListLinks.

Then it can be valuable to be able to specify that a certain GSN produces a list or set of a certain type. For instance, if one has a GSN for “append” (that appends two ListLinks) then one has the parametrized deep type,

(List of T, List of T) ==> List of T

meaning that if the argument lists are lists of elements of type T, so is the output list. To construct a "List of T" types one needs to use the IntervalLink to specify the min and max length of the allowed list, together with the TypeSetLink. The "List of T" type is currently heavily used in ghost, to specify regex-like matching patterns for GlobNodes.

Deep Types and Evaluation2Member

One example illustrating the value of all this is the creation of a general-purpose Evaluation2Member rule. For a single-argument predicate, we can say

EvaluationLink
	P
	X

is equivalent to

MemberLink
	X
	SatisfyingSet
		P

In general, we can think about a parameterized rule

Evaluation2Member(m,k) 

for dealing with the k'th argument of a predicate that takes an argument-list of length m

For two-argument predicates, we can look at two variations,

Evaluation2Member(2,1) 

which is

Implication
    Evaluation
        D
        List
	    A
            B
    Member
        A
        SatisfyingSet
           $V
           Evaluation
               D 
               List
		$V
               	B

and

Evaluation2Member(2,2) 

which is

Implication
    Evaluation
        D
        List
	    A
            B
    Member
        B
        SatisfyingSet
           $V
           Evaluation
               D 
               List
		A
               	$V

These are OK so far as they go, but it would be much nicer to have a general rule for

    Evaluation
        D
        L

for the case where L is a list of length m. In this case there will be k different basic rules, one corresponding to each position 1 thru m. E.g. we can write a rule such as

Evaluation2Member(*,k)

(the * meaning that it holds for all m) of the form

ForAllLink $D, $L, $k
Implication
    Evaluation
        $D
        $L
    Member
        ExecutionOutputLInk
            GSN “ElementAt”
            ListLink
               ListLink $L
               NumberNode $k
        SatisfyingSet
            Variable $V
            ExecutionOutputLink
               GSN “Insert”
               ListLink
                   ListLink $L
                   Variable $V
                   NumberNode $k
 

Where do deep types come in here? The point is, the GSN “Insert” should have type

(List of T, T) ==> List of T

as well as

(List of T, List of T) ==> List of T

and the GSN "ElementAt" should have type

List of T ==> T

Deep Types and backward chaining

Then the backward chainer can utilize Evaluation2Member(*,k) properly, based on knowledge of what (deep) type its output is going to have. For instance, if $L is a list of ConceptNodes, then the deep type signature of "ElementAt" lets us know that the output of

        ExecutionOutputLInk
            GSN “ElementAt”
            ListLink $L
            NumberNode $k

is a ConceptNode. This is very helpful because it tells us that

    Member
        ExecutionOutputLInk
            GSN “ElementAt”
            ListLink $L
            NumberNode $k
        SatisfyingSet
            Variable $V
            ExecutionOutputLink
               GSN “Insert”
               ListLink $L
               Variable $V
               NumberNode $k

is of the form

Member
    ConceptNode X
    ConceptNode Y

And this means that if the backward chainer is looking for some rule that can output a MemberLink between two ConceptNodes, it should potentially consider applying Evaluation2Member(*,k) to a PredicateNode which is applied to a list of m ConceptNodes.

Without the deep type signature associated with "ElementAt", the backward chainer would have no way of knowing that the Evaluation2Member rule should be considered in this context, because it would simply encounter the ExecutionOutputLink and not know what it was going to output.