[chriswarbo]

> The more abstract parts like dependent types are really complicated and even unintuitive to use.

I disagree with this: dependent types are way easier than lots of the convoluted schemes that non-dependent languages have come up with.

As a simple example, dependently-typed languages don't need parametric polymorphism or generics: we can achieve the same thing by passing types as arguments; e.g.

    map: (inType: Type) -> (outType: Type) -> (f: inType -> outType) -> (l: List inType) -> List outType
    map inType outType f l = match l with
      Nil  inType      -> Nil  outType
      Cons inType x xs -> Cons outType (f x) (map inType outType f xs)

When I program without dependent types, I regularly find myself getting "stuck" inadvertently; knowing that (a) there's no way to make my current approach work in this language, (b) that it would be trivial to make it work if I could pass around types as values, (c) that I need to throw away what I've done and choose a different solution, and (d) the alternative solution I'll end up with will be less correct and less direct than my original approach (e.g. allowing more invalid states)

[andrewflnr]

Is there work on cleanly subsetting dependently typed languages to ones where well-typed-ness can be automatically proven? That's not generally the case, right? I think those concerns are basically why people come up with less-general typing mechanisms.

[chriswarbo]

The two main hurdles with dependent types are:

- Type-checking is undecidable. I've not found that to be much of a problem, since it can be given a timeout (or hit Ctrl-C).

- Soundness requires functions to be total (either terminating or co-terminating). That's generally a good idea anyway, but the approaches for doing this aren't particularly great; e.g. structural recursion is simple to implement and understand, but is very restrictive.

Idris makes the pragmatic choice of allowing the totality-checker to be turned off on a per-function basis; which is certainly no worse than using a language with no totality checking.

Another approach I've enjoyed using is Mtac in Coq: general recursion is an effect, which gets wrapped in a type (similar to Haskell's IO); there is an unwrapping function (like unsafePerformIO) but it gets executed at compile-time, so non-total functions create an infinite loop at compile time (rather than at runtime).

[dwohnitmok]

> Type-checking is undecidable.

This is only true if you allow non-total functions in your types, which most dependently-typed languages don't by default (i.e. the condition implied by your soundness condition).

By default in e.g. both Idris and Agda type-checking is decidable.