Basically, yes. If you want your type checker to be decidable, you're going to have to restrict the type language to be much smaller. In general, dependent types are undecidable to type check.
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.
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).
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.
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.
"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.
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.
>Basically, yes. If you want your type checker to be decidable, you're going to have to restrict the type language to be much smaller. In general, dependent types are undecidable to type check.
In dependently typed programming languages like agda and Idris typechecking is decidable. You are wrong here.
You're right. I was being handwavey, and I apologize for that.
Let me clarify my position: In theory yes, you're right, it is decidable. In practice Agda and Coq force you to prove pretty much everything about your program using expensive annotations, in order to satisfy the typechecker. It's like pulling teeth. The type checker must be taught that your program terminates, and it must be taught that you maintain even the most simple of invariants.
There's a reason dependent types haven't caught on in industry, and even the "fancy" types that are cited by proponents as being used in practice (like ML's Hindley-Milner type system) are MUCH simpler than full blown dependent type systems. Because the burden is shifted to the programmer, and that makes it super unusable.
I'm not a dependent types hater. (I have dependent type friends :) ). But the best way to get a usable type system is to restrict it's expressivity to make automation easier, and the annotation burden much smaller. Sure, we're giving up something there. But it's better than having a system that can prove any theorem in the Calculus of Constructions, but used by about thirty people.
>Let me clarify my position: In theory yes, you're right, it is decidable. In practice Agda and Coq force you to prove pretty much everything about your program using expensive annotations, in order to satisfy the typechecker. It's like pulling teeth. The type checker must be taught that your program terminates, and it must be taught that you maintain even the most simple of invariants.
That's why we need gradual typing. Some critical parts should be written with full dependent types with termination checker, etc, but most of the code should be just type checked.
P.S. I have some dependent types experience, including applying Coq in commercial projects.
You're right with a strict reading. "In general, dependent types ..." should be a statement about all instances of "dependent types" or (weakening to one common English usage) a statement about typical instances of "dependent types". In neither case, are they undecidable.
A loose reading (probably overly loose, but possibly what was intended rather than what was expressed) would permit something closer to "Dependent types, in full generality, are undecidable to type check." which I believe to be the case, where actual implementations are more constrained (though decreasingly so!).