4 ms·
Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns
by huntie 8y ago
Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1.
Edwin Brady shows off some examples in Idris here[1]. I thought the matrix example was really impressive.
[1] https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU
- joe_the_user 8y agoWhen I see this definition, I scratch my head and wonder why this isn't a different way to introduce object orientation, generics, c++ parameterized templates and such.
- RossBencina 8y agoYes. C++ templates provide some subset of what you can do with dependent types in Idris.
- logicchains 8y agoThe key difference with C++ templates is that in C++ you can't have a type parameterised by a value that's only know at runtime, e.g. a std::array<N> where N is read from stdin. In a dependently typed language, you can. Object orientation is a different matter entirely; in the sense it implies Java-style class-based inheritance, it's almost in the opposite spirit to dependent types, as such late-binding (virtual methods) means it's possible to call methods such that the compiler has no idea which method will be called at compile time, making it hard to reason about the code at compile time.
- deleted 8y ago[deleted]
- deleted 8y ago[deleted]