Crate path_iter

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§

path: Syntax sugar for a path sub-type.
path_type: Syntax sugar for the type of a path sub-type.

Structs§

Add: Addition.
AddRangeIter: 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).
PathIter: Iterates over a path composition, e.g. [f] [g] a.
ProductIter: Iterates over a product of two iterator generators.
Sndb: Returns the second argument of a boolean binary function.
Square: Square.
SquareRangeIter: 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.
EitherIter: Iterates over two the sum type of two iterators.
Empty: A type that is impossible to construct.

Traits§

HigherIntoIterator: 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 and g.

Type Aliases§

Item: Used to make end of path disambiguous from path composition.
PathComp: Represents a path composition.
PathEnd: Represents a terminal path [T] U.

Crate path_iterCopy item path