Dependent Types
← Back to Advanced Type Features
Types that depend on values, allowing the type system to express invariants that are impossible in simpler type systems. For example, a vector type parameterized by its length ensures at compile time that indexing is always within bounds.
Key Properties
Related
- Languages: Idris, Agda