Type System and Composition

2.3 Type System and Composition

Spaxiom's expressiveness comes from a small set of composable primitives with a well-defined type system. Unlike ad-hoc sensor integration scripts, Spaxiom enforces type safety at DSL construction time and provides algebraic composition operators that enable complex spatiotemporal queries to be built from simple building blocks.

Core type hierarchy

The DSL defines the following fundamental types:

• Sensor: base abstraction for any physical or virtual sensor. Key methods:
  • read() → Value: synchronous read of current sensor state
  • position → (x, y, z): 3D location in space
  • zone → Zone: containing spatial region
  • units → Unit: physical units (e.g., meters, celsius, pascal)
• Condition: boolean-valued predicate over sensor state and time. Conditions are lazy: they are not evaluated until subscribed or explicitly triggered. Key properties:
  • holds() → bool: evaluate condition at current time
  • since_true → float: seconds since condition became true (or 0.0 if false)
  • since_false → float: seconds since condition became false (or 0.0 if true)
• Zone: 3D spatial region with geometric operations. Supports axis-aligned boxes, convex polygons, and union/intersection:
  • contains(x, y, z) → bool
  • overlaps(other_zone) → bool
  • distance_to(x, y, z) → float
  • volume → float
• Entity: tracked object with identity and attributes. Examples: a person, robot, forklift, or pallet. Entities have:
  • id → str: unique identifier
  • position → (x, y, z): current location (if trackable)
  • velocity → (vx, vy, vz): optional velocity vector
  • attributes → dict: arbitrary key-value metadata
• Quantity: numeric value with physical units. Enforces dimensional analysis:
  • value → float
  • unit → Unit
  • Supports arithmetic with automatic unit conversion and error on incompatible units

Condition composition operators

Conditions form a boolean algebra with standard operators:

from spaxiom import Condition

# Logical operators
c1 = Condition(lambda: temp.read() > 25.0)
c2 = Condition(lambda: humidity.read() > 60.0)

hot_and_humid = c1 & c2    # conjunction (AND)
hot_or_humid  = c1 | c2    # disjunction (OR)
not_hot       = ~c1        # negation (NOT)

# Temporal chaining
humid_then_hot = c2.before(c1, within_seconds=300)  # c2 before c1, within 5 min

Importantly, these operators are not evaluated eagerly. They construct a lazy evaluation graph that the runtime optimizes.

Temporal operators

Spaxiom provides temporal logic operators inspired by Linear Temporal Logic (LTL) but adapted for continuous real-time systems:

• within(duration, condition): condition holds continuously for at least duration seconds.

  sustained_motion = within(5.0, motion_detected)  # motion for ≥5s

• always(duration, condition): condition holds at all sampled times over the past duration seconds (similar to within but checks discrete samples).

  stable_temp = always(60.0, temp_in_range)  # stable for 1 minute

• eventually(duration, condition): condition becomes true at least once within the next duration seconds (forward-looking, requires buffering or prediction).

  # Predictive: will door open in next 10s?
  door_will_open = eventually(10.0, door_sensor_active)

• before(c1, c2, within_seconds=T): condition c1 occurs before c2 within time window T.

  alarm_then_evacuation = alarm_triggered.before(exit_door_opened, within_seconds=120)

• after(c1, c2, within_seconds=T): condition c1 occurs after c2 within time window T.

These operators enable expressive temporal patterns without manually managing timers or state machines.

Spatial operators

Spatial queries are first-class in Spaxiom. Common patterns:

• inside(entity, zone): returns a Condition that is true when entity is within zone.

  robot_in_hazard_zone = inside(robot_entity, hazard_zone)

• near(entity1, entity2, threshold): true when Euclidean distance < threshold.

  collision_risk = near(robot, human, threshold=2.0)  # within 2 meters

• overlaps(zone1, zone2): true if zones intersect.
• distance(entity, zone): returns Quantity in meters.

  dist_to_exit = distance(person, exit_zone)
  far_from_exit = Condition(lambda: dist_to_exit.value > 10.0)

Type checking and unit validation

Spaxiom performs compile-time validation where possible:

• Unit compatibility: operations on Quantity objects check dimensional compatibility. For example:

  from spaxiom.units import meters, seconds, kg
  
  distance = 10.0 * meters
  time = 5.0 * seconds
  velocity = distance / time  # OK: m/s
  
  mass = 70 * kg
  invalid = distance + mass   # TypeError: incompatible units (length + mass)

• Condition type safety: logical operators (&, |, ~) only accept Condition objects, preventing accidental confusion with Python's native boolean operators.
• Spatial type checking: Zone methods enforce 3D coordinate tuples or Entity objects with positions.

Runtime validation handles cases that cannot be checked statically:

• Sensor read failures (timeouts, disconnections) raise SensorException with configurable retry/fallback policies.
• Out-of-bounds spatial queries (e.g., entity position outside known coordinate system) trigger warnings or exceptions.
• Temporal operator timeouts (e.g., eventually failing to observe condition) can fire explicit callbacks.

Composition example: complex spatiotemporal query

Combining these primitives enables concise expression of complex behaviors. Example: detect a "loitering near exit" pattern.

from spaxiom import Sensor, Zone, Entity, Condition, within, inside, near
from spaxiom.units import meters

# Spatial setup
exit_zone = Zone(x=10, y=20, width=3, height=2)
exit_vicinity = exit_zone.buffer(5 * meters)  # 5m buffer around exit

# Entity tracking
person = Entity(id="person_42")

# Conditions
near_exit = inside(person, exit_vicinity)
not_exiting = ~inside(person, exit_zone)
stationary = Condition(lambda: person.velocity.magnitude() < 0.1)  # < 0.1 m/s

# Composite pattern: near exit, not moving, for 30+ seconds
loitering = within(30.0, near_exit & not_exiting & stationary)

@on(loitering)
def alert_security():
    print(f"Person {person.id} loitering near exit at {person.position}")

This single composite condition would require dozens of lines of manual state tracking, timers, and geometric computations in a traditional imperative approach.

Formal semantics and denotational interpretation

For verification purposes (see Section 7.3), we can give Spaxiom conditions a denotational semantics as functions from time to truth values:

Where ⟦c⟧(t) is the truth value of condition c at time t. Composition operators have natural interpretations:

• ⟦c₁ & c₂⟧(t) = ⟦c₁⟧(t) ∧ ⟦c₂⟧(t)
• ⟦c₁ | c₂⟧(t) = ⟦c₁⟧(t) ∨ ⟦c₂⟧(t)
• ⟦~c⟧(t) = ¬⟦c⟧(t)
• ⟦within(δ, c)⟧(t) = true iff ∀t' ∈ [t−δ, t], ⟦c⟧(t') = true

This formal interpretation enables model checking and equivalence proofs between Spaxiom programs and temporal logic formulas.

Performance characteristics of composition

Lazy evaluation and operator fusion are critical for performance:

• Lazy evaluation: Condition objects are not evaluated until subscribed via @on() or explicitly polled. This avoids wasted computation on conditions that are never used.
• Operator fusion: the runtime analyzes the condition graph and fuses compatible operators. For example, within(5.0, c1) & within(5.0, c2) shares a single 5-second time buffer rather than maintaining two separate buffers.
• Incremental evaluation: temporal operators like within use circular buffers and incremental updates, avoiding full re-evaluation on every sensor tick.
• Short-circuit evaluation: boolean operators (&, |) short-circuit when possible, skipping expensive sensor reads if the result is already determined.

These optimizations make Spaxiom practical even on resource-constrained edge devices with hundreds of sensors and conditions.