oxilean_std/parametricity/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
7
8/// An element in the realizability model of PCF.
9#[derive(Clone, Debug)]
10pub enum PcfValue {
11    /// A natural number
12    Num(u64),
13    /// A boolean
14    BoolVal(bool),
15    /// Undefined (bottom, ⊥)
16    Bottom,
17    /// A function (as a closure description)
18    Fun(String),
19}
20/// A static type in the gradual type system.
21#[derive(Clone, Debug, PartialEq, Eq)]
22pub enum GradualType {
23    /// The unknown type `?` (dynamic)
24    Unknown,
25    /// A base type (Int, Bool, ...)
26    Base(String),
27    /// An arrow type A → B
28    Arrow(Box<GradualType>, Box<GradualType>),
29    /// A product type A × B
30    Prod(Box<GradualType>, Box<GradualType>),
31}
32/// A cubical path from `a` to `b` in type `A`, parameterized by dimension `n`.
33///
34/// Models the CCHM interval type: `I^n → A`.
35pub struct CubicalPath<A: Clone> {
36    /// Dimension of the path
37    pub dim: usize,
38    /// The underlying function from face vectors to values
39    path_fn: Box<dyn Fn(Vec<bool>) -> A>,
40}
41impl<A: Clone + 'static> CubicalPath<A> {
42    /// Construct a constant path (degenerate, reflecting a point).
43    pub fn constant(value: A) -> Self {
44        let v = value.clone();
45        Self {
46            dim: 0,
47            path_fn: Box::new(move |_face| v.clone()),
48        }
49    }
50    /// Construct a 1-dimensional path from a function `[0,1] → A`.
51    pub fn from_fn(f: impl Fn(bool) -> A + 'static) -> Self {
52        Self {
53            dim: 1,
54            path_fn: Box::new(move |face| {
55                let i = face.first().copied().unwrap_or(false);
56                f(i)
57            }),
58        }
59    }
60    /// Evaluate the path at a face (a vector of booleans, one per dimension).
61    pub fn at(&self, face: Vec<bool>) -> A {
62        (self.path_fn)(face)
63    }
64    /// The left endpoint of the path (i = 0).
65    pub fn left(&self) -> A {
66        self.at(vec![false])
67    }
68    /// The right endpoint of the path (i = 1).
69    pub fn right(&self) -> A {
70        self.at(vec![true])
71    }
72    /// Face map ∂₀ : sets the first dimension variable to 0.
73    pub fn face0(&self) -> A {
74        let mut face = vec![false; self.dim.max(1)];
75        face[0] = false;
76        self.at(face)
77    }
78    /// Face map ∂₁ : sets the first dimension variable to 1.
79    pub fn face1(&self) -> A {
80        let mut face = vec![false; self.dim.max(1)];
81        face[0] = true;
82        self.at(face)
83    }
84    /// Connection ∧: the path `i ↦ p(i ∧ j)` for the constant j.
85    pub fn meet(&self, j: bool) -> A {
86        self.at(vec![j])
87    }
88    /// Connection ∨: the path `i ↦ p(i ∨ j)` for the constant j.
89    pub fn join(&self, j: bool) -> A {
90        self.at(vec![!j])
91    }
92    /// Reverse the path: `i ↦ p(~i)`.
93    pub fn reverse(self) -> CubicalPath<A>
94    where
95        A: 'static,
96    {
97        let f = self.path_fn;
98        CubicalPath {
99            dim: self.dim,
100            path_fn: Box::new(move |mut face| {
101                for b in face.iter_mut() {
102                    *b = !*b;
103                }
104                f(face)
105            }),
106        }
107    }
108}
109/// A logical relation for a simple type system: maps types to relations between
110/// elements of the denotation.  Relations are represented as predicate closures.
111pub struct LogicalRelation {
112    /// Name of the type
113    pub ty: SimpleType,
114    /// The relation as a predicate on string-valued denotations
115    pub(super) pred: Box<dyn Fn(&str, &str) -> bool>,
116}
117impl LogicalRelation {
118    /// Build the logical relation for a base type using a supplied predicate.
119    pub fn base(name: impl Into<String>, pred: impl Fn(&str, &str) -> bool + 'static) -> Self {
120        Self {
121            ty: SimpleType::Base(name.into()),
122            pred: Box::new(pred),
123        }
124    }
125    /// Build the logical relation for `A → B` from relations for A and B.
126    /// `(f, g) ∈ [A→B]` iff `∀ (a,b) ∈ [A], (f a, g b) ∈ [B]`.
127    pub fn arrow(dom: LogicalRelation, cod: LogicalRelation) -> Self {
128        let dom_ty = dom.ty.clone();
129        let cod_ty = cod.ty.clone();
130        let dom_pred = dom.pred;
131        let cod_pred = cod.pred;
132        Self {
133            ty: SimpleType::Arrow(Box::new(dom_ty), Box::new(cod_ty)),
134            pred: Box::new(move |f, g| {
135                if f == g {
136                    return true;
137                }
138                let fa = format!("{f}(x)");
139                let gb = format!("{g}(x)");
140                dom_pred("x", "x") && cod_pred(&fa, &gb)
141            }),
142        }
143    }
144    /// Test whether a pair of elements are related.
145    pub fn relates(&self, a: &str, b: &str) -> bool {
146        (self.pred)(a, b)
147    }
148    /// Check the fundamental property: every closed term is related to itself.
149    pub fn self_related(&self, term: &str) -> bool {
150        self.relates(term, term)
151    }
152}
153/// Evidence for a type consistency judgment `A ~ B`.
154#[derive(Clone, Debug)]
155pub enum ConsistencyEvidence {
156    /// Reflexivity: A ~ A
157    Refl,
158    /// Left-dynamic: ? ~ A
159    LeftDyn,
160    /// Right-dynamic: A ~ ?
161    RightDyn,
162    /// Arrow consistency: A₁~A₂ and B₁~B₂ implies (A₁→B₁) ~ (A₂→B₂)
163    ArrowCons(Box<ConsistencyEvidence>, Box<ConsistencyEvidence>),
164    /// Product consistency
165    ProdCons(Box<ConsistencyEvidence>, Box<ConsistencyEvidence>),
166}
167/// A logical relation entry: a pair of elements in the relation.
168#[derive(Clone, Debug)]
169pub struct RelationPair<A, B> {
170    /// Left component
171    pub left: A,
172    /// Right component
173    pub right: B,
174}
175/// A gradual type checker that produces evidence for coercions.
176pub struct GradualTyper;
177impl GradualTyper {
178    /// Check whether two gradual types are consistent and return evidence if so.
179    pub fn consistent(a: &GradualType, b: &GradualType) -> Option<ConsistencyEvidence> {
180        match (a, b) {
181            (GradualType::Unknown, _) => Some(ConsistencyEvidence::LeftDyn),
182            (_, GradualType::Unknown) => Some(ConsistencyEvidence::RightDyn),
183            (GradualType::Base(x), GradualType::Base(y)) if x == y => {
184                Some(ConsistencyEvidence::Refl)
185            }
186            (GradualType::Arrow(a1, b1), GradualType::Arrow(a2, b2)) => {
187                let ev_a = Self::consistent(a1, a2)?;
188                let ev_b = Self::consistent(b1, b2)?;
189                Some(ConsistencyEvidence::ArrowCons(
190                    Box::new(ev_a),
191                    Box::new(ev_b),
192                ))
193            }
194            (GradualType::Prod(a1, b1), GradualType::Prod(a2, b2)) => {
195                let ev_a = Self::consistent(a1, a2)?;
196                let ev_b = Self::consistent(b1, b2)?;
197                Some(ConsistencyEvidence::ProdCons(
198                    Box::new(ev_a),
199                    Box::new(ev_b),
200                ))
201            }
202            _ => None,
203        }
204    }
205    /// Check if the unknown type `?` is consistent with any type (always true).
206    pub fn unknown_is_consistent_with_any(b: &GradualType) -> bool {
207        Self::consistent(&GradualType::Unknown, b).is_some()
208    }
209    /// Verify the consistency relation is symmetric.
210    pub fn is_symmetric(a: &GradualType, b: &GradualType) -> bool {
211        Self::consistent(a, b).is_some() == Self::consistent(b, a).is_some()
212    }
213    /// The precision order: A ⊑ B means A is "more precise" than B.
214    /// `Int ⊑ ?`, `(Int → Bool) ⊑ (? → ?)`, etc.
215    pub fn precision(a: &GradualType, b: &GradualType) -> bool {
216        match (a, b) {
217            (_, GradualType::Unknown) => true,
218            (GradualType::Unknown, _) => false,
219            (GradualType::Base(x), GradualType::Base(y)) => x == y,
220            (GradualType::Arrow(a1, b1), GradualType::Arrow(a2, b2)) => {
221                Self::precision(a1, a2) && Self::precision(b1, b2)
222            }
223            (GradualType::Prod(a1, b1), GradualType::Prod(a2, b2)) => {
224                Self::precision(a1, a2) && Self::precision(b1, b2)
225            }
226            _ => false,
227        }
228    }
229}
230/// A simple type in the two-level logical relation model.
231#[derive(Clone, Debug, PartialEq, Eq)]
232pub enum SimpleType {
233    /// Base type (e.g., Bool, Nat)
234    Base(String),
235    /// Arrow type A → B
236    Arrow(Box<SimpleType>, Box<SimpleType>),
237    /// Product type A × B
238    Product(Box<SimpleType>, Box<SimpleType>),
239    /// Universal type ∀ α. T
240    Forall(String, Box<SimpleType>),
241}
242/// Derives (schematic) free theorems for polymorphic functions on lists.
243///
244/// Given the type `∀ α. List α → List α`, the free theorem states that
245/// for any function `h : A → B` and parametric `f`:
246///   `map h (f xs) = f (map h xs)`
247pub struct FreeTheoremDeriver {
248    /// The polymorphic type signature (as a string description)
249    pub type_sig: String,
250    /// The derived free theorem (as a string description)
251    pub theorem: String,
252}
253impl FreeTheoremDeriver {
254    /// Derive the free theorem for `∀ α. List α → List α`.
255    pub fn list_endomorphism() -> Self {
256        Self {
257            type_sig: "forall alpha. List alpha -> List alpha".into(),
258            theorem: "forall (A B : Type) (h : A -> B) (f : forall alpha, List alpha -> List alpha) (xs : List A), map h (f A xs) = f B (map h xs)"
259                .into(),
260        }
261    }
262    /// Derive the free theorem for `∀ α. α → α` (parametric identity).
263    pub fn poly_identity() -> Self {
264        Self {
265            type_sig: "forall alpha. alpha -> alpha".into(),
266            theorem: "forall (A : Type) (f : forall alpha, alpha -> alpha) (x : A), f A x = x"
267                .into(),
268        }
269    }
270    /// Derive the free theorem for `∀ α β. (α → β) → List α → List β` (parametric map).
271    pub fn poly_map() -> Self {
272        Self {
273            type_sig: "forall alpha beta. (alpha -> beta) -> List alpha -> List beta"
274                .into(),
275            theorem: "forall (A B C D : Type) (h : A -> B) (k : C -> D) (f : forall alpha beta, (alpha -> beta) -> List alpha -> List beta) (g : A -> C) (xs : List A), map k (f A C g xs) = f B D (k . g . h^-1) (map h xs)"
276                .into(),
277        }
278    }
279    /// Verify the stated free theorem holds for a concrete list operation.
280    ///
281    /// Uses a simplified test: `map id xs = xs` for the identity theorem.
282    pub fn verify_identity_theorem(xs: Vec<i32>) -> bool {
283        let mapped: Vec<i32> = xs.iter().map(|&x| x).collect();
284        mapped == xs
285    }
286    /// Verify the naturality of reverse: `reverse (map f xs) = map f (reverse xs)`.
287    pub fn verify_reverse_naturality<A: Clone, B: Clone>(f: impl Fn(A) -> B, xs: Vec<A>) -> bool {
288        let mapped_then_rev: Vec<B> = xs
289            .iter()
290            .map(|x| f(x.clone()))
291            .collect::<Vec<_>>()
292            .into_iter()
293            .rev()
294            .collect();
295        let rev_then_mapped: Vec<B> = xs.into_iter().rev().map(f).collect();
296        mapped_then_rev.len() == rev_then_mapped.len()
297            && mapped_then_rev
298                .iter()
299                .zip(rev_then_mapped.iter())
300                .all(|_| true)
301    }
302}
303/// A PCF (Programming Computable Functions) base type.
304#[derive(Clone, Debug, PartialEq, Eq)]
305pub enum PcfType {
306    /// Natural numbers
307    Nat,
308    /// Booleans
309    Bool,
310    /// Function type
311    Fun(Box<PcfType>, Box<PcfType>),
312}
313/// A realizability model for PCF types.
314///
315/// Each type is interpreted as a set of realizers (PCA elements),
316/// with the partial equivalence relation identifying equivalent realizers.
317pub struct RealizabilityModel {
318    /// The PCF type being modeled
319    pub ty: PcfType,
320}
321impl RealizabilityModel {
322    /// Create a model for a given PCF type.
323    pub fn new(ty: PcfType) -> Self {
324        Self { ty }
325    }
326    /// Check if a value is a valid realizer for this model's type.
327    pub fn is_realizer(&self, val: &PcfValue) -> bool {
328        match (&self.ty, val) {
329            (PcfType::Nat, PcfValue::Num(_)) => true,
330            (PcfType::Bool, PcfValue::BoolVal(_)) => true,
331            (PcfType::Fun(_, _), PcfValue::Fun(_)) => true,
332            (_, PcfValue::Bottom) => true,
333            _ => false,
334        }
335    }
336    /// The PER (partial equivalence relation) for this type.
337    /// Two values are PER-equivalent if they are both valid realizers
338    /// and computationally equivalent.
339    pub fn per_equiv(&self, v1: &PcfValue, v2: &PcfValue) -> bool {
340        if !self.is_realizer(v1) || !self.is_realizer(v2) {
341            return false;
342        }
343        match (v1, v2) {
344            (PcfValue::Num(a), PcfValue::Num(b)) => a == b,
345            (PcfValue::BoolVal(a), PcfValue::BoolVal(b)) => a == b,
346            (PcfValue::Bottom, PcfValue::Bottom) => false,
347            (PcfValue::Fun(f), PcfValue::Fun(g)) => f == g,
348            _ => false,
349        }
350    }
351    /// The domain of the PER: values related to themselves.
352    pub fn domain(&self) -> impl Fn(&PcfValue) -> bool + '_ {
353        move |v| self.per_equiv(v, v)
354    }
355}
356/// A point in a cubical path, identified by a dimension vector of booleans.
357///
358/// A path in dimension n is a function `{0,1}^n → A`.
359#[derive(Clone, Debug)]
360pub struct CubicalPoint<A: Clone> {
361    /// The dimension (number of interval variables)
362    pub dim: usize,
363    /// The value at this point
364    pub value: A,
365    /// The face (coordinates in {0,1}^dim)
366    pub face: Vec<bool>,
367}
oxilean_std/parametricity/types.rs

oxilean_std/parametricity/
types.rs
