The Coq mailing list

[Stefan Monnier <monnier AT IRO.UMontreal.CA>]

> The usual objection is that typechecking is undecidable.  The party line
> for typed programming languages is that they should be Turing-complete but
> have decidable type-checking, or maybe even type inference.  F_omega +
> general recursion fits this profile.

I think this is just the result of a confusion between theory and practice.
Decidability of type-checking is neither necessary nor sufficient for
what people really want:
- decidability doesn't do them any good if it takes centuries (or
  petabytes) to terminate.
- lots of real languages have potentially non-terminating "compile-time
  operations" (whether it's type-checking, type-inference,
  macro-expansion, tactic expansion (to tie this back to Coq), ...)  and
  users don't seem to mind.

I think the more important aspect is that you can only erase terms which
are known to be pure (and hence terminating).  For that reason Type:Type
makes erasure of type arguments more difficult.


        Stefan