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::strict::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 using the `new_operation` method.
49//!     // This creates nodes for each type in the input and output, and returns their `NodeId`s.
50//!     let (_, (_, x)) = state.new_operation(Op::Copy, vec![A], vec![A, A]) else {
51//!         // OpenHypergraph::new_operation will always turn as many sources/targets as appear in
52//!         // the provided source/target types, respectively.
53//!         panic!("impossible!");
54//!     };
55//!
56//!     // create a `Mul : 2 → 1` operation
57//!     let (_, (y, _)) = state.new_operation(Op::Mul, vec![A, A], vec![A]) else {
58//!         panic!("impossible!");
59//!     };
60//!
61//!     // Connect the copy operation to the multiply operation
62//!     state.unify(x[0], y[0]);
63//!     state.unify(x[1], y[1]);
64//!
65//!     // return the OpenHypergraph that we built
66//!     state
67//! }
68//! ```
69//!
70//! The "lax" representation also allows for type checking and inference:
71//! when composing two operations as in the former diagram, we can have distinct types for
72//! connected nodes, e.g., x0 and y0. this allows both *checking* (of e.g. equality) and
73//! *inference*: inequal types might be *unified* into a single type.
74pub mod category;
75pub mod functor;
76pub mod hypergraph;
77pub mod mut_category;
78pub mod open_hypergraph;
79
80pub use crate::category::*;
81pub use hypergraph::*;
82pub use open_hypergraph::*;
83
84pub mod var;
open_hypergraphs/lax/mod.rs

open_hypergraphs/lax/
mod.rs
