Errors are handled declaratively. Thus, * errors have provenance; * the errors that we get don’t depend on the execution strategy (in
the single-fixpoint world);
There is at least one special $error value. We may need many such values that are particular error tokens (like gensyms) and carry messages around and may have specific types.
Where errors originate:
How errors are consumed:
So, is it an error to ask for 5 is 10/X? How about 5 is 10/0? (Note that 10 is X*5 and 10 is 0*5 are not errors; the latter just fails.)
nwf’s opinion is that these just fail (return null) without an error. 10/0 returns a special $error value that doesn’t unify with 5. Handling $error like an ordinary value will certainly make it easier to catch exceptions by writing rules that unify with $error. A downside of the approach is that while prime(0) is an error, true is prime(0) is simply null.
Another approach says that even attempting to unify a non-error with $error gives an error. In this case, it’s an error to even inspect the value of prime(0). And the query f(5) would match against a rule head f(10/0), giving an error. Basically, deriving any value for f($error) would add an $error aggregand to contrib(f(X)) ... This version may not work well because ordinary queries would crash when encountering rules that define values for error terms, unless those are somehow handled separately or unification is asymmetric. Unfolding may also have this problem.
Example: count += f(X), 1 for prime(X).
We also have to figure out the default value of error terms (see above).
Full discussion in Frozen terms.
Dynamic (non-const) types, and relation to intern table implementations.
Discussion moved to Dyna Type System
I think I really want the semantics of dynabase extension to be the same as the semantics of updates. This means that when you extend a dynabase, you don’t disturb randomness or cycles that are not transequents of your extension. Whether dynabases become new in an update is not answerable from within Dyna, I think, because the old dynabase can no longer be accessed; but it should be answerable from outside, e.g., d.e may be different before and after we update d.e.x += 1. This may be up to the implementation. (Certainly snapshots of those two are different.) But maybe two snapshots both before the update should be the same.
(All queries are against snapshots, so how do we actually get a live version of e? Maybe we can’t. Or maybe queries are not totally against snapshots after all – the snapshot is taken only to get the path to e but the thing that that path points to is live by default, so the recursive snapshotting doesn’t go all the way down. Anyway, if we do get two snapshots of e before and after, then they must be different in the sense that they get different results when we query them.)
See discussion of current implementation in When Things Go Wrong.
Some documentation of currently implemented declarations is in Pragmas.
the rule were f(:int _)., and we should get the same behavior if it were f(X) :- X=1., in other words, f(X) := X = :int Y.. It’s possible that types might get restricted in order to pass type checking, e.g., f(X) :- X=1, g(X). where g(X) restricts the type of X further because it only takes #0|#1.
Type checking: when we encounter a subgoal F is f(X,Y,Z), and only F and Z are first-use variables, then we determine the possible values of (Z,F) such that f(X,Y,Z) is well-formed for any value of (X,Y) allowed by the current type. This becomes the type of (Z,F), and we fail type-checking if it is empty. Actually we must get a joint type of (X,Y,Z,F). An explicit type restrictor :ty V restricts the type of V and again we fail type-checking if the result is empty. That is equivalent to saying that this copy of V by identity_ty(V) declared as
:ty identity_ty(:term V)
which takes any term and returns a copy of it if it’s in the type, otherwise returns null. That means that we really have
V’ is identity_ty(V)
as a subgoal and we use V’ instead of V. FURTHERMORE, we use V’ instead of V everywhere later in the rule.
If update or query modes are declared for a particular functor, they are assumed to be exhaustive. If they are not declared, then we automatically declare ground update modes (available to the user), at least if writeable, and infer as many query modes as we can manage to support. Note the ground updates may feed through the graph to produce non-ground updates, so we must be able to plan those even if they’re not public, and we must advertise them for other dynabases that are customers of ours. Also, if we write rules that refer to other dynabases that emit non-ground updates, we must be able to accept those updates, which may cause us to emit non-ground updates. The reason we only allow ground updates by default is that those are enough in practice and if we have more ground updates then (we think) we may have to have fewer queries, i.e., there is not a unique way to infer declarations that are as generous as possible.
There is currently some documentation in Builtins.