[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.