This library defines the 'pluggable' parts of a grabapl implementation.

These are all contained in the [Semantics] trait, which this library implements for the [TheSemantics] holder type.

For the non-pluggable parts of a grabapl implementation, see the grabapl crate and documentation.

Type Systems

The example semantics we're defining here is made up of a node and edge type system as follows:

Node Type System

We have the following node values (also known as concrete node values) - see [NodeValue]:

• i32 - representing integers (1, 2, -3, etc.)
• String - representing strings ("hello", "world", "", etc.)

We have the following node types (also known as abstract node values) - see [NodeType]:

• Integer - representing nodes that hold integer values
• String - representing nodes that hold string values
• Any - a wildcard type that matches any node type, i.e., it represents nodes that can hold both integer and string values

See [NodeConcreteToAbstract] for the implementation of getting the most precise node type of a node value.

The type system on those types is induced by the following partially ordered set, visualized as a Hasse diagram:

          Any
         /   \
        /     \
    Integer  String

In other words, Integer and String are subtypes of Any, Any is a supertype of both, and a String is not a subtype of Integer and vice versa. See [NodeSubtyping] for the implementation of this type system.

Edge Type System

We have the following edge values (also known as concrete edge values) - see [EdgeValue]:

• () (the unit type) - representing no interesting value besides presence (i.e., just the singleton value () of the unit type)
• String - representing strings ("next", "parent", etc.)
• i32 - representing integers (1, 2, -3, etc.)

We have the following edge types (also known as abstract edge values) - see [EdgeType]:

• (), the unit type - representing edges that do not carry any additional value besides presence
• ExactString(s) - representing edges that carry the specific string value s, e.g., ExactString("next") represents exactly those edges with a string value of "next".
• String - representing edges that carry a string value
• Integer - representing edges that carry an integer value
• Any - a wildcard type that matches any edge type, i.e., it represents edges that can carry (), string, and integer values)

See [EdgeConcreteToAbstract] for the implementation of getting the most precise edge type of an edge value.

The type system on those types is induced by the following partially ordered set, visualized as a Hasse diagram:

              ____Any____
             /     |     \
            /      |      \
          ()   String      Integer
               / ... \
ExactString("a") ...  ExactString("zzzz...")

In other words, all types are subtypes of Any, ExactString(s) is a subtype of String for any string s, and String and Integer and () are not subtypes of each other. and there are no other relationships between the types. See [EdgeSubtyping] for the implementation of this type system. The notion of storing a concrete string value inside a type is closely related to (but much weaker than) refinement types.

Operations and Queries

Additionally, every [Semantics] implementation can define its own set of "builtin" operations and queries. These are arbitrary Rust functions (or any other language through FFI and/or interpreters) that operate on the graph.

Builtin Operations

Builtin operations are defined by the [BuiltinOperation] trait, which we have implemented for the [TheOperation] enum.

Builtin operations can be used to manipulate the graph, e.g., adding nodes or edges, removing them, changing their values, etc., but also for anything side-effectful, like printing a trace to the console.

There is a set of generic operations that are defined in the [LibBuiltinOperation] enum, which can be used to perform common operations on the graph independent of the custom semantics.

See the [BuiltinOperation] trait for more details on how to implement operations.

Builtin Queries

Queries are defined by the [BuiltinQuery] trait, which we have implemented for the [TheQuery] enum.

Queries can be used to retrieve information from the graph that is used to decide which branch of two to take. Essentially, these are the if conditions of traditional programming languages. Notably, queries do not return a first-class node value, but rather a value only visible in how the control flow of the program proceeds.

See the [BuiltinQuery] trait for more details on how to implement queries.

For queries that are supposed to change the statically known abstract graph, see [TODO: link to GraphShapeQuery

Optional Features

See the syntax module if you want to use this semantics in concjuction with grabapl's pluggable syntax parser and interpreter.

Usage

Once the semantics is defined, it can be used to build user defined operations and run operations on concrete graphs.

Continue in template/README.md for the next steps.

Your Turn

Feel free to copy this crate and adjust the semantics to your liking!