[solomatov]

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

[arjunnarayan]

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.

[solomatov]

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

[dllthomas]

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!).