open_hypergraphs/lax/
mod.rs

1//! An imperative/sequential interface for constructing "Lax" Open Hypergraphs.
2//!
3//! A lax open hypergraph is similar to an open hypergraph, but where the connecting of nodes
4//! is deferred until the [`OpenHypergraph::quotient`] operation is called.
5//!
6//! For example, a "strict" [`OpenHypergraph`] representing the composite of "copy" and "multiply"
7//! operations can be depicted as follows:
8//!
9//! ```text
10//!     ┌──────┐       ┌──────┐
11//!     │      ├───●───┤      │
12//! ●───┤ Copy │       │ Mul  ├───●
13//!     │      ├───●───┤      │
14//!     └──────┘       └──────┘
15//! ```
16//!
17//! A *lax* OpenHypergraph supports having distinct nodes for each operation, with a "quotient
18//! map" (depicted as a dotted line) recording which nodes are to be identified.
19//!
20//! ```text
21//!     ┌──────┐   x0    y0  ┌──────┐
22//! a   │      ├───●╌╌╌╌╌●───┤      │    b
23//! ●───┤ Copy │             │ Mul  ├───●
24//!     │      ├───●╌╌╌╌╌●───┤      │
25//!     └──────┘   x1    y1  └──────┘
26//! ```
27//!
28//! Calling [`OpenHypergraph::quotient`] on this datastructure recovers the strict
29//! [`crate::open_hypergraph::OpenHypergraph`] by identifying `x0` with `y0` and `x1` with `y1`.
30//!
31//! The lax [`OpenHypergraph`] can be constructed with the following Rust code.
32//!
33//! ```rust
34//! use open_hypergraphs::lax::OpenHypergraph;
35//!
36//! #[derive(PartialEq, Clone)]
37//! pub enum Obj { A }
38//!
39//! #[derive(PartialEq, Clone)]
40//! pub enum Op { Copy, Mul }
41//!
42//! fn copy_mul() -> OpenHypergraph<Obj, Op> {
43//!     use Obj::A;
44//!
45//!     // we use the stateful builder interface to add nodes and edges to the hypergraph
46//!     let mut state = OpenHypergraph::empty();
47//!
48//!     // create a `Copy : 1 → 2` operation
49//!     let (_, (_, x)) = state.new_operation(Op::Copy, vec![A], vec![A, A]) else {
50//!         // OpenHypergraph::new_operation will always turn as many sources/targets as appear in
51//!         // the provided source/target types, respectively.
52//!         panic!("impossible!");
53//!     };
54//!
55//!     // create a `Mul : 2 → 1` operation
56//!     let (_, (y, _)) = state.new_operation(Op::Mul, vec![A, A], vec![A]) else {
57//!         panic!("impossible!");
58//!     };
59//!
60//!     // Connect the copy operation to the multiply operation
61//!     state.unify(x[0], y[0]);
62//!     state.unify(x[1], y[1]);
63//!
64//!     // return the OpenHypergraph that we built
65//!     state
66//! }
67//! ```
68//!
69//! The "lax" representation also allows for type checking and inference:
70//! when composing two operations as in the former diagram, we can have distinct types for
71//! connected nodes, e.g., x0 and y0. this allows both *checking* (of e.g. equality) and
72//! *inference*: inequal types might be *unified* into a single type.
73pub mod hypergraph;
74pub mod open_hypergraph;
75
76pub use hypergraph::*;
77pub use open_hypergraph::*;
78
79pub mod var;
open_hypergraphs/lax/mod.rs

open_hypergraphs/lax/
mod.rs
