Expand description
§Path-Iter
A cocategory enumeration library based on path semantics
Implementation based on paper Cocategory Enumeration.
For an introduction to Path Semantics, see this paper.
§Sub-types in Path Semantics
In normal Path Semantics, one uses normal paths in theorem proving. Normal paths is a derivation from functions with sub-types.
This library focuses on sub-types, not on the more general case of normal paths.
A sub-type in Path Semantics is written in this form:
x : [f] a
Where x
is some input, f
is a function and a
is the output of f
.
This library is for enumerating such sub-types efficiently.
§Example: AND
The path!
macro is used to write in the standard notation of Path Semantics.
It constructs a type using Path
that implements IntoIterator
:
use path_iter::*;
fn main() {
for a in path!([And] true) {
// Prints `(true, true)`
println!("{:?}", a);
}
}
It prints (true, true)
because that is the only input value to And
which produces true
as output.
§Example: AND 2
You can decide the output value at runtime:
use path_iter::*;
fn main() {
for &b in &[false, true] {
for a in path!([And] b) {
println!("{:?}", a);
}
println!("");
}
}
This prints:
(false, false)
(false, true)
(true, false)
(true, true)
§Example: AND-NOT
You can chain path sub-types together:
use path_iter::*;
fn main() {
for a in path!([And] [Not] true) {
println!("{:?}", a);
}
}
§Example: Partial Application
Partial application is a technique where a function reduces to another function when calling it with fewer arguments than the signature.
For example, And(true)
reduces to Idb
.
use path_iter::*;
fn main() {
for a in path!([And(true)] true) {
println!("{:?}", a);
}
}
This should not be confused with function currying, which is extensionally equal to partial application, but captures the underlying function in a closure.
The path!
macro expands to partial application automatically, but it is very limited.
Outside the macro path!
or for complex cases, one must use PApp::papp
.
§Example: AND 3
The standard notation for composing paths is not very friendly with Rust macros.
Therefore, one can use a single bracket []
with functions separated by commas:
use path_iter::*;
fn main() {
for a in path!([((And, And), (And, And)), (And, And), And] true) {
println!("{:?}", a);
}
}
Macros§
Structs§
- Add
- Addition.
- AddRange
Iter - Iterates over numbers that adds up to some range.
- And
- Logical AND.
- Eqb
- Logical EQ.
- False1
- A boolean unary function that returns
false
. - Fstb
- Returns the first argument of a boolean binary function.
- Id
- Identity function.
- Idb
- Returns the argument of a boolean unary function.
- Imply
- Logical IMPLY.
- Neg
- Negation.
- Not
- Logical NOT.
- Or
- Logical OR.
- Path
- Stores a path sub-type with either
[T] U
(left) or[T] [V] ...
(right). - Path
Iter - Iterates over a path composition, e.g.
[f] [g] a
. - Product
Iter - Iterates over a product of two iterator generators.
- Sndb
- Returns the second argument of a boolean binary function.
- Square
- Square.
- Square
Range Iter - Iterates over numbers that squares up to some range.
- True1
- A boolean unary function that returns
true
. - Xor
- Logical XOR.
Enums§
- Either
- Used to lift iterator generators into a sum type.
- Either
Iter - Iterates over two the sum type of two iterators.
- Empty
- A type that is impossible to construct.
Traits§
- Higher
Into Iterator - Implemented by iterator generators.
- PApp
- Implemented for partial application.
Functions§
- item
- Constructs an item.
- path
- Construct a path composition.
- pullback
- Gets the pullback of two maps
f
andg
.