5 ms·

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

by ekidd 6y ago

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.

guerrilla 6y ago
> 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.
- bmc7505 6y ago
  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.
intortus 6y ago
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.
- dleslie 6y ago
  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.
- jcelerier 6y ago
  > 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 https://streamable.com/0k6lvl
  - intortus 6y ago
    There are mainstream languages with decidable static type systems. They compile quickly and give obvious short error messages.
    - jcelerier 6y ago
      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

by ekidd 6y ago

guerrilla 6y ago

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

bmc7505 6y ago
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.

intortus 6y ago

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.

dleslie 6y ago
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.
jcelerier 6y ago
> 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 https://streamable.com/0k6lvl
- intortus 6y ago
  There are mainstream languages with decidable static type systems. They compile quickly and give obvious short error messages.
  - jcelerier 6y ago
    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