3 ms·

The examples are completely out of context. > Relationships to be expressed between values; for example, that two lists have the same length. This can be also

The examples are completely out of context. > Relationships to be expressed between values; for example, that two lists have the same length. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. You don't need types for that at all… > Assumptions to be made explicit and checked by the compiler. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. In theory you don't need types for that at all. (Even types would be the current std. method to achieve that). > For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run. You can construct a NEL (NonEmptyList) in any language. That's trivial. You just need to enforce the usage of the right factory method for your list. > If desired, properties of program behaviour to be formally stated and proven. This has nothing to do with dependent types (directly). A language based on simply typed lambda calculus is "enough" to arrive at this property.

dmytrish 4y ago
Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus? It's just that dependent types enable you to express any invariants statically, without actually running the code. > You can construct a NEL (NonEmptyList) in any language. That's trivial. That's true, with the caveat of: this invariant only exists in your head and hopefully docs. When it's encoded in a type, your compiler gets awareness of this invariant as well. Then it's able to do things that were impossible before, it can catch bugs that you would not (e.g. due the sheer amount of source code). Even though there are other approaches to software verification, types are the only one that got mainstream adoption so far.
- still_grokking 4y ago
  Of course. But the examples given missed the point imho. All of the stated things don't need any type level machinery. You can just test things at runtime and be good. If you want to prove things at compile time that's a very different story. But than this needs to be explicitly stated in the examples.

dmytrish 4y ago

Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus? It's just that dependent types enable you to express any invariants statically, without actually running the code. > You can construct a NEL (NonEmptyList) in any language. That's trivial. That's true, with the caveat of: this invariant only exists in your head and hopefully docs. When it's encoded in a type, your compiler gets awareness of this invariant as well. Then it's able to do things that were impossible before, it can catch bugs that you would not (e.g. due the sheer amount of source code). Even though there are other approaches to software verification, types are the only one that got mainstream adoption so far.

still_grokking 4y ago
Of course. But the examples given missed the point imho. All of the stated things don't need any type level machinery. You can just test things at runtime and be good. If you want to prove things at compile time that's a very different story. But than this needs to be explicitly stated in the examples.