[tomkludy]

Every discussion or article I have read on dependent types assumes that the reader is a mathematician. I usually make it only a few paragraphs in before I am completely lost.

Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly. In exchange for that burden, there must be practical (not theoretical) benefits but they do not come through clearly. All of the examples I've seen are about "index of a list is guaranteed in bounds". That is such a minor and infrequent bug in practice that it does not justify the additional complexity. There must be more, that I'm just not seeing.

Is there a "Dependent types for non-mathematicians" article out there somewhere, where I can learn about patterns and practical applications?

[lmm]

> Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly.

I'd say that's backwards: rather a dependently typed language relaxes a huge restriction that most programming languages have, that only certain things can be used as types. Any program that's valid in language X is also valid in a dependently typed version of language X (e.g. most Haskell functions translate directly into Idris as long as they don't rely on laziness).

Dependent types make it easier to encode properties that you care about into the type system, i.e. rather than the programmer having to get them right, the compiler can check them for you. Far from burdening the programmer, it lightens your mental load.

> All of the examples I've seen are about "index of a list is guaranteed in bounds". That is such a minor and infrequent bug in practice that it does not justify the additional complexity.

Most code is in terms of domain-specific things, and so the types you use are also domain-specific. In my experience every code bug (as distinct from "behaving as specified but not as intended" bugs) boils down to "we thought x, but actually y" and can be avoided by making more precise use of a type system. If you have bugs that hit production, you can probably avoid them with better types. If you avoid production bugs by using tests, you can probably replace most of those tests with types and they'll become more concise and easier to maintain. But of course the specifics of what types to use will be specific to your domain; examples like list indices are common because they're one of those rare types that virtually everyone uses.

[b2gills]

Indexing into a List

    sub lookup ( List \xs, Int \index ){…}

Make sure the index is valid.

    sub lookup ( List \xs, Int \index where 0 ..^ xs.elems ){…}

The `where` clause gets attached to the `Int` typecheck.

---

I think it may also apply if you have other limitations that you need to check regularly, like making sure that strings fit into a database.

    sub foo ( Str \name where .chars ≤ 256 ){…}

Which Perl6 has the ability to give that a name as if it was a type so that it can be reused.

    subset DB-Str of Str where .chars ≤ 256;

    sub foo ( DB-Str \name ){…}

    my DB-Str $name = '';

    $name = 'a' x 10000;
    # Typecheck error

---

One use of this feature is to implement the UInt type (This is almost exactly how it is implemented in the Rakudo implementation of Perl6)

    subset UInt of Int where {$_ >= 0};

---

Then again I've never read any that talk about Perl6 as already having that feature; so maybe I'm mistaken.

I would guess that they are talking about something slightly different. (That often seems to be the case)

[anon_d]

Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly

It's basically the opposite of this.

If a language has dependent types, you can continue to use it in the same way as a language with does not have dependent types.

BUT, there's a lot of programming patterns that previously couldn't be implemented in a type-safe way, that now can be. This also gives a ton of opportunities for libraries to implement abstractions that weren't expressible before.

Dependent types are not that complicated, actually, and they don't add any burden to programs that don't use them.