6 ms·

Just because the current implementation of the Idris type checker always terminates due to the size change termination heuristic does not mean that type checkin

Just because the current implementation of the Idris type checker always terminates due to the size change termination heuristic does not mean that type checking Idris is decidable. If the type system as specified allows an author to express undecidable statements, it should not be considered decidable, regardless of whether one type checking implementation terminates on all inputs. If some type checker does not implement its type system, this is a property of the implementation, not the language. Otherwise any undecidable type system could easily call itself decidable by checking only a subset of the specification (in fact, this is exactly how most checkers for undecidable type systems work anyway). If the type system for a language is undecidable, type checking that language is undecidable.

guerrilla 6y ago
This is right. I was comparing Idris (the only existing implementation rather than its core type theory) to C++ (which has many implementations.) I think the situation may have be similar for Epigram as its core theory was very expressive but eliminators were only elaborated for strictly positive types or something like that (I might be wrong about this.) My point was just that the situation with C++ is worse than it has to be.
Kutta 6y ago
Incorrect. Whether the language as a logic is capable of expressing undecidable statements, is orthogonal to whether type checking is decidable. Type checking is analogous to checking proof validity in logics. Commonly used proof systems for first-order or higher-orders logics admit decidable proof validity, and already many first-order theories allow expressing undecidable statements. ZFC is a rather obvious example. Likewise intensional type theory is highly expressive as a logic and admits decidable proof validity. Decidability of type checking is instead related to how explicit surface syntax is. In intensional type theory, the usage of equality proofs is marked explicitly, which is sufficient to retain decidable type checking. In contrast, in extensional type theory, the usage of equality proofs is left implicit, which causes type checking to be undecidable.
- johncolanduoni 6y ago
  This is not true, as MLTT-style type theories have a different syntactical notion of proof than first order logical theories like ZFC. Proof of termination of type checking for Idris is equivalent to proof that all terms can be reduced to a normal form: for any given term, you can construct another term which when type checked requires fully normalizing the first term. It is well known that proving that the normal form evaluation of all terms in a MLTT type theory terminates is equivalent to the system’s consistency (because the false type has no constructors). This is how proofs of relative consistency of these type theories are usually proved.
  - Kutta 6y ago
    I don't see that "normalization implies consistency", which I'm aware of, relates to my previous comment in any relevant way. ZFC and MLTT do not differ in that decidability of proof validity is not related to logical expressiveness. It's not even true that for type theories, decidability of proof validity implies normalization. Normalization is not logically equivalent to decidable type checking. For example, we can have a term language for extensional type theory which is annotated with reduction traces. This is the kind of syntax that we get when we embed ETT inside ITT. It has decidable type checking, as the type checker does not have to perform reduction, it only has to follow traces. This kind of tracing is actually used in the GHC Haskell compiler to some extent. So we have decidable type checking for a surface syntax of a type theory, for a type theory which is a) consistent b) not strongly normalizing.
    - johncolanduoni 6y ago
      You’ve actually hit on the difference here: in the type theory the witness term plus the reduction trace is equivalent to the ZFC proof. It’s true that checking this combination is decidable, regardless of consistency. The intentionality does not eliminate the limitations of this property, it only provides that the reduction trace is implicit given the witness term. The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem, which assumes consistency of the type theory. Let’s come at this from the other direction. Suppose I find a non-normalizing term X of type false (like that produced by Girard’s paradox if we leave off stratification). What happens when I try to type check this? id(X): ==(X, rec_0(0, X)) Where id is the constructor of the propositional equality type and rec_0 is the recursor for False.

guerrilla 6y ago

This is right. I was comparing Idris (the only existing implementation rather than its core type theory) to C++ (which has many implementations.) I think the situation may have be similar for Epigram as its core theory was very expressive but eliminators were only elaborated for strictly positive types or something like that (I might be wrong about this.) My point was just that the situation with C++ is worse than it has to be.

Kutta 6y ago

Incorrect. Whether the language as a logic is capable of expressing undecidable statements, is orthogonal to whether type checking is decidable. Type checking is analogous to checking proof validity in logics. Commonly used proof systems for first-order or higher-orders logics admit decidable proof validity, and already many first-order theories allow expressing undecidable statements. ZFC is a rather obvious example. Likewise intensional type theory is highly expressive as a logic and admits decidable proof validity. Decidability of type checking is instead related to how explicit surface syntax is. In intensional type theory, the usage of equality proofs is marked explicitly, which is sufficient to retain decidable type checking. In contrast, in extensional type theory, the usage of equality proofs is left implicit, which causes type checking to be undecidable.

johncolanduoni 6y ago
This is not true, as MLTT-style type theories have a different syntactical notion of proof than first order logical theories like ZFC. Proof of termination of type checking for Idris is equivalent to proof that all terms can be reduced to a normal form: for any given term, you can construct another term which when type checked requires fully normalizing the first term. It is well known that proving that the normal form evaluation of all terms in a MLTT type theory terminates is equivalent to the system’s consistency (because the false type has no constructors). This is how proofs of relative consistency of these type theories are usually proved.
- Kutta 6y ago
  I don't see that "normalization implies consistency", which I'm aware of, relates to my previous comment in any relevant way. ZFC and MLTT do not differ in that decidability of proof validity is not related to logical expressiveness. It's not even true that for type theories, decidability of proof validity implies normalization. Normalization is not logically equivalent to decidable type checking. For example, we can have a term language for extensional type theory which is annotated with reduction traces. This is the kind of syntax that we get when we embed ETT inside ITT. It has decidable type checking, as the type checker does not have to perform reduction, it only has to follow traces. This kind of tracing is actually used in the GHC Haskell compiler to some extent. So we have decidable type checking for a surface syntax of a type theory, for a type theory which is a) consistent b) not strongly normalizing.
  - johncolanduoni 6y ago
    You’ve actually hit on the difference here: in the type theory the witness term plus the reduction trace is equivalent to the ZFC proof. It’s true that checking this combination is decidable, regardless of consistency. The intentionality does not eliminate the limitations of this property, it only provides that the reduction trace is implicit given the witness term. The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem, which assumes consistency of the type theory. Let’s come at this from the other direction. Suppose I find a non-normalizing term X of type false (like that produced by Girard’s paradox if we leave off stratification). What happens when I try to type check this? id(X): ==(X, rec_0(0, X)) Where id is the constructor of the propositional equality type and rec_0 is the recursor for False.