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
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
GroundedSchemaNode “py:plus” ListLink NumberNode “2” NumberNode “3” NumberNode “5”
then the GSN labeled “py:plus” would have the function signature
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
PredicateNode “eat” ListLink ConceptNode “Ben” ConceptNode “steak”
Then the PredicateNode labeled “eat” would have deep type
which represents the mapping the PredicateNode actually carries out.
If we had
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
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
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,
Implication Evaluation D List A B Member A SatisfyingSet $V Evaluation D List $V B
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
(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.