[Kutta]

Note though that undecidability is not really an issue in practice. You can always just refuse to run any function compile time that has not yet passed termination check. In fact Idris does exactly this. This already puts Idris ahead of C++ in terms of compilation termination, and it's not even like people are frequently disgruntled about diverging C++ templates.

[dllthomas]

"You can always just refuse to run any function compile time that has not yet passed termination check."

I don't understand this sentence.

[Kutta]

Both Idris and Agda check whether functions provably terminate. Halting problem notwithstanding it is possible to have conservative checks that never return false positives, so that an OK from the checker implies termination, but a FAIL doesn't imply non-termination.

Idris is not total by default, so it is not required that all functions pass the termination check. However, when Idris does the type checking it has to occasionally run Idris functions (that's what makes it dependent). This is in fact the only source of potential non-termination in the checker. So, whenever Idris needs to run a function compile time, and it cannot prove termination via the checker, it just throws an error.

(Side note: it is never required to run a function in order to the typecheck the very same function. All major dependent type checkers has the property that they never have to run a function that is not already checked).

[dllthomas]

So that was "You can always just refuse to run any function [at] compile time that has not yet passed termination check."?

All of this is certainly the case, and useful, and interesting. It doesn't contradict the point that 1) guaranteeing termination and 2) guaranteeing you return "no" on every incorrectly typed program are incompatible, which was approximately the original question.

[jessaustin]

Maybe I'm misunderstanding, but Kutta's description seems to handle 1) and 2) just fine. An additional requirement of "guaranteeing 'yes' on every correctly typed program" would lead to contradiction, but the point is that you don't need that requirement in practice.

[Kutta]

You're not misunderstanding. In short, we should rightfully expect our dependent type checker to be sound, if not complete. Weaker, non-dependent type systems can have complete checkers though, see for example

http://www.mpi-sws.org/~neelk/bidir.pdf

[dllthomas]

Hmm. Conceivably. I will have to revisit when I have more bandwidth.

[Someone]

"1) guaranteeing termination and 2) guaranteeing you return "no" on every incorrectly typed program are incompatible"

You do need more bandwidth. Trivial counterexample (for any reasonable inference of the semantics of the source code of this made-up language):

  define isCorrectlyTyped( program P)
  as
    return "no".

Of course, a practical version would have to have the function return "yes" on more valid programs :-)

By the way: compilers for languages such as Java and C# do something similar: they reject all programs that may use a variable before a value is assigned to it, at the price of rejecting some programs that properly assign a value to each variable before use on the grounds that the compiler cannot prove it. Typically, the language specification describes exactly how smart compilers can be (or rather, how stupid compilers must be) when checking this, to ensure that all compilers agree about what programs are valid.

[dllthomas]

Fair point! I was wrong above - "Can a dependent type system catch all type errors at compile time?" Yes, so long as you're okay with rejecting some correctly typed programs! If you're not okay with that, then your type checker might not halt. Shame it's too late to add an addendum above...

[aidenn0]

I can write a compiler in 5 minutes that handles both #1 and #2. It returns no on every program. Therefore it always terminates and always returns "no" on every incorrectly typed program.

[dllthomas]

Someone beat you to it.

https://news.ycombinator.com/item?id=7569967