py4sci

Table Of Contents

Previous topic

Builtins

Next topic

Dyna Glossary

This Page

Specification of the Dyna Language

Introduction

What is Dyna?

Intended users

Key features

Relation to other work

How to read this specification

Organization

Notation

User comments

Coloring and formatting conventions

Cross-refs

Notifications

Glossary/Index

Terms (i.e., ground terms)

Overview

Primitive terms

Booleans

Numbers

Strings

Escape codes

Blobs

Compound terms

Functors

Single quotes

Positional arguments

Operator syntax

Keyword arguments

List syntax

Reserved functors

$ convention
$error

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);
  • if f(1) has an error value than f(X) will also return an error value.

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:

  • We define assert(:bool B) be true if B is true and $error otherwise. (Perhaps including if the argument is null, in which case the argument actually has to be unevaluated as with ?B. If not, the user can still write assert(?B) to have this meaning.)
  • Built-ins may have error values. For example, $error is the value of 1/0.
  • User programs may define some items to have an $error value. E.g., perhaps prime takes integer arguments but we say that prime(N) = $error for N < 2.
  • Items can be defined extensionally to have $error values.
  • If a type has a side condition that must be checked at runtime, then failing that side condition at runtime generates an error. For example, we might declare a range type of integers that are >= 2 and we use that as the type of the argument to prime. If the compiler cannot prove at compile time that the argument to prime satisfies the >= 2 test, then it inserts a runtime assertion, replacing prime(N) with assert(N >= 2), prime(N).
  • Integrity constraints.

How errors are consumed:

  • By default, any item whose name is an $error or contains an $error has value $error. In other words, if no value can be proved for such an item, its value is taken to be $error rather than null. If a value of $null can be proved for such an item, then evaluation of the item does return null. (Maybe better: if the item unifies with the head of any rule or can be set extensionally, then we skip the default behavior and just go with the rule(s) that define the value, possibly null. Note that this means that we can’t just clear out dead code – rules that always fail – because they might ensure that error terms have null values.)
  • However, this is overridden by some built-ins. For example, true | $error evalues to true and 0 * $error evaluates to 0.
  • Similarly, a user program can trap errors. For example, times(0,$error) := 0. Also, f(:int X) = 0 presumably means that f($error) yields 0.

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).

$null

Sets

Dynabases

Full discussion in Dynabases.

Gensyms

Frozen terms

Full discussion in Frozen terms.

Patterns (i.e., non-ground terms)

Variables

Variable names

Underscores

Non-ground terms

Types

Dynamic (non-const) types, and relation to intern table implementations.

Type coercion

Discussion moved to Dyna Type System

Unification

Frozen terms

Dynabases

Overview

Items

Null items

Syntax for items

Brackets vs. parentheses

Quoting items with &

Evaluating terms with *

Assertions

Queries

Simple queries

Complex queries

Expressions

Aggregating queries

Accessors

Query modes

Some discussion of current approach is in Pragmas.

Lambdas

Terms as dynabases

Updates

Update modes

Stability

Dynabase types

Extensions

Const declaration

Snapshots

Inspecting and modifying dynabases

Abstract API

Command line interface

Graphical interface

Programming interface

Dyna programs

Overview

File format

Rules

Definition

Aggregation

Guards

Fixpoint semantics

Errors
Cycles
Stability
to nwf:

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.

Gensyms

Head destructuring

Dynabase literals

Syntax

Ownership

Semantics

Declarations

Some documentation of currently implemented declarations is in Pragmas.

Type declarations

Evaluation declarations

There is currently some documentation in Syntax.

Default arguments

Visibility declarations

Const

Import

Syntax declarations

Declaring new aggregators

Declaration inference [elaboration]

If we have a rule f(1). then we act as if
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.

Type inference [elaboration] on variables

Type inference [elaboration] on functors

Aggregator declaration inference [elaboration]

Scripting commands

Include

Foreign function interface

Concrete syntax

Overview

Standard syntactic sugar

Default syntax table

Changing the syntax table

Printing

Readable printing

Prettyprinting

Standard library

There is currently some documentation in Builtins.

Generic operators and aggregators

Boolean operators and aggregators

Numeric operators and aggregators

Randomness

String operators and aggregators

Array operators and aggregators

Set operators and aggregators

Graph operators and aggregators

Other standard encodings

Analyzing program execution

$rule

$gradient

Voodoo items

Reflection

Controlling program execution

Storage classes

Priorities

Query costs and plans

Features for learning

Foreign dynabases

Files

Processes

Sockets

Servers

Appendices