Design/StorageSpec

From Dyna
Jump to: navigation, search

Contents

Jason's Comments on the Document Below

I've also clarified since then that a name like foo or foo.sub refers to a class, not just a type. A class is a type (i.e., set of terms) plus some additional information about how the type is stored and about the classes returned by its accessors. It corresponds to a C++ class.

When you write foo.sub as a functor inside a declaration or other pattern, it is a class name. Methods that simply match a term against that pattern only care about the TYPE that is implemented by the foo.sub class. Any implementation of that type will match. But methods that will return an object e.g., accessors) actually pay attention to which classes you used, since they have to know what class of object to return -- e.g., foo.sub rather than some other implementation of the same type.

(Classes are sometimes called "named types" below.)

Earlier Comments from Jason

This is almost the level of detail we'll need for a spec. It is still a bit short of a formal spec, because it doesn't give a grammar for the concrete syntax of the language, and it is missing a few details. It is also not written as a minimalist set of definitions (just the facts, ma'am) that is structured to make implementation obvious.

The biggest missing piece, by far, is values and svals (as well as specifying strategies at the inference layer -- chaining, memoization, maintenance of squeries, etc.). But it seems simpler to sort out the value-free case first, and that's what I've done here.

This message winds up with a detailed example about storing Peano integers. You could peek ahead!

There are probably still some slips of terminology; maybe other errors too, not sure.

Rethinking Variants As "Pattern Types"

Before launching into the design, let me explain the key change. The big insight from our meeting on Tuesday was that variants ought to be regarded as types in their own right, not just partial implementations of types.

Thus, you declare foo and foo.a using the same syntax -- there's really no difference except in the names. Both are pattern restrictions on a universal type FOO that is not necessarily implemented.

Also, there is no need for a separate "traditional declaration" of foo that names its fields. I have a new way of handling named accessors and keyword constructors that associates names with the variables in a pattern, not the fields. This is actually much more useful because it allows efficient construction and destructuring of deeply nested patterns. And it is general enough to get the old named fields if you want them. Finally, it notices when you're using inconsistent names.

foo.a is required to be a subtype of foo. This is checked after the types are defined. The requirement has the following benefits:

  • it provides a semantic guarantee about type names that makes programs easier to read.
  • it allows a consistent view of pattern type definitions, including 0-depth pattern types and pattern subtypes of a union type.
  • it ensures that all terms of the form foo(...) actually do have the type foo. Otherwise, there would be a lot of confusion when some terms of the form foo(...) were skipped over by an inference rule like
    • sum += f(foo X).
  • it guarantees that foo.a can upcast implicitly to foo. That means that you can safely do this in C++:
    foo_t myfoo = x.arg1();
    without knowing whether the static return type of x's arg1() method is actually foo or a more efficient variant such as foo.a.

Previously, I had tried to keep open the possibility that foo.a might just as well be a supertype of foo. (Why? Because if you had any three variants foo.1, foo.2, foo.3, you were supposed to be able to pick the variant that you wanted to use most, or by default, and rename it to the simpler "foo".)

But I don't think it's much of a limitation in practice to require foo.a to be a subtype of foo. If you really want to use foo to refer to a subtype, then define bar to be the supertype, define bar.a to be the subtype, and then simply define foo as an alias for bar.a:

   foo X ~ bar.a X.

Ok, prelude over. So now let me explain the new design.

The Universe Of Terms

Let's start simple. Conceptually in Dyna, there is the universe of all terms. This is just as in Prolog, but for us, every term has a type (which at first we won't use for anything). We also allow primitive terms more extensively than Prolog does.

type 
is a (named) set of terms, usually an infinite set.

We have a set of "primitive types," such as int, each of which is a set of "primitive terms". These primitive types might not be disjoint; e.g., short is a subset of int.

We also have an arbitrary set of functor symbols. Let's now define the

"functor terms"
  • If FOO is a functor symbol, and t1, ... tk are terms, then FOO<t1,...tk> is a functor term. It is said to have functor FOO, arity k, and arglist <t1,...tk>.
    Note the use of <> and boldface FOO to write an actual term. These do not appear in programs. In programs, we only have patterns like foo(t1,...tk), which may denote a single term or several terms.
  • There are no other terms besides the functor terms required by the above, and the primitive terms.

Some of the primitive types are built-in, and their terms may have literal representations in written Dyna, such as the int 123 or the string "hello world". Other typed primitive terms may declared to exist as well, but without literal representations: the syntax is given later.

Declarations for the built-in primitive types may be omitted in high-level Dyna. But when they're omitted, they should probably be added during preprocessing. (A user declaration should override the built-in ones, which allows us to extend the set of built-in ones in future versions of Dyna without breaking existing user code.)

Note that all terms are variable-free, at least for now; this is different from Prolog.

Patterns

Patterns, unlike terms, can be written directly in Dyna.

A ;pattern: is best regarded as a "destructuring" partial function that maps a term to an assignment of values to variables. For example,

   foo(f(A, string B), g/1 A, 3)

might map the term FOO<f(g(5),"bar"), g(5), 3> to the assignment {A ~ g(5), B ~ 6}. Here string and g/1 are type names.

Patterns are defined recursively as follows.

  • A type name is a lowercase identifier that denotes a set of terms. (In some cases it may contain punctuation or spaces: foo/3, foo.mysubtype, and indirect foo.)
  • Variable names are identifiers that start with a capital letter or the underscore. The special "one-time" variable name _ is replaced during preprocessing with a gensym variable name.
  • a typed primitive term is a pattern. For example, "string" or 123.
  • foo X is a pattern, for any type name foo and any variable X. Here foo is referred to as a restrictor.
    This pattern maps any term x of type foo to the assignment {X ~ x}.
  • X is a pattern, for any variable X. It is just like foo X, but without the restriction to type foo.
  • foo is a pattern, for any type name foo. It is equivalent to foo _.
  • foo(p1, ... pk) is a pattern, for any base type name foo, and any patterns p1, ... pk. Here foo is referred to as a pattern constructor.
    (We only allow a base type name here, i.e., one that does not end in an arity such as /3, because the constructor notation already implies that the arity is /k.)
    This pattern maps a functor term of type foo that has arglist <a1,... ak> to the union of the assignments that result from applying p1 to a1, p2 to a2, etc., provided that all these applications succeed and the union of the assignments does not assign conflicting values to any variable.
    Note that the term must have type foo, but that doesn't necessarily imply anything about its functor. Remember that functors cannot be written directly in Dyna.
  • The pattern foo() can be abbreviated simply as foo.
  • If foo is the name of a "pattern type" (see below), then there are one or two other ways to write patterns of type foo, using "keyword constructors" as discussed in a later section. The keywords in question were specified when the type name foo was defined.

Again, a pattern is a PARTIAL function. If a term is in the domain of a pattern, we say that the term matches the pattern or vice-versa.

A pattern can easily be used to define a type -- namely, the set of terms in the domain of the pattern. We'll do this below.

Examples Of Patterns In Inference Rules

We haven't yet seen how to define any type names other than the primitive types. However, let's suppose for the following examples that int and cons are both type names.

Patterns are used in inference rules:

   foo(X) += bar(X).

It may be useful to restrict this rule to the case where X is of a particular type, say int. We can do this by using type restrictors in the pattern:

   foo(X) += bar(int X).
   foo(int X) += bar(X).   % equivalent effect

The entire inference rule is really a pattern with infix pattern constructor +=. It would be matched by, e.g.,

   foo(3) += bar(3).

which means that the value of bar(3) is a summand in the value of foo(3).

Thus, the above restricted rules can equivalently be regarded as meaning

   foo(X) += bar(X) if is_int(X).

Similarly,

   foo(int X) += bar(cons X).

can be regarded as meaning

   foo(X) += bar(X) if is_int(X) & is_cons(X).

Unfortunately, this rule can never fire because the pattern has empty domain -- it does not match any term, assuming that int and cons are disjoint types. We should detect this at compile time if we can.

NOTE: The expressions "is_int(X)" and "is_cons(X)" above are probably just meant to be explanatory. I don't think we need to allow the user to write such expressions directly. The restrictor syntax already allows the user to do almost anything she wants, and is much prettier.
I think the type restrictor syntax lacks only one thing: if the rule (or storedas declaration) only mentions X once,
       sum += bar(X).
then there is no way for it to restrict X to the INTERSECTION of two types. But we can handle that in other ways, perhaps:
       % first somehow declare intcons to be the intersection of int
       % and cons -- see later
       sum += bar(intcons X).
or even by using this hack that is gets the same effect as is_cons:
       sum += bar(int X) if is(cons X).   
                 % where "is" is a dummy function that always returns true
The main reason to avoid the is_cons(X) syntax is only a problem with the surface syntax: since type names may contain punctuation, I don't think it's generally possible to turn an arbitrary type name T into a functor name is_T without confusion.
(In particular, cons/2 is a type name. To test whether X is of type cons/2, would we write is_cons/2(X)? Here that is supposed to mean something like (is_(cons/2))(X), but it is indistinguishable from ((is_cons)/2)/X. In other words, someone would expect is_cons/2 to be the subtype of is_cons terms that have arity 2, but in fact, is_cons/2(X) is being used to pick out terms that are not is_cons terms at all and have arity 1. There are similar problems with type names that contain dots, which we'll see below.)

Abbreviating Restricted Variables

The definition of patterns says that it is legal to use _ for one-time variable names, or simply to omit them if a type restrictor is given. So the following all have equivalent effect:

   sum += bar(int X).
   sum += bar(int _).
   sum += bar(int).

The definition of patterns says that it is perfectly fine to omit type restrictors. Then the rule is not restricted by them. For example, either of

   sum += bar(X).
   sum += bar(_).

is equivalent to any of

   sum += bar(term X).
   sum += bar(term _).
   sum += bar(term).

since the special type term is the union of all named types and therefore does not really impose any restrictions.

In fact, it could be that all terms of type bar/1 happen to have a cons as the first argument. Then the above are also equivalent to

   sum += bar(cons X).
   sum += bar(cons _).
   sum += bar(cons).

Why Define Types?

You need to define some types in order to write interesting patterns. Types are used both as pattern constructors and as variable restrictors.

You may also want to define several variant names for the same type, or for a type and some subtypes of it. Each type name will allow particular keyword patterns that can be used to construct and destructure terms of that type in a particular way. Each name also compiles into a C++ class that is stored in a particular way and may print out in a particular way that indicates its class. So the reason to have multiple names is to support efficient construction, destructuring, and storage.

In general, if a type name is used without definition in Dyna -- particularly as a pattern constructor -- then the preprocessor might be able to infer an appropriate definition from usage. Of course, this might be a bad idea in the case of typos. Probably the compiler should warn about likely typos (e.g., two "similar" type names are used and they are not both explicitly defined).

Defining A Pattern Type

A type name can only be defined once.

The pattern type declaration

  :- double foo(term X, int Y, f(int Y)).

defines the type name foo/3 to refer to the domain of the pattern

  FOO(term X, int Y, f(int Y))

if we let FOO temporarily denote a name for the type of all functor terms with functor FOO. (Remember that boldface FOO cannot actually be written in Dyna.)

Note that foo/3 is now a subtype of FOO. The type name foo is automatically defined to be the set union of all types foo/0, foo/1, foo/2, foo/3 ...

NOTE: The "double" is a value type, discussed later. Ignore it for now. After this section, I am going to omit all value types until they are further discussed!

As a more advanced example, we can use a guard:

  :- double foo(term X, int Y, f(int Y)) if prime(Y).

This defines foo/3 to refer to the set of terms that are mapped by the pattern

  FOO(term X, int Y, f(int Y))

to assignments that assign Y to a variable such that prime(Y).

In other words, if (a1,a2,a3) unifies with (X, Y, f(Y)) such that X is a term, Y is an int, Y is an int, and prime(Y), then FOO<a1,a2,a3> is a term of type foo/3.

Infix pattern constructors are syntactically valid, as usual. We might declare */2 via

  :- double (double X * double Y).

Notes on guards

The material following "if" is called a "guard." It is an optional test appended to the type definition. In the above examples, it would be kosher to consider any boolean expression in terms of X and Y.

Well, not quite any boolean expression! The type of a term is immutable. So it must be possible to evaluate the guard expression without reference to any chart or other program state. In other words, the guard expression (whether an axiom or a theorem) must be "const." We need to work out this concept and a syntax for it.

For consistency with the guards in inference rules, we might allow guards to contain free variables such as Z. But then we would have to force them to start with "if always" or "if ever," rather than just "if," to indicate how to quantify over the free variables.

Pattern Subtypes

A pattern type with a dot in its functor name is treated slightly differently:

  :- foo.mysubtype(0, int X, bar(X, term Y)) if mytest(X,Y).

defines the type name foo.mysubtype/3 to refer to the set of terms that are mapped by the pattern

  foo(0, int X, bar(X, term Y))   % chop off the ".mysubtype"

to assignments such that mytest(X,Y).

foo.mysubtype/3 is now a pattern subtype of foo/3, just as foo/3 was a pattern subtype of FOO/3.

Note carefully that either type is still a set of terms whose functor is FOO! We are not defining new functors in either case, only new type names.

Note carefully that the type is still a set of terms whose functor is foo! We are NOT defining foo.mysubtype here as a functor, but only as a type (and as a constructor; see below).

In other words, the declaration asserts that

If t1, t2, t3 are terms that unify respectively with 0, X, and bar(X, Y) such that X is an int and Y is a term, then foo(t1,t2,t3) is a term of type foo.mysubtype/3.

Of course, foo.mysubtype is just the union of all declared types of the form foo.mysubtype/k.

Pattern subtypes with infix constructors

Infix constructors also need the ability to have pattern subtypes:

  :- pathto(U) *.3 edge(U,V)

uses the *.3 subtype of the * infix functor. This seems like a nuisance for the parser, but zyacc does allow new operators to be defined dynamically with precedences, as the file is being parsed. So we can just define *.3 dynamically.

Not all subtypes are pattern subtypes

foo.b is correctly a subtype of foo here:

  :- foo(X,Y).
  :- foo.b(Y,Y).   

But if we had instead written

  :- foo.a(X,Y).
  :- foo.b(Y,Y).   

then foo.b would still be a subtype of foo.a, even though that is not as obvious from the syntax. That is, every term of type foo.b is also of type foo.a. (On the C++ side, we therefore generate an implicit cast from foo.b to foo.a.)

Pattern subsubtypes

You can also declare subsubtypes:

  :- foo.mysubtype.subsub(int A, int B, int C).

which defines foo.mysubtype.subsub/3 to be a name for the set of terms that match

  :- foo.mysubtype(int A, int B, int C).   % chop off the ".subsub"

Compiler warnings to avoiding confusion with subtype declarations

The following pair of declarations seems likely to be confusing:

 :- funny(f(X),X).
 :- funny.sub(A,g(B)).

One might glance at these and mistakenly think that the type funny.sub/2 includes the term FUNNY<1,g(2)>.

Why doesn't it? Remember that funny.sub/2 is forced to be a subtype of funny -- namely, the domain of the "chopped" pattern funny(A,g(B)). That pattern consists of terms of type funny/2 whose arglists unify with (A,g(B)). Since they are of type funny/2, their arglists must also unify with (f(X),X).

I think the above code should result in a compiler warning, suggesting that the programmer should explicitly write

 :- funny.sub(f(g(B)), g(B)).   % intersection of the two explicit patterns

which has the same effect. The warning is generated because the defined type funny.sub/2 is different from the type we would have gotten without inheritance, i.e., if we'd written the pattern one level up as

 :- funny(A,g(B)).

Zero-depth pattern subtypes

Our earlier definitions allow one to write

  :- foo.mysubtype X if mytest(X).

Again, this defines a set of terms of the form foo(...), namely the ones that are mapped by the TRIVIAL pattern

  foo X

to an assignment where X satisfies the guard.

Or to put this in a form parallel to our earlier definitions,

  If t is a term of type foo that unifies with X such that mytest(X),
  then t is a term of type foo.mysubtype.

Of course foo may be any type, including a primitive type or a union type (see below).

The only difference from using deeper patterns is that we are declaring the entire foo.mysubtype, not just foo.mysubtype/2. So in this case, we have to define foo.mysubtype/2 from foo.mysubtype, not vice-versa as before.

Specifically, we'll implicitly define foo.mysubtype/2 to be all functor terms of type foo.mysubtype that have arity 2. (Note that some foo.mysubtype terms might be primitive terms, which don't have arities at all. They are obviously not included in foo.mysubtype/2.)

In other words, foo.mysubtype/2 is identical to the type defined by

  :- foo.mysubtype.two(_,_).  % what we want, but might give a warning.

If you only wanted to define foo.mysubtype/2 in the firstplace, you could write

  :- foo.mysubtype/2 X if mytest(X).

Some useful examples:

  :- int.prime X if prime(X).   % in this case, int is a primitive type
  :- foo.tagged X.    % foo.tagged is the same type as foo -- there
                      % are no conditions, so it's a subtype that is
                      % equal to the original.  However, the C++
                      % class corresponding to foo.tagged may store
                      % the same term differently than the C++ class
                      % corresponding to foo.
  :- term.u X if is_foo(X) || is_bar(X).  % if we allowed user to write is_foo, is_bar,
                                          % then this would be a way of defining a union type
  :- foo.u X if is_bar(X).     % an alternative way to define the same type as term.u,
                               % again, only if we allowed user to write is_bar
                               %
                               % FIXME: Eric thinks that foo.u is not the same as
                               % term.u, since foo.u inherits all of foo's
                               % restrictions even if they don't apply to bar.

Examples Of Using Pattern Type Names As Restrictors and Functors

Again, suppose we have declared some pattern type like

  :- double foo.mysubtype(0, int X, bar(X, term Y)).

It's fine to use it as a restrictor:

   sum += bar(foo.mysubtype/3 X).   

Also, the "bare" version of the type name (without the "/3") may be used as a functor in a pattern. Thus, one can write

   sum += foo.mysubtype(0,Q,R).

A term matches this pattern iff it has type foo.mysubtype and also has three arguments that match 0, B, C. Given our definition, that means the above is equivalent to

   sum += foo(A1,A2,A3) if A1 ~~ 0 && A2 ~~ Q && A3 ~~ R
                           && A1 ~~ 0 && is_int(A2) && A3 ~~ bar(B, term Y).

Note that examples such as

   sum += foo.mysubtype(list P, Q, R).   % not possible for P to be
                                         % both list as required here 
                                         % and int as required by foo.mysubtype
   sum += foo.mysubtype(P,R,R).  % not possible for R to be both int and bar:
                                 % both are required by foo.mysubtype

should probably fail at compile time because the pattern can never match. (Or equivalently, because the pattern foo.mysubtype(P,R,R) in effect defines an even more restricted "intersection type" which is known at compile-time to be empty. Or equivalently, because the foo.mysubtype "constructor" is GUARANTEED to fail on these arguments.)

Ground patterns are just a particular case of the above, where the domain of a pattern has size at most one:

   sum = foo.mysubtype(0,5,bar(5,nil)).    % a specific term
   sum = foo.mysubtype(1,5,bar(6,nil)).    % fails at compile-time
   sum = foo.mysubtype(1,2,3).             % fails at compile-time

Storage Declarations

Every type name in Dyna corresponds to a class in C++. Instances of that class correspond to terms of the type. The same term may be a member of several named types, which means that it may allow several different representations as statically typed C++ objects.

Names

We need some way of naming the classes that correspond to types with punctuation. I suggest using inner classes:

  Dyna type name    C++ class                   C++ constructor function
  --------------    ---------                   ------------------------
  foo               foo_t                       foo    // returns e.g. foo_t::arity3_t
  foo/3             foo_t::arity3_t             foo    // exploits overloading
  foo.mysubtype     foo_t::mysubtype_t          foo_t::mysubtype
  foo.a.b/3         foo_t::a_t::b_t::arity3_t   foo_t::a_t::b


NOTE: This naming convention doesn't allow pattern subtypes to be named starting with a digit. That is, foo.3 is not allowed since foo_t::3_t and foo_t::3 are not legal in C++. Instead, the user might write foo.v3 or foo.sub3.
(We could allow foo.3 in Dyna if we changed the naming convention so that the corresponding C++ class was foo_t::sub3_t. But then foo.mysubtype in Dyna would correspond to foo_t::submysubtype_t in C++, which would make things less readable on the C++ side.)

Field accessors

An instance of one of these classes represents a particular term. It has I/O methods, and methods to get its arity and its arguments.

Casts

C++ classes that correspond to overlapping types can cast to one another. These casts are checked and explicit if they might fail, but unchecked and implicit if they are guaranteed to succeed -- i.e., a cast from a subtype to a supertype.

Equality, hash, copy

Other constructors that are needed.

Storage declarations

When a type name is defined, it specifies how its corresponding C++ class should be stored in memory. If this storage declaration is omitted, it will be filled in during preprocessing.

So the full form of

  :- foo(list X, int Y, f(int Y)) if prime(Y).

would be something like

  :- foo(list X, int Y, f(int Y)) if prime(Y)
     storedas whatever(X,Y).

where whatever(X,Y) could replaced by any pattern (possibly a deep one!).

The pattern on the left of "storedas" is then stored exactly like the pattern on the right of "storedas". In this case, an instance of foo/3 actually uses an instance of whatever/2 as its storage record.

(Note: When we get to value types, "foo" will be preceded by a value type and "whatever" will be preceded by an sval type.)

Storage of tuples

Where does this ground out? Well, the storage of typed tuples is built-in (using something like the first-fit algorithm in a recent message). The storage record can be a typed tuple of terms:

  :- foo(list X, int Y, f(int Y)) if prime(Y)
     storedas (list X, int Y).

In general in Dyna, I think (a,b,c) should be syntactic sugar for tuple(a,b,c), using the tuple/3 functor. (It is distinct from [a,b,c], which is sugar for cons(a,cons(b,cons(c,nil))), using cons/2 and nil/1.)

More precisely, at least in a storage declaration, (a,b,c) is syntactic sugar for tuple.subtype(a,b,c), where the subtype is defined "on the fly" and is storedas a record whose fields are just big enough to hold a, b, c.

Note that if there is only one variable in the tuple,

  :- s(peano Predecessor) storedas (peano Predecessor).

then the parentheses will just be interpreted as ordinary grouping parentheses rather than syntactic sugar for tupling. In fact, for this reason, tuple/1 doesn't even exist. So the above is parsed into the same abstract syntax tree as

  :- s(peano Predecessor) storedas peano Predecessor.

But that's okay -- we interpret either case "as if" it were a 1-tuple.


FIXME: if we interpret either case as a 1-tuple, why have the special exception for single-element () groups? It would be simpler if we always tuplize. --Eric

Generous storage

The storage declaration may be more generous in its types than necessary. In the first example above, the pattern whatever(X,Y) might actually accommodate any two terms; or the second declaration might have been made similarly, as

  :- foo(list X, int Y, f(int Y)) if prime(Y)
     storedas (term X, term Y).

The only requirement is that it must be possible to construct the given storedas pattern from the variables X and Y in the type definition. In practice, that just means calling the storedas pattern, which will cast X and Y to the necessary types.

It can be useful to use generous storage for the sake of making two classes symbiotic.

A complicated example

Here is a more complicated declaration:

  ... storedas (int X, char 255, whatever(0, Y), Z, (double A, double B))

The top-level tuple has 5 arguments:

 - The type of int X is explicitly specified, so the 
 tuple constructor will cast X to an int.  
 - The type of char 255 is explicitly specified, so the tuple
 constructor will cast 255 to a char.  
 - The type of the third argument is obviously whatever/2.  And the
 types of ITS arguments were specified elsewhere and don't need to be
 specified again here.  The tuple constructor just calls the
 whatever/2 constructor on 0 and Y, so the whatever/2 constructor
 handles any casting that is needed.
 - The type of the fourth argument is omitted, so it will be filled
 in during preprocessing.  (You might think it would be filled in as
 "term Z", but it is inefficient to allocate storage for a general
 term.  Typically, it will be chosen to be the type of Z in the
 pattern being stored, so that no casting is necessary to store Z.)
 - (double A, double B) is another tuple, with type [double,double].
 There is not much reason to nest tuples directly like this, but
 see the next section.
 

Therefore, the storedas tuple has type

  [int,char,whatever/2,ztype,[double,double]].

Possibly we will need to complicate the tuple notation even further to specify alignment and packing in more detail than the first-fit algorithm allows.

Indirect, interned, etc.

Once foo is defined, one could define alternative ways of storing it:

  :- foo.tagged X storedas (char 123, X).

or equivalently

  :- foo.tagged X storedas (char 123, foo X).

is a tagged variant of foo, stored as the byte "123" followed by an ordinary foo. As noted earlier, foo.tagged and foo are different names for the same type; they compile into different C++ classes that store the same terms differently.

Some alternative names for a type are declared automatically. If the Dyna type "foo" compiles to foo_t, then Dyna automatically has a type called "indirect foo" or "foo.indirect." It represents the same type as foo, but compiles to foo_t::indirect_t, which is a smart pointer to foo_t. (Similar deal for interned.)

The obvious use of (e.g.) indirect types is in storage declarations, where they can be used to store

  ... storedas (indirect int X, indirect whatever(0, Y), Z,
                               indirect (double A, double B)).

This is a 4-tuple, three of whose elements are pointers to other objects (in one case, to a nested 2-tuple). One could even add a level of indirection so that the storage is a POINTER to the above 4-tuple:

  ... storedas indirect (indirect int X, indirect whatever(0, Y), Z,
                                   indirect (double A, double B)).

Here's an interesting example. foo is indirect, and foo.d is the corresponding direct type:

  :- foo(A,B,C) storedas indirect foo.d(A,B,C).
  :- foo.d(A,B,C) storedas (A,B,C).   % or, storedas mytriple(A,B,C)

What's interesting is that foo.d's definition depends on foo's definition (it is a subtype), but foo's implementation depends on foo.d's implementation -- which is the other way around. That is fine -- we define the formal types and their implementations in natural order.

Indirect and interned types are full-fledged types that can be used anywhere, not just in storage declarations. (See the later section on "optimization by pattern specialization.") However, I'm not sure I have any use cases where there is a real benefit from using them elsewhere.

Besides indirect and interned, we might also want "tagged" or "boxed" as a shorthand for generating standardly boxed versions, even though it is possible to define foo.tagged manually as shown above.

Automatic storage declarations

If a storage declaration is omitted, how is it filled in during preprocessing? Ultimately that's up to the optimizer, I think. But there seem to be three natural approaches:

  :- foo.mysubtype(list X, int Y, f(int Y)).

could be naturally storedas any of

  foo(X,Y,f(Y))               % foo.mysubtype is stored exactly as
                              %   the same foo would be stored
                              %   ("inherited storage")
  (X, Y, f(Y))                % a tuple of the arguments ("natural
                              %   storage" -- the storedas
                              %   declaration matches the pattern 
                              %   being stored)
  (X, Y)   % a tuple of the variables used, duplicates eliminated

Foreign storage

Another kind of storage declaration is to write

  :- foo(int X, Y, f(Y)) storedas foreign "fooclass".

That means that "fooclass" is a C++ class that has been defined by someone else to support all the methods that we need. We can optionally generate a skeleton for this that the user can fill in. fooclass needs a two-argument constructor that would be passed X and Y. It also needs field accessors and keyword accessors (see below). And it needs all the usual methods for copy, equality, etc.

See ticket #227 for why we might like to allow foreign implementations of compound terms.

However, the most important reason for foreign implementations is simply to declare new PRIMITIVE term types:

  :- complex X storedas foreign "complex".
  :- intset S storedas foreign "set<int>".

Actually, since the variable X in each case is used only once, it could be renamed to _ or even omitted:

  :- complex storedas foreign "complex".
  :- intset _ storedas foreign "set<int>".

It would probably cause an compilation error to write only

  :- complex X.

without any storedas declaration, since there is no obvious storedas declaration to infer for this new class of objects.

Improving Patterns Further

Pattern subtypes with storage declarations make it possible to store a particular pattern efficiently. However, we would also like to be able to construct and analyze that pattern efficiently.

The next section (keywords) gives a solution to this problem, with some extra benefits.

And the following section (aliases) gives a different solution that mainly allows us to choose new names for pattern subtypes (so that we are not stuck with foo.mysubtype).

KEYWORD ACCESSORS AND KEYWORD CONSTRUCTORS

The old way

In Dyna 0.3, we had named fields:

  :- structure(constit(string nonterm, int start, int end)).

These names are nice for three reasons:

  • self-documentation of the Dyna code
  • convenient access methods in the C++ code
  • could possibly serve as keyword arguments,
    • as in
      constit(start=3, end=8, nonterm="np").

The new way

Here is a redesign. It takes the named accessors for a type to be the names of the VARIABLES that were used in the type's definition. That means that they may access something deeper than the top-level FIELDS.

(The top-level fields can still be gotten via the standard field accessors arg0, arg1, etc.)

One cool consequence of this approach, as we'll see, is that the compiler can give a warning or error on a Dyna program that names variables in an inconsistent way across type definitions and/or inference rules.

Here are a couple of type name declarations to illustrate things:

  :- constit(string Nonterm, int Start, int End).

The C++ class constit_t will have keyword accessor methods Nonterm(), Start(), and End().

  :- edge(vertex, vertex).
  :- edge.loop(vertex(string Name), vertex(string Name)).

The C++ class edge.loop will have a single keyword accessor method, Name(), which returns type string_t. Of course it also still has the standard field accessors arg0() and arg1(), which return type vertex_t.

Constructors by keyword

A pattern constructor in the Dyna code can be used with keyword arguments (in any order) instead of ordinary arguments:

  constit(Start~3, End~8, Nonterm~"np") % same as constit("np",3,8)
  edge.loop(Name ~ "new york")          % same as edge.loop(vertex("new york"), vertex("new york")).

I have used ~ in the keyword syntax rather than the conventional = because we are unifying terms, not their values. In fact, the above can be read as equivalent to

  constit(Nonterm,Start,End) if Start ~~ 3 && End ~~ 8 && Nonterm ~~ "np"
  edge.loop(vertex(Name),vertex(Name)) if Name ~~ "new york"
  % not quite legal syntax because the "if" clause would not
  % immediately follow the pattern, but rather come at the end
  % of the type definition or inference rule

(However, I admit that using ~ makes the keyword syntax visually ugly, and it might be worthwhile using = instead or permitting it as an alternative.)

These would presumably compile into something in C++ like

  constit_keywords("np",3,8)    // note that compiler had to reorder arguments
  edge_t::loop_keywords("new york")

where one mimics Dyna's pattern constructor on ground terms by calling a special C++ constructor function, *_keywords(), whose arguments correspond to the VARIABLES (in the order of first mention). Of course, as a C++ function it doesn't really have keywords, but it does differ usefully from the usual constructor function, whose arguments correspond to the FIELDS.

In particular, edge_t::loop_keywords("new york") may be quite a bit more efficient in C++ than edge_t::loop(vertex("new york"), vertex("new york")), even though they have the same effect. After all, the latter has to construct two vertices and then check that they are equal. The former can drop "new york" right into the storedas declaration of edge.loop.

Although C++ doesn't support real keyword arguments, Python does. So if we eventually generate Python bindings for the compiled code, THOSE can take keywords.

It might be convenient in Dyna to have a positional pattern constructor syntax that works like the C++ keywords constructor, where the arguments bind to the pattern variables in order of first mention. Then instead of writing

   edge.loop(Name ~ "new york")
   edge.loop(Name ~ Name)

you could write something like

   edge.loop{"new york"}
   edge.loop{Name}

Mixed keyword construction

Languages with keyword constructors usually also allow you to write a mixed form where the first several arguments are bound positionally and the remaining ones are bound via keywords. We could allow this:

  constit("np", Start ~ 3, End ~ 5)

Note that positional arguments correspond to fields, while keyword arguments correspond to variables. So in the selfloop example above,

  selfloop(vertex("baltimore"), Name ~ "new york")

would be equivalent to

  selfloop(vertex("baltimore"), vertex(Name))) if Name ~~ "new york"

where only the second field of selfloop is copied from the type definition. Probably no one will ever use this mixed form for nested pattern types, but at least this is a consistent way of defining it.

Keyword construction and overloading

It is possible that both constit/2 and constit/3 have a single keyword, Start. In that case, constit(Start ~ 3) is a pattern that matches multiple terms, just like u(4,5) when u is a union type.

The programmer could specialize the pattern by writing constit/2(Start ~ 3) or constit/3(Start ~ 3) -- i.e., we should allow type names with arities as keyword constructors.

Default arguments in keyword construction

Languages with keyword constructors usually also allow default arguments. We could allow that in Dyna by giving specifying defaults in the type definition, like this:

  :- constit(string Nonterm ~ "s", int Start, int End ~ =Start+1).

Now if Nonterm is omitted from a keyword constructor, it defaults to "s", and if End is omitted, it defaults to be =Start+1. Start may not be omitted because no default was specified.

This means that constit(Start ~ 3) is sugar for constit("s",3,=3+1). And constit(Start ~ Start) is sugar for constit("s",Start,=Start+1).

Name checking

Part of the conventional reason for keyword arguments is so that you don't get mixed up and pass arguments around in the wrong order.

Now that variable names are supposed to be meaningful, here is a further remedy for that problem that is independent of keyword arguments. The user can safely write any of these patterns,

  constit(X,Y,Z)
  constit(Nonterm,Start,End)
  constit(Nonterm,I,J)

but if the user writes

  constit(I,J,Nonterm)

then the compiler should generate a warning!

The principle is that constit defines Nonterm as an accessor, so any variable named Nonterm that appears inside a constit functor (even deeply nested) should be expected to be bound to the same value that that accessor would have returned.

Notice that under this policy, it is fine to write

  constit(Nonterm,End,End)   % zero-width constituent

since End is appropriately bound to the value that would be returned by the End accessor. (It is also bound to the value that would be returned by the Start accessor, since that is required to be the same; but that's irrelevant.)

The reason to restrict the use of names even when deeply nested is that if we define edge/2 as

   :- edge(vertex(Start),vertex(End)).

then I feel we ought to detect the error in the pattern

   :- edge(vertex(End), vertex(Start))
   

The restriction on nested variable names means that if we define the Peano integers like this,

  :- zero.
  :- s(peano Predecessor).
  % where peano is declared as a union of {zero, s}
  % We'lll discuss a syntax for that later

then it is not okay to write

  s(s(Predecessor))

because although the inner pattern's Predecessor() accessor does return Predecessor, the outermost pattern's Predecessor() accessor returns something else, so the outermost pattern fails name checking. You would need to write something like

  s(s(MinusTwo))

I tend to think this is a good thing, but I am not 100% sure.

There might be some exceptions to name checking if you use keyword arguments. For example, it might be allowed to write

   constit(Nonterm, Start ~ End, End ~ Start)

because then the order-switching is clearly deliberate. We'd have to think out what the precise conditions are in the case of nested terms.

Dummy names (unchecked names)

In the above Peano integer example,

  :- s(peano Predecessor).

suppose one had instead defined

  :- s(peano X).

The name X isn't intended to be meaningful. So it would be kind of annoying to get warned for writing s(s(X)).

This problem can be avoided by naming dummy variables with dummy names -- names starting with underscore:

  :- s(peano _X).

Name checking does not apply to dummy names. So the above definition relinquishes any claim on the name _X. The user is now free to write s(s(X)) or s(s(_X)) -- whatever variable name they write in a pattern, it will never be warned about.

(Though _X remains a keyword as usual: so s_t in C++ stil has an _X() keyword accessor, and s(_X ~ zero) in C++ still works as a keyword constructor. This is not so useful to human coders, but the consistency will be helpful for machine-generated code.)

The most common case of dummy names is

  :- s(peano).

which, remember, is equivalent to

  :- s(peano _).

which starts with an understcore. (_ is never a keyword -- it can't be, in fact, because there may be multiple _ names in the same declaration, which are not required to unify: they are translated internally to _(1), _(2), etc.)

You can use dummy names outside type definitions, too. For example, rather than write s(s(X)) in an inference rule, which might run afoul of name checking (depending on how s/1 was defined), you might want to write s(s(_X)). That's guaranteed to work, since even if s/1 has an accessor named _X, you know it won't be checked. In short, patterns that use dummy names are safe. This trick is useful mainly when generating code automatically.

Possibly the set of dummy names should be bigger than just those starting with _. For example, perhaps any name of the form [A-Z][0-9]* (a single letter optionally followed by some digits) should be regarded as dummy.

Name checking across pattern subtypes

I think variable names should also be required to be consistent across the various named types foo, foo.*, foo.*.*. So the above policy can be strengthened as follows.

Let alpha be a pattern foo...(...) that is used in a type definition, to define foo or one of its pattern types or subtypes. Let K be the set of non-dummy keywords in alpha.

Let beta be another pattern foo...(...) that is used anywhere -- in a type definition, a storage clause, an inference rule, whatever.

Suppose also that alpha and beta unify (i.e., they have some term in common -- this should take type restrictors and guards into account when possible).

Then any k in K that appears in beta must be bound to k in alpha by the unification, or else the compiler will generate a warning.

Example:

  :- foo(X,Y,Z).
  :- foo.a(A,B,C).
  :- foo.b(C,B,Z).

is not okay since when foo.a(A,B,C) unifies with foo.b(C',B',Z'), C' is not bound to C. This would generate a warning. On the other hand,

  :- foo(X,Y,Z).
  :- foo.a(A,A,B).
  :- foo.b(B,A,A).

is okay since when foo.a(A,A,B) unifies with foo.b(B',A',A'), then A, B, A', and B' are all unified, so in particular A' is bound to A and B' is bound to B. Also,

  :- foo(X,Y,Z).
  :- foo.a(int A, int B, int C).
  :- foo.b(list C, list B, list A).

is fine since foo.a and foo.b don't unify -- they have no terms in common. But one would get a warning when writing foo(A,B,C) in an inference rule, unless the guards on the rule ensured that A, B, C could not all simultaneously be lists, which would make that foo an instance of foo.b.

In short, the policy ensures that if any foo-variant term in C++ is upcast, downcast, or sidecast to another foo-variant class, any accessors that work both before and after the casting should give the same answer.

The main rationale is to make code more readable and warn about potential errors.

As a special case, it warns about possible errors due to pattern specialization (see above). If the programmer writes x.arg1().A(), she might think she is calling A() on a foo_t object. But perhaps the compiler has done pattern specialization so that x.arg1() actually returns an object of the more efficient subtype foo_t::b_t. Then we would like x.arg1().A() to return the same thing as if it had been written as x.arg1().to_foo().A(). The policy ensures that we'll at least get a warning if it would return something different. HOWEVER, that is only a warning -- and the policy does not guarantee that x.arg1().A() will be defined at all! The next section fixes these problems.

Inheriting keyword accessors across pattern types

The above policy applies when alpha and beta are overlapping. Let's do something stronger when beta (like alpha) is used to define a type, and specifically a SUBTYPE of alpha (i.e., EVERY beta is an alpha).

In this case, perhaps alpha's named accessors should be "inherited" by beta as well. Then pattern specialization will really work: in the above example, x.arg1().A() is guaranteed to be defined and to mean the same thing as x.arg1().to_foo.A().

For example, consider the pattern subtype definitions

  :- constit(term, term, term).
  :- constit.any(category Nonterm, int Start, int End).
  :- constit.epsilon(category(string Name), int End, int End).

where constit.any and consit.epsilon play the roles of alpha and beta. Observe that any constit.epsilon is a constit.any, and we generate an implicit cast to that effect.

It's clear that constit.epsilon has keywords Name and End. So you can write

   constit.epsilon(Name ~ "np", End ~ 3)

and if you have a constit.epsilon object on the C++ side, then it has Name() and End() accessors.

The proposal is that constit.epsilon on the C++ side should ALSO have accessors Nonterm() and Start(), "inherited" from the supertype constit.any.

To be precise: If x is a constit.epsilon object, then x.Nonterm() would be defined to return the same thing as ((constit_t::any_t)x).Nonterm(). However, the accessor should be implemented without actually casting to constit. (Remember that constit.epsilon might be stored quite differently from constit.any, in which case a cast may be expensive.)

If we inherit keyword accessors, does that mean that one should be able to use the keywords Nonterm and/or Start when using constit.epsilon as a keyword constructor? I think not. The keyword constructor for constit.epsilon should only take two keywords, Name and End. It is probably possible to figure out a consistent way to mix the two sets of keywords, but it doesn't seem very worthwhile, since why would anyone want to do that? It would look confusing. And we wouldn't be able to emulate that mixed behavior in the foreign language interface -- in the constit_t::epsilon_keywords constructor in C++, nor in a Python binding for the constit.epsilon constructor.

Notice that if you got the arguments of constit.epsilon in the wrong order,

  :- constit.epsilon(int End, int End, category(string Name)),

then constit.epsilon would not be a subtype of constit.any, so we'd get no inheritance of accessors. We wouldn't get warning messages either -- since constit.epsilon and constit.any don't even overlap. We'd just be treating this as a deliberate overloading of constit, where the arguments were ALLOWED to show up in different orders.

By contrast, you would get both a warning and an error in this case of misordered arguments:

  :- constit(category Nonterm, int Start, int End).
  :- constit.epsilon(End, End, Name).

The warning is that End is misused. How so? Because you are defining constit.epsilon to be the type of terms that match constit(End, End, Name), and the IMPLICIT use of the constit(End, End, Name) pattern is run through name checking.

The error is that the constit(End, End, Name) pattern is empty. It can never match anything, because End can't be both a category and an int (i.e., empty type intersection). This has nothing to do with variable names: you'd get the same error even if you tried to use constit(Y,Y,X) in an inference rule, or to define

  :- constit.epsilon(Y, Y, X).

ALIASES

Suppose you have declared

   :- vertex(string).
   :- edge(vertex U, vertex V).

Instead of writing

   :- edge.loop(vertex(Name), vertex(Name)) storedas Name.

you can write

   :- selfloop(string Name) storedas Name.
   :- selfloop(Name) ~ edge(vertex(Name), vertex(Name)).

or combine the above pair of declarations into one,

   :- selfloop(string Name) ~ edge(vertex(Name), vertex(Name)) storedas Name.

Now selfloop/1 is basically just like edge.loop/2, but it has a different positional constructor and probably prints differently upon I/O.

In general, we could write things like

  :- foo.sub(int A, pair(B,B)) ~ blah.sub.sub(A,g(A),B).

Formally, the meaning of ~ is to make two terms considered equivalent ("equiv") for the purposes of pattern matching, values, equality testing (== in C++ and ~~ in Dyna), and casts in both directions. (But not for the purpose of name checking or I/O.)

selfloop("foo") is a separate term from edge(vertex("foo"), vertex("foo")), but the above operations should be redefined to refer only to equivalence classes of terms. At least I think that's the best way to think about it.

A given term, such as selfloop("foo"), is only allowed to match at most one pattern to the left of ~. If so, it is considered to be an "alias" for the instantiated pattern on the right of ~.

Matching only one means that at least pattern matching, etc., will be deterministic.

We might require that the directed graph on named types defined by ~ should be acyclic (including no self-loops). That prevents cycles and infinite regress when trying to de-alias a term or a pattern (for pattern matching, == testing, etc.).

ON-THE-FLY PATTERNS USED IN INFERENCE RULES

Note that if foo.a(X,f(X)) appears in an inference rule, we may have to test whether a term matches that pattern. We may also have to construct that pattern when X is known.

These are the same operations that we need to do with named patterns. Therefore, it might be convenient to transform the program so that new subtypes are declared for patterns that appear in inference rules. In the case above, we'd be implicitly declaring something like

  :- foo.a.temp123(X,f(X)) storedas foo.a(X,f(X)).

Then we can easily test whether an item matches the pattern by asking whether it has type foo.a.temp123. Or to construct the pattern efficiently, given X, we can use the keyword notation to be described in a later section, namely foo.a.temp123(X ~ X) or foo.a.temp123{X}.

As noted earlier, an entire inference rule (or its antecedent expression) is itself a pattern. We'll probably want to declare subtypes to represent these patterns, since we return them as backpointers.

OPTIMIZATION BY PATTERN SPECIALIZATION

As we've discussed, there are C++ casts defined between any pair of named types that overlap (i.e., they have terms in common). These are checked explicit casts in general, but unchecked implicit casts if they are guaranteed to succeed (i.e., the input type is a subtype of the output type).

For example, there are casts among pattern subtypes, between unions and their member types, etc.

If the Dyna programmer writes a pattern, then the compiler pipeline is free to optimize by replacing it with any other pattern that matches the same set of terms.

As an example, here's how we handle overloading (I'm including the value types in these declarations, although they have been suppressed above):

   :- term plus(term, term).   % can be omitted in favor of an automatic declaration
   :- int plus.i(int,int).
   :- double plus.d(double,double).

If the user writes simply plus(3,5) or plus(int X, int Y), then the compiler might replace this with plus.i(3,5), as a more specific subtype that matches the same set of terms. In general, more specific patterns may have more efficient storage (although they could be slower in some cases).

In principle, the compiler is even free to invent a new subtype matching exactly the pattern that the user provided, as noted in the last section.

The particular named types used in the pattern makes no difference when the pattern is only being matched against an existing term representation -- then it will match in exactly the same circumstances.

But the particular named types do matter if we are constructing a new term to match the pattern or part of the pattern, because then the pattern's storage declaration comes into play.

Consider a compiler optimization that specializes

  :- bar(f(X),Y) storedas foo(X,g(Y)).

to

  :- bar(f.a(X), Y) storedas foo.b(X, g.c(Y)).

The storedas clause certainly cares what named types are used -- it is borrowing the storage techniques of foo.b and g.c. Those pattern constructors are called (literally or in effect) whenever a bar is constructed.

The named type f.a also matters, because f.a(X) must be constructed whenever a bar's arg0 is accessed.

(Probably g.c should be chosen to be the type that foo.b uses to store its arg1, so that the foo.b constructor doesn't have to cast it to that type. We are still stuck with having to build up the storage with two constructor calls, but at least we avoid the cast. Alternatively, we *might* be able to reduce the number of constructor calls. The storage declaration above *directs* us to call g.c and foo.b, but one could replace it with another storage declaration that replaces foo.b(X,g(Y)) with however *it* is stored. That would lead us to generate different code. Whether it's a good idea depends on whether it's stored as (X,Y) (one call) or as (X,g(Y),g(Y),g(Y)) (four calls).

To block such optimizations (if you want to write or generate low-level code), write

  :- bar(f.(X),Y) storedas foo.(X,g.(Y)).

where the trailing period says to really use the plus type as it stands, not any subtype.

Similarly, in inference rules, consider specializing

 foo(f(X), Z) += bar(X, g(Y)) * baz(Y, Z).

to, say,

 foo.a(f.b(X)) += bar(X, g.c(Y)) * baz.d(Y).

If we're forward-chaining, then foo.a and f.b constructors are called to build the consequent. And if we're forward or backward chaining, then we may have to build the ground arguments of an antecedent in order to look up the rest in the chart; so we may have to call g.c and baz.d.

(In practice, we have to build query terms and look up their iterator values; we'll have to think about the patterns for building those.)

Another possible specialization is to use indirect types, e.g.,

 foo.indirect(f.indirect(X)) += bar(X, g.indirect(Y)) * baz.indirect(Y).

or equivalently

 indirect foo(indirect f(X)) += bar(X, indirect g(Y)) * indirect baz(Y).

However, I don't see much point in this. The indirect constructors will just call the direct constructors anyway. It is fine to just use the direct constructors, and then have them cast implicitly to indirect if they are used in a context that wants indirect: that cast is exceptionally cheap.

UNION TYPES

Basic declaration syntax

We'll want some simple way of defining union types and probably also intersection types. Earlier I noted a conceptual way of doing it:

   :- term.u X if is_foo(X) || is_bar(X).  % if we allowed user to write is_foo, is_bar,
                                           % then this would be a way of defining a union type

The actual current syntax for unions in Dyna 0.3 is

   :- union(u, [foo,bar]).

But this looks very different from the pattern type definitions we've been talking about until now.

We could use the name (foo|bar) to specify a union type in a type restrictor -- and similarly (foo&bar) for an intersection type. But that would not (yet) allow a name or a storedas clause for the union.

Here is a possible syntax for unions and intersections that builds on aliases:

  :- u X ~ (foo|bar) X storedas {foo.tagged X, bar.tagged X}.
  :- i X ~ (foo&bar) X storedas foo X.

which is the same syntax as

  :- selfloop(X) ~ edge.loop(X,X) storedas X.

As usual, storedas clauses would be filled in if omitted. Even so,

  :- u X ~ (foo|bar) X.

seems like it might be too awkward for end users. Maybe we could get away with dropping some elements:

  :- u ~ foo|bar.

If the user wants to drop hints here about storage, of course they can do the usual type specialization and write

  :- u ~ foo.tagged | bar.tagged.

Storage

The {foo.tagged X, bar.tagged X} storage notation above simply overlays the storage of the member types. So when defining a union, it is necessary to use types whose storage can be discriminated:

  :- foo.tagged X storedas indirect (char 123, X).
  :- bar.tagged X storedas indirect (char 124, X).

More later about laying out storage to make this possible. The {...} notation may need to be extended to also specify HOW to discriminate the types. It may involve deep comparisons or range checks.

Using union types as pattern constructors

It is easy to see that one could use u as restrictor in a pattern:

   sum += bar(u X).   

More subtly, one could use u as a pattern constructor. We saw earlier how to do this with pattern subtypes like foo.mysubtype, and the same principles apply here. Thus,

   sum += u(A,B,C).

sums over all terms of type u that have 3 arguments that match A,B,C. That is completely consistent with the handling of foo.mysubtype(A,B,C).

I'm not sure whether name checking should apply to patterns like u(A,B,C).

Note that u(3,4,"five") is not necessarily a term, despite appearances. It is a pattern that may match 0 things or many things. It matches all terms whose type is u and whose arguments are 3, 4, "five".

   sum += u(3,4,"five").   % sums over foo(3,4,"five") and bar(3,4,"five")

This is similar to the earlier observation that if we've defined

  :- double foo.mysubtype(0, int X, bar(X, term Y)).

then foo.mysubtype(1,2,3) is not a term -- it is a pattern that matches nothing (leading to a compile-time error).

We might also allow this pattern to be used as a consequent:

   u(3,4,"five") += 99.

which is equivalent to

   foo(3,4,"five") += 99.
   bar(3,4,"five") += 99.

This is spiritually similar to having a variable on the left-hand side that wasn't on the right-hand side, but we could reasonably allow it since it's only a finite number of cases.

Using u as a functor does get tricky, for the following subtle reason. Suppose that foo(3,4,"five") and bar(3,4,"five") are equiv (i.e., the "same" term). In that case u(3,4,"five") refers to that single term, and we would only want to add ONE thing to sum, or increment ONE thing by 99.

But how can it happen that they are equiv? Either thanks to an equiv declaration using "~", or more simply, in the case where we are taking a union over pattern subtypes, which may easily be equiv:

   :- baz.a(A,A,B).  
   :- baz.b(A,B,B).  
   :- baz.u X storedas {baz.a, baz.b}.  
   sumone += baz.u(3,3,5).    % adds baz(3,3,5), which is ~~ baz.a(3,3,5)
   sumone += baz.u(3,3,3).    % THE TRICKY CASE:
                              % adds baz(3,3,3) which is ~~ baz.a(3,3,3)
                              %   and also ~~ baz.b(3,3,3) but we must take
                              %   care to only add it once (under either 
                              %   forward or backward chaining).
   baz.u(3,3,5) += 99.
   baz.u(3,3,3) += 99.   % THE TRICKY CASE

Casting and construction of union types

Again consider

   :- baz.u X storedas {baz.a, baz.b}.  !!! fix syntax

or for that matter

   :- u X storedas {baz.a, baz.b}.

What happens on the C++ side if we cast a term x to this union type?

If x already has type baz.a or baz.b, then there is basically nothing to do -- just copy it into a term of type u. (Which could have a larger size in bytes.)

Otherwise, I think we should first try casting it to baz.a and then, if this doesn't work, to baz.b. In other words, it tries the types in the order they're listed inside the {...} storage specification.

What happens on the C++ side if we use u as a constructor, e.g., u(3,5,5)?

A constructor function for u/3 should be defined on the C++ side only if the pattern u(A,B,C) is guaranteed at compile time to match at most one actual term when A, B, and C are all ground.

If so, the constructor function tries calling baz.a(A,B,C) if it can, and uses baz.b(A,B,C) if it can't. If neither works, as in the case u(3,4,5), then it fails with an exception.

For some statically typed arguments, we may be able to determine at compile time that the constructor function will construct baz.a or baz.b. We should overload the constructor function so that it actually returns baz.a or baz.b in those cases (rather than u). In general, we always want to return static types that are as strong as possible, for future efficiency.

Pattern subtypes of a union type

Since union types can be used as pattern constructors, we can declare pattern subtypes of a union type. For example,

  :- u.three_in_a_row(A,A,A).

defines u.three_in_a_row to be anything that matches the pattern u(A,A,A). That makes it equivalent to (foo.three_in_a_row | bar.three_in_a_row).

In fact, u/3 is defined automatically as if it meant

  :- u.three(A,B,C).

which is equivalent to (foo/3 | bar/3).

Processing order of pattern subtype declarations

Consider this example from above:

   :- baz.u X storedas {baz.a, baz.b}.
   :- baz.a(A,A,B).  
   :- baz.b(A,B,B).  

There is clearly a dependency graph among these types: baz.u depends on baz.a and baz.b, and all three depend on baz. In practice, we could make this dependency graph and process the definitions in topological order.

We might CONSIDER even allowing this, for convenience (e.g., we do it for the Peano integers example below):

   :- baz X storedas {baz.a, baz.b}.
   :- baz.a(A,A,B).  
   :- baz.b(A,B,B).  

so that the top-level baz type is a union over some implementations. This is just for naming convenience, so I'm not sure it's really needed. But it is very handy -- note that we are still enforcing that baz.a and baz.b are subtypes of baz. And if there were a baz.c, not included in the union, then we would declare it as a pattern subtype of baz.

Formally, we could handle this as follows:

We'd break the cycles in the dependency graph by making baz.a and baz.b depend not on their parent, baz, but rather on its parent, in this case the universal BAZ type (see the section "Pattern type declarations" earlier).

The general principle is that when we construct the dependency graph, the last thing we add is the links from each pattern subtype to its parent type. If baz.a.c(...) must be defined before baz.a(...), then instead of setting baz.a.c to be the type defined by the domain of pattern baz.a(...), we use pattern baz(...). If that didn't work either, we'd try pattern BAZ(...).

At the end, after baz.a had been defined, we'd check that baz.a.c really was a subtype of it. This is so in the common case where baz.a is defined as a union over its apparent pattern subtypes.


Implicitly defined types

We've already noted that if term is not defined by the user, it is implicitly defined to be a union of all types used by the program (foo|bar|int|...).

Other implicitly defined types include axiom, item, etc.

These types and their implementations are added during preprocessing. The implementation is not always obvious since we could implement (foo|bar) as {foo,bar} but also as {foo.a,foo.b,bar.a,bar.b,...}

We've also noted that foo/3, u/3, term/3, etc. are automatically defined. However, I think there are never explicit written declarations for these.

A USEFUL EXAMPLE

Here's the obvious way to define Peano integers:

  :- peano ~ zero | s.
  :- zero.
  :- s(indirect peano Pred).

Storage

The above is expanded by preprocessing into

  :- peano X ~ (zero X | s X) storedas {zero X, s X}.
  :- zero storedas ().
  :- s(indirect peano Pred) storedas (Pred).

and then the last line is expanded again into

  :- s(indirect peano Pred) storedas (indirect peano Pred).

The storage declarations were guessed automatically (see "Automatic storage declarations" above).

What would have happened if the original program had read

  :- s(peano Pred).

without the "indirect" specifier? That wouldn't make any difference to s/1 as a type, since "peano" and "indirect peano" are equal types and therefore have exactly the same effect as type restrictors. However, a dumb method for guessing storage declarations might then guess

  :- s(peano Pred) storedas (peano Pred).

leading to an infinite storage recursion (which g++ will catch if dynac doesn't!). A smarter method for guessing storage declarations might notice this problem. Or we could just use the default method that Dyna currently uses, in which all terms are stored as interned pointers:

  :- peano X ~ (zero X | s X) storedas interned indirect {zero X, s X}.
  :- zero storedas interned indirect (char 123).                      % 123 is a tag value for zero/0
  :- s(peano Pred) storedas interned indirect (char 124, peano Pred). % 124 is a tag value for s/1

Transformation to a more efficient version

Here's a version that stores Peano integers mod 4. I'll introduce a little syntactic sugar for easily defining tagged unions (I'm not sure this is the right sugar exactly):

  :- peano ~ tagged indirect (zero | s).
  :- s ~ tagged indirect (s.mod0 | s.mod1 | s.mod2 | s.mod3).
  :- peano.mod0 ~ tagged indirect (zero | s.mod0).
  :- zero.
  :- s.mod0(s.mod3 Pred).
  :- s.mod1(peano.mod0 Pred).
  :- s.mod2(s.mod1 Pred).
  :- s.mod3(s.mod2 Pred).

Here the third line, for example,

  :- peano.mod0 ~ tagged indirect (zero | s.mod0).

is intended as sugar that would be preprocessed into a union of automatically generated tagged versions,

  :- peano ~ (zero.indirect.tagged | s.mod0.indirect.tagged).
  :- zero.indirect.tagged X storedas (bit 1, zero.indirect X).
  :- s.indirect.tagged X storedas (bit 0, s.mod0.indirect X).   
  

and the s.mod2 line, for example,

  :- s.mod2(s.mod1 Pred).

is preprocessed to get the obvious storage declaration,

  :- s.mod2(s.mod1 Pred) storedas (s.mod1 Pred).

What is the consequence?

  • The s object representing 6 would be stored as a tagged pointer
 whose free bits have been munged to indicate that it is an indirect
 s.mod2.  
  • If we follow that pointer, we find a direct s.mod2 representing 6.
  • As shown by the s.mod2 storage declaration above, that direct s.mod2 is
 symbiotic with an direct s.mod1 representing 5 which is symbiotic
 with a peano.mod0 representing 4.
  • That peano.mod0 representing 4 is a tagged pointer to a direct
 s.mod0 representing 4, which is symbiotic with direct terms
 representing 3, 2, and 1, and a peano.mod0 representing 0.  
  • This last peano.mod0 is a tagged pointer to an empty record of type
 zero.

In short, s 6 points to peano.mod0 4 which points to peano.mod0 0 which points to zero.

How about peano 6? It would be a tagged pointer to s 6, the tag indicating that this peano integer is an s, not a zero.

If at least zero were interned indirect in the union, then we wouldn't even need to tag the peano.mod0 union because it would already be discriminable on the basis of zero's address:

  :- peano.mod0 ~ (interned indirect zero | indirect s.mod0).

And by the same trick, the peano union could then lose its extra level of indirection, so that peano 6 becomes symbiotic with s 6:

  :- peano ~ (interned indirect zero) | s.    % remember that s is itself a 4-way union

Of course, it is also possible to intern s:

  :- s ~ tagged interned indirect (s.mod0 | s.mod1 | s.mod2 | s.mod3).

Remember that symbiotic types can be interned in the same place, so s.mod2.indirect.interned 6 and s.mod1.indirect.interned 5 will be the same pointer, and s 6 and s 5 will be tagged versions of that pointer.

Warning: what would happen if you wrote interned tagged indirect instead of tagged interned indirect? Then we'd have s.mod2.indirect.tagged 6 and s.mod1.indirect.tagged 5, which would no longer be symbiotic -- they'd have different memory representations because of the tag. So they would end up being interned separately in a hash_set of canonical tagged pointers, whose equality test would have to mask out the tag (if equal) and then follow the pointers to do a deep comparison. The hash_set would therefore be 4 times as big. (Although there's a little bit of compensation in the fact that that the equality tests during hash lookup would be faster since 3 out of 4 comparisons would fail based on the tag, without having to actually follow the pointers.)

Now, what happens if you write s(s(s(s(s(s(zero)))))) in C++? We want all the intermediate results to be statically typed, and for the result to come out with static type s.mod2. This will happen if the C++ code properly overloads the s/1 union constructor function as discussed above.

For example, we can tell at compile time that zero has type zero_t. That lets us tell at compile time that s(zero) will be returning an s_t::mod1_t, since s.mod1 is the first member of the s union (in fact the only member) that can succeed on an argument of type zero. That in turn lets us tell that s(s(zero)) will be returning an s_t::mod2_t, etc.

Personal tools
Namespaces

Variants
Actions
Navigation
Tools