Declaration inference

From Dyna
Jump to: navigation, search


Inferring declarations of structure types

If you write foo(bar(X)) without declaring foo or bar, Dyna assumes that foo and bar are structure types. It creates declarations for them by trying to infer appropriately restrictive types for their arguments in the context of the program.

The basic idea: If you write the inference rules

foo(A) += bar(A)*baz(A).
foo(A) += bing(A).

then type safety requires that Failed to parse (Missing texvc executable; please see math/README to configure.): t_{foo,1} \supseteq ((t_{bar,1} \cap t_{baz,1}) \cup t_{bing,1})

(where Failed to parse (Missing texvc executable; please see math/README to configure.): t_{foo,1}

is the type of the first argument of

foo). This fact can be used to propagate explicitly declared type information through the program. Lower bounds propagate from antecedent to consequent, and upper bounds propagate in the other direction.

Thus, if you explicitly declare

:- structure(bing(int x)).

then Dyna knows that foo's first argument must be a supertype of int. Conversely, if you explicitly declare

:- structure(bing(int x)).

then Dyna knows that bing's first argument must be a subtype of int.

In particular, if you declare the types of fields in your axioms, then Dyna will figure out the minimum types that your theorems can use. Conversely, if you declare the types of fields in your theorems, then Dyna will restrict your axioms to the maximum types that would justify those declarations. If you declare nothing, then Dyna will give all fields the maximum declaration, term, so it will act like a weakly typed language (Prolog or LISP).

Dyna currently uses this inference algorithm.

The algorithm will be too permissive as it stands. What it doesn't recognize is that the declarations resulting from "permit everything that's not explicitly forbidden" need to be fed back in as required and propagated forward again. For example, if tbar is declared as int but tbaz is undeclared, then we can't propagate any "required" information forward to foo, and will prepare to use upper-bound declarations tbaz=term and tfoo=term since nothing is explicitly required for either. But declaring tbaz=term allows us to propagate forward that tfoo has a lower bound of int. So now we can use a lower-bound declaration tfoo=int after all. Now that gets propagated backward, changing tbaz's upper-bound declaration to tbaz=int. Notice that permitting term for tbaz changed our mind about whether tfoo had a lower bound, but not about whether tbaz itself had a lower bound. Possibly the algorithm can be fixed in a well-defined way. However, let's get the original version running first; it will be fine for most real cases, in particular the case when all axioms are explicitly declared.
Another reason the algorithm will be too permissive: foo(X)+=bar(X)*baz(X), where tbar and tbaz have null intersection, should not result in tfoo being term.

Automatic declarations of union types

Currently described at list of keywords; should probably be moved.

Automatic declarations of pattern types

For each item type, antecedent and consequent patterns are automatically declared.

Automatic declarations of computed expressions

Not implemented yet. Based on reading a .h file to find operators and methods. So if we know that log() is a function, we should read the .h to find out what it applies to and what it returns. See more thinking at expressions.

Retraction closure

If you retract a set of axioms, what theorems should be deleted as a result? Given a declaration

:- retractable(foo).

where foo is a subtype of axiom, this step answers the question using this algorithm. It changes the declaration to

:- retractable(foo, foo_closure).
:- union(foo_closure, result of algorithm).

to tell subsequent stages of compilation that chart::retract_foo() should actually delete all items of type foo_closure.

If there are some classes of theorem that must be partly but not fully deleted, then the compiler currently gives a "not yet supported" error. In future the compiler will deal with this less common case by applying one of three fallback strategies: deriving a closure that is a union of patterns rather than simple types, transforming the program to distinguish subtypes that should be fully deleted from those that should be fully preserved, and in the worst case, simply tracing through all the consequents of retracted axioms and undoing their work.

Automatic generation of compiler pragmas

This will be DynaMO's job.

Personal tools