Hacker News Reader

Comment by ekidd | Hacker News Reader

Pretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time. This is, of course, "undecidable", because it's Turing complete.

This is not necessarily the end of the world. If you go out of your way to write an actual compile-time program by abusing your type system, and that program contains an endless loop, you probably shouldn't be surprised that your compiler hangs.

Unsound type systems cause more headaches in practice. For example, TypeScript types are only trustworthy if your program is careful about boundaries with the outside world. In larger, older systems, I occasionally do get bit by this.

View on HN

> Pretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time.

It depends on what you mean by "something like" because Idris' dependent types are arguably equally as useful in practice but type checking remains decidable due to totality. This goes for Agda, Coq and Epigram (if it still exists?) as well for different technical reasons each, not that they are as convenient to program with.

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.

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.

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.

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.

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.

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.

What you say is kind of interesting but I get the impression that we are talking past each other.

id(X): ==(X, rec_0(0, X))

Sorry, what's this supposed mean, is it a definition? The propositional equality type has two or three arguments, I only see one (X) here, if as you say "id" is propositional equality.

In any case, nothing peculiar happens when we check a trace-annotated proof of bottom. We are free to use any particular finite-step unfolding of the non-normalizing proof.

We also don't need any paradox or inconsistency for a non-normalizing term, it is enough to work in ETT in a typing context which implies bottom, or which contains an undecidable equational theory, e.g. the rules of the SK-calculus.

> The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem

Decidability of type checking is always relative to a particular surface/raw syntax. A trace-annotated raw syntax does not need a normalization assumption for type checking.

I left the first argument of the equality type implicit, written fully it’s ==(0, X, rec_0(0, X)) since those terms are both of type 0.

The overall expression is shorthand for any term whose typechecking involves that type assertion. For example, type checking passing the term to the left of the colon to an identity lambda with argument type of the term to the right of the colon (λ(x: ==(0, X, rec_0(0, X))).x)(id(X)) will pass iff the left term’s type is right term.

I’m not talking about extensional type theories here (as Idris/MLTT is not extensional), so I don’t think I understand the relevance of the trace annotated proof. Idris will let you write the term I have above without any trace annotations so its typechecker must do something with it.

You’re right that a trace-annotated raw syntax doesn’t need normalization assumptions, but Idris is not trace annotated; the type checking algorithm is required to perform any normalization required without further direction from the user.

I think you might be confusing the language and the type system. Not saying anything about the runtime characteristics of the language (which is obviously Turing Complete), but the type system itself, which is TC. If the type system allows you to encode a TM, then it is undecidable, regardless of whether it terminates due to an incomplete type checker. Since the Idris type system allows you to encode a TM, then the type system is undecidable due to the Halting problem.

A type system cannot be TC. What you seem to talk about, is that if a type checker can simulate arbitrary TM's through an encoding of its input, then the type checker is necessarily non-total. This is correct. But the Idris checker is total and it is not possible to use it to simulate TMs.

The Idris type system does allow you to specify and formalize TMs internally, but that has no bearing on decidability of type checking, as I explained before.

A type system can be TC. A type system is a logical system comprising a set of rules that assigns a property called a type to the various constructs of a computer program, such as variables, expressions, functions or modules. If those rules can encode a Turing complete system, then the system is Turing complete. Type checking is the process of verifying and enforcing the constraints of types. Type assignment is different from verification.

Sure, you don't have to go out of your way to challenge your type system, but it still means that you're a single typo away from sending your compiler and yourself on a wild goose chase.

Stage early and stage often; if a single-but-syntactically-valid typo will break your build then you should only be a commit away from something that works.

> Sure, you don't have to go out of your way to challenge your type system, but it still means that you're a single typo away from sending your compiler and yourself on a wild goose chase.

the alternative would be writing bash or python or ... scripts to generate the code, and for those :

- you likely don't have any error message at all (ugh)

- they won't have knowledge of the type system of the language you're operating.

Seriously, everyone complains about pages and pages of template errors, but if you use any decent IDE it's a two-click process to go to the part of your code where things fail. Errors will be split, then (at least with GCC & clang) you just start at the bottom of the error which is the place in your code where things go wrong 99% of the time - and if not, rarely if ever more than a couple steps above that. see e.g. : https://streamable.com/0k6lvl

There are mainstream languages with decidable static type systems. They compile quickly and give obvious short error messages.

names ! we want names !

also, decidable likely implies total - and my experience with total languages is that more often than not you need to add another turing-complete "scripting" layer on top of it (for instance, a TC language to generate expressions in the total language) as it's so cumbersome to write otherwise when you have actually business rules and not simple math examples

Reply on news.ycombinator.com