Dependent Type

Definitions

1. A type that depends on a value — for example, Vector<n> where n is the length, allowing the compiler to verify that you never access an out-of-bounds index. Enables proving program correctness at compile time. Found in Idris, Agda, and Lean. TypeScript and Rust approximate some dependent typing features.

   In plain English: A type that includes a specific value (like a list's exact length), letting the compiler catch more errors.

   Example: "With dependent types, concat(Vector<3>, Vector<4>) returns Vector<7> — the compiler tracks the exact length."

Related Terms

• Algebraic Data Type
• Class
• Derived Type
• Discriminant
• Horn Clause
• Testing
• Algebraic Data Type
• Covariance
• Nominal Typing
• Effect System