[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