ordofp_core 0.1.0

OrdoFP core provides developers with HList, Disiunctio, NominataUniversalis, Universalis, and functional type classes
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117

//! Quantitative Types Module - Type-level multiplicity tracking
//!
//! > *"Quot usus, tot modi"*
//! > — As many uses, so many modes. (Neo-Latin)
//!
//! This module provides quantitative type abstractions inspired by Idris 2's
//! Quantitative Type Theory (QTT). QTT extends linear types with explicit
//! multiplicity annotations that track how many times a value is used.
//!
//! # Overview
//!
//! Quantitative Type Theory distinguishes three multiplicities:
//!
//! | Multiplicity | Name | Meaning |
//! |--------------|------|---------|
//! | 0 | Zero/Erased | Compile-time only, erased at runtime |
//! | 1 | One/Linear | Used exactly once |
//! | ω | Omega/Unrestricted | Used any number of times |
//!
//! # Scholastic Naming
//!
//! | English | Latin | Etymology |
//! |---------|-------|-----------:|
//! | Multiplicity | Multiplicitas | *multiplicitas* = manifoldness |
//! | Zero | Nihil | *nihil* = nothing |
//! | One | Semel | *semel* = once |
//! | Omega | Omega | ω = unlimited |
//! | Linear | Linearis | *linearis* = of a line |
//! | Erased | Erasum | *erasum* = wiped out |
//! | Handle | Manus | *manus* = hand |
//! | Pair | Par | *par* = equal, pair |
//! | Function | Functio | *functio* = performance |
//! | Monad | Monas | *monas* = unit |
//!
//! # Type-Level Multiplicities
//!
//! This module encodes multiplicities at the type level using phantom types,
//! enabling compile-time verification of usage patterns.
//!
//! ```rust
//! use ordofp_core::quantitative::{Multiplicitas, Qtt, Semel, Omega};
//!
//! // A linear value (used exactly once)
//! let linear: Qtt<i32, Semel> = Qtt::new(42);
//! assert_eq!(linear.multiplicity(), Multiplicitas::Semel);
//!
//! // An unrestricted value (can be cloned)
//! let unrestricted: Qtt<i32, Omega> = Qtt::new(42);
//! assert_eq!(unrestricted.multiplicity(), Multiplicitas::Omega);
//! ```
//!
//! # Reference
//!
//! - [Idris 2: Quantitative Type Theory in Practice](https://arxiv.org/abs/2104.00480)
//! - [The Syntax and Semantics of Quantitative Type Theory](https://bentnib.org/quantitative-type-theory.pdf)

extern crate alloc;

mod functio;
mod manus;
mod monas;
mod multiplicitas;
mod par;
mod qtt;

pub use functio::{
    FunctioLinearis, FunctioSemel, linear_apply, linear_compose, linear_const, linear_curry,
    linear_flip, linear_uncurry,
};
pub use manus::{ManusGuard, ManusLinearis};
pub use monas::{
    MonasLinearis, QttMonad, bind_qtt, join_qtt, kleisli_qtt, lift2_qtt, map2_qtt, map3_qtt,
    purus_qtt, sequence_qtt, traverse_qtt,
};
pub use multiplicitas::{
    Multiplicitas, MultiplicitasSemiring, Nihil, Omega, Semel, Usage, is_subusage, mult_add,
    mult_mul,
};
pub use par::{AdditiveChoice, ParLinearis, TensorLinearis, WithLinearis};
pub use qtt::{Qtt, QttErasum, QttExt, QttLiber, QttLinearis};

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_multiplicitas_variants() {
        let zero = Multiplicitas::Nihil;
        let one = Multiplicitas::Semel;
        let omega = Multiplicitas::Omega;

        assert!(zero.is_nihil());
        assert!(one.is_semel());
        assert!(omega.is_omega());
    }

    #[test]
    fn test_multiplicitas_semiring() {
        // 0 * x = 0
        assert_eq!(
            mult_mul(Multiplicitas::Nihil, Multiplicitas::Omega),
            Multiplicitas::Nihil
        );

        // 1 * x = x
        assert_eq!(
            mult_mul(Multiplicitas::Semel, Multiplicitas::Omega),
            Multiplicitas::Omega
        );

        // ω + ω = ω
        assert_eq!(
            mult_add(Multiplicitas::Omega, Multiplicitas::Omega),
            Multiplicitas::Omega
        );
    }
}