Module dependent 

Dependent type system for value-dependent types in TensorLogic.

This module implements dependent types, where types can depend on runtime values. This is crucial for tensor operations where dimensions are first-class values.

Examples

use tensorlogic_ir::dependent::{DependentType, IndexExpr, DimConstraint};

// Vector of length n: Vec<n, T>
let n = IndexExpr::var("n");
let vec_n_int = DependentType::vector(n.clone(), "Int");

// Matrix with dimensions m×n: Matrix<m, n, T>
let m = IndexExpr::var("m");
let matrix_type = DependentType::matrix(m.clone(), n.clone(), "Float");

// Bounded vector: Vec<n, T> where n <= 100
let constraint = DimConstraint::lte(n.clone(), IndexExpr::constant(100));

Key Features

• Index expressions: Arithmetic on dimension variables
• Dependent function types: (x: T) -> U(x)
• Refinement types: Types with predicates on values
• Dimension constraints: Bounds and relationships between dimensions
• Type-level computation: Compute types from values

Structs

DependentTypeContext

Type checking context for dependent types.

Enums

DependentType

Dependent type: types that depend on runtime values.

DimConstraint

Dimension constraints for dependent types.

IndexExpr

Index expression for dimension calculations.