Re:Idris: A Language for Type-Driven Development
by still_grokking on Tuesday January 24, 2023 @03:22AM
(#34500951)
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.
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.