Types That Depend on Values
← Back to Dependent Types
Types parameterized by runtime values, not just other types. For example, Vector n Int is a vector of exactly n integers, where n is a value. This allows encoding invariants like array bounds, protocol states, and resource linearity directly in the type system.