Can you elaborate on the undecidability bit?
The task that isn't decidable is, what, "Given a program, determine whether the types are respected in all assignments" ?
I'm pretty sure that the calculus of constructions has dependent types, but wikipedia says that it is strongly normalizing, and I'm pretty sure that determining whether a program is valid in CoC is decidable? (Right? I could be wrong..)
> I'm pretty sure that the calculus of constructions has dependent types, but wikipedia says that it is strongly normalizing, and I'm pretty sure that determining whether a program is valid in CoC is decidable?
If you write a program in Coq where termination is not trivially true, you need to do the work and write a manual proof of termination. Given a program and something you claim to be a termination proof it's decidable whether that program with that proof is terminating and hence valid in CoC. Given an arbitrary program but no termination proof, I don't see how it can be decidable whether a termination proof of that program exists. You can write a Turing machine simulator in CoC (but won't be able to write a general termination proof).
For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops.
Ok, so the assumption I left out was, “for a turing complete language” or something like that (uh, in a sense in which “takes in a description of a Turing machine, an input to it, and a maximum number of steps, and runs the tm for up to that many steps” doesn’t count as turing complete)
> For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops.
I'm not sure about CoC-the-abstract-calculus-on-paper, but I guess it cannot allow programs that lack a termination proof. Coq-the-concrete-implementation-of-CoC does allow some. Or not, depending how you look at it: What it will really do is infer a termination proof behind the scenes for certain simple cases, like iterating over a list and the recursive call always being on the tail of the current list. So everything has a termination proof in Coq, it's just that in simple cases you get it for free.
I'm no type theory expert, but if you can describe natural numbers as:
Even (n: Natural) | n % 2 == 0
Then what's stopping you from doing:
Undecidable _ | loop {}
I'm not sure, but I think that's because strict dependent language systems like Pie (similar to CoC) use induction over the structure of a type for decidability. If I had 'the little typer' on hand, I'd elaborate more on this point. I think there's some relation between undecidability and the type Absurd, but I'd have to look into it more.
Just FYI, most dependent type systems don’t typecheck when a parameter to a type constructor is a function, since they can’t “deduce” very much about a function except its signature. They can take proof
objects (including objects involving evaluated functions, like ‘n % 2 = 0’) but not functions by themselves (like ‘loop {}’).
This isn’t a technical problem with unification, the issue is a fundamental conflict between “intensional” versus “extensional” equality. Wikipedia has a good example that communicates the underlying confusion: https://en.wikipedia.org/wiki/Extensionality
AFAIK all depedently-typed general-purpose languages use intensional equality since it’s consistent, but there are proof-checkers that use extensional dependent type theories (inconsistency is less of a problem than you might think, and actually makes some higher-order topology and set theory much easier to program).
I'm pretty sure that the calculus of constructions has dependent types, but wikipedia says that it is strongly normalizing, and I'm pretty sure that determining whether a program is valid in CoC is decidable? (Right? I could be wrong..)