View Source cure_dependent_types (cure v0.7.0)
Dependent Type Checking with SMT
This module implements type checking for dependent types, extending the base type checker with support for:
- Value parameters in types (e.g., n: Nat in Vector(T, n))
- Type-level expressions (arithmetic, comparisons)
- Constraint generation and verification
- SMT-based proof of type correctness
Architecture
Type Environment
The type environment is extended to track:
- Type variables (T, U, etc.)
- Value parameters (n: Nat, m: Int, etc.)
- Accumulated constraints
- SMT environment for verification
Verification Conditions
When checking a dependent type, we generate verification conditions (VCs):
- Well-formedness: Value parameters satisfy their constraints
- Subtyping: Type-level expressions respect subtyping relations
- Arithmetic: Type-level arithmetic is sound
Example
def concat<T, m: Nat, n: Nat>(
v1: Vector(T, m),
v2: Vector(T, n)
): Vector(T, m + n) = v1 ++ v2
% Verification conditions:
% 1. length(v1) == m (from v1's type)
% 2. length(v2) == n (from v2's type)
% 3. length(v1 ++ v2) == m + n (return type requirement)
% 4. Prove: length(v1 ++ v2) == length(v1) + length(v2) via SMTUsage
% Check if type is well-formed
{ok, Env2} = cure_dependent_types:check_type(Type, Env),
% Generate verification conditions
VCs = cure_dependent_types:generate_vcs(Expr, Type, Env),
% Verify via SMT
{ok, _} = cure_dependent_types:verify_vcs(VCs, Env).