 Dependently typed languages

Dependently typed languages are a category of programming languages that integrate a type system where types can depend on values. This means that types can be parameters that depend on specific values in the program, allowing for more expressive types that can capture more program properties within the type system itself. ### Key Features of Dependently Typed Languages: 1. **Types as First-Class Citizens**: In dependently typed languages, types can be treated as first-class entities.