Length-Indexed Lists

Encode the length of a list in the type — eliminate IndexError at verification time.

The Problem

Python's list is length-agnostic. Calling lst[0] on an empty list raises IndexError at runtime. With dependent types, we can track the length in the type itself, making out-of-bounds access a type error caught before the code runs.

Defining Vec[T, N]

from __future__ import annotations
from dataclasses import dataclass
from typing import TypeVar, Generic
from deppy import guarantee, check, assume
from deppy.types import Nat, NatLiteral

T = TypeVar('T')
N = TypeVar('N', bound=Nat)
M = TypeVar('M', bound=Nat)

@dataclass(frozen=True)
class Vec(Generic[T, N]):
    """A list whose length is tracked at the type level."""
    _items: tuple[T, ...]

    def __post_init__(self):
        check(len(self._items) == N,
              "runtime length must match type-level N")

    def __len__(self) -> int:
        return len(self._items)

Constructors: Nil and Cons

def nil() -> Vec[T, NatLiteral[0]]:
    """The empty vector."""
    return Vec(())

@guarantee("result has length N + 1")
def cons(x: T, xs: Vec[T, N]) -> Vec[T, N + 1]:
    """Prepend an element — length increases by 1."""
    return Vec((x,) + xs._items)
# Z3 proves: len((x,) + xs._items) == len(xs._items) + 1  ✅

Safe Head and Tail

The key insight: head and tail require N > 0 at the type level. Code that calls head(nil()) fails type-checking — no runtime exception possible.

@guarantee("returns the first element")
def head(v: Vec[T, N]) -> T:
    assume("N > 0")  # proof obligation for caller
    return v._items[0]

@guarantee("returns all but the first element")
def tail(v: Vec[T, N]) -> Vec[T, N - 1]:
    assume("N > 0")
    return Vec(v._items[1:])

# Usage:
v3: Vec[int, NatLiteral[3]] = Vec((10, 20, 30))
x  = head(v3)        # ✅ — Z3 proves 3 > 0
v2 = tail(v3)        # ✅ — v2 : Vec[int, 2]
# head(nil())         # ❌ — Z3 refutes 0 > 0

Z3_VERIFIED — IndexError impossible

Append with Length Addition

@guarantee("result length == len(a) + len(b)")
def append(
    a: Vec[T, N],
    b: Vec[T, M],
) -> Vec[T, N + M]:
    """Concatenate two vectors — lengths add."""
    return Vec(a._items + b._items)
# Z3 proves: len(a._items + b._items) == N + M  ✅

Zip Requires Equal Lengths

A = TypeVar('A')
B = TypeVar('B')

@guarantee("result has same length N, pairing elements")
def zip_vec(
    a: Vec[A, N],
    b: Vec[B, N],  # same N — enforced by the type
) -> Vec[tuple[A, B], N]:
    return Vec(tuple(zip(a._items, b._items)))

# Usage:
names: Vec[str, NatLiteral[3]] = Vec(("a", "b", "c"))
nums:  Vec[int, NatLiteral[3]] = Vec((1, 2, 3))
pairs = zip_vec(names, nums)   # ✅ both length 3

short: Vec[int, NatLiteral[2]] = Vec((1, 2))
# zip_vec(names, short)           # ❌ 3 ≠ 2 — type error

Map Preserves Length

@guarantee("result has the same length as input")
def map_vec(
    f: Callable[[A], B],
    v: Vec[A, N],
) -> Vec[B, N]:
    """Apply f to every element, preserving length."""
    return Vec(tuple(f(x) for x in v._items))
# Z3 proves: len(tuple(f(x) for x in items)) == len(items)  ✅

Comparison with F*

type vec (a:Type) : nat -> Type =
  | Nil  : vec a 0
  | Cons : a -> vec a n
          -> vec a (n+1)

let head (#a:Type)
         (#n:pos)
         (v:vec a n) : a =
  Cons?.hd v

@dataclass(frozen=True)
class Vec(Generic[T, N]):
    _items: tuple[T, ...]

def head(v: Vec[T, N]) -> T:
    assume("N > 0")
    return v._items[0]

F* encodes the length as an index on the inductive type. Deppy uses the same idea via a type parameter N : Nat, with Z3 verifying the arithmetic obligations.

Filter with Bounded Length

Not all operations preserve the exact length. filter produces a vector whose length is at most the original — we express this as a refinement on the return type.

from deppy.types import Refined

@guarantee("result length <= input length")
def filter_vec(
    pred: Callable[[T], bool],
    v: Vec[T, N],
) -> Refined[Vec[T, M], "M <= N"]:
    """Filter elements, result length bounded by N."""
    result = tuple(x for x in v._items if pred(x))
    check(len(result) <= len(v._items))
    return Vec(result)
# Z3 proves: len(filtered) <= len(original)  ✅

Concatenation Associativity

K = TypeVar('K', bound=Nat)

@guarantee("append is associative")
def append_assoc(
    a: Vec[T, N],
    b: Vec[T, M],
    c: Vec[T, K],
) -> PathType[
    Vec[T, N + M + K],
    "append(append(a, b), c)",
    "append(a, append(b, c))",
]:
    """append(append(a,b),c) == append(a, append(b,c))"""
    # Both sides produce the same tuple: a._items + b._items + c._items
    # Z3 + tuple theory discharges this as tuple concat is associative.
    return Refl(append(append(a, b), c))

Advanced: Reverse with Length Preservation

@guarantee("len(result) == len(v) and elements are reversed")
def reverse(v: Vec[T, N]) -> Vec[T, N]:
    return Vec(v._items[::-1])

# Deppy's tuple theory includes:
# ∀ t : tuple. len(t[::-1]) == len(t)
# This lemma lets Z3 discharge the length obligation.

Exercises