4 ms·

Type checking /compiling often is conservative for this purpose. It's sound (Rejects all incorrect programs), decideable (There is an algorithm to reject all

Type checking /compiling often is conservative for this purpose. It's sound (Rejects all incorrect programs), decideable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect). There are exceptions of course (C++ templating is turing complete; so type-checking is undecidable) but often you want your compiler to be sound and decidable Also see https://3fx.ch/typing-is-hard.html https://3fx.ch/typing-is-hard.html (edit: Apparently , as the link I posted shows, rust is indeed undecidable in certain edge cases. However you can usually reason about a subset of the language (Restrict using certain features) that is still decidable. I have the feeling Rust might have such a subset but it's just a fuzzy feeling)

thaumasiotes 5y ago
> It's sound (Rejects all incorrect programs), decidable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect). Isn't that the definition of "semidecidable" as distinct from "decidable"? A decidable question is one where you can determine the answer, whatever that answer may be. A semidecidable question is one where, if the answer is yes, you can determine that, and if the answer is no, you may not be able to determine that. If you can always show that a program is incorrect, but you can't necessarily show that a program is correct, then the correctness of a program isn't decidable.
- cedilla 5y ago
  Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. It's the same as having a generator that generates every correct formula eventually. In my opinion, OP is incorrect and those systems are sound but indecidable.
  - thaumasiotes 5y ago
    > Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. By this definition, program incorrectness isn't semidecidable either - the compiler will accept all correct [incorrect] formulas, and will either reject or accept incorrect [correct] formulas.
    - ThreeFx 5y ago
      Not really, because for undecidable problems semidecidability can only hold one-way. If it held in both ways then the language would be decidable. Take the Halting program for example: For a program p which halts, you can determine whether it will halt in finite time (because by definition it halts). However, there is no semidecidable algorithm for "this program runs infinitely long".
      - thaumasiotes 5y ago
        I don't understand what you're trying to say. What are you contradicting with "Not really"? The claim above you is "by this definition, program incorrectness isn't semidecidable either". You're saying that it is?
- arianvanp 5y ago
  Decide-ability here means "Can we come to an answer in a known amount of steps". If you have an algorithm for type checking; then that answer is yes! You're _always_ able to come up with an answer that is yes or no. For example the following algorithm is for typechecking is decideable: typechecks :: Program -> Bool typechecks _ = false We always come to decision. There is no "semi" here. Just a clear yes/no answer. The algorithm is even sound. It rejects all incorrect programs. However it is not complete. It might also reject correct programs (In this case it rejects all correct programs). Of course you want a as little conservative typechecker without getting into trouble. But it's always conservative to some extent. Preferably you would both be sound _and_ complete. But the problem is that any reasonable logic system can't proof its own consistency. Hence we can't have both. However we can get "as close as we possibly can".
  - thaumasiotes 5y ago
    > We always come to decision. There is no "semi" here. That's not really how I understand the "semi" in the terminology. For a decidable question, you can recognize when the answer is yes, and you can recognize when the answer is no. For a semidecidable question, you can recognize when the answer is yes. It doesn't take much of a stretch to describe that as cutting your capabilities in "half". The way I usually think about this is that with full decidability, you can rule something in or out. With semidecidability, you can rule something in, but you can't rule things out. That framework extends well to the situation described above, where if the compiler chooses to compile a program, then the typing in that program was valid, and if the compiler chooses to complain about the typing, we can't draw any conclusions. It doesn't match your example; you can't rule anything in or out.
  - kmill 5y ago
    I believe you're explaining what a computable function is. A decidable set S of a type T is defined to be one for which there is a computable function f : T -> Bool such that the set of values x with f x = true is equal to S. A semidecidable set S of a type T is defined to be one for which there is a partial computable function f : T -> Bool such that whenever x is in S, then f x is computable and equals true. Given a definition for a well-typed program, you get a set W of Program of the well-typed programs. You can ask whether W is decidable or semidecidable -- i.e., whether there is some (partial) computable function f : Program -> Bool with the above properties. The example you give is certainly computable, but it has nothing to do with the set W, so it says nothing about (semi)decidability of the typechecking decision problem. However, it is a valid trying to find the largest subset of W that is (semi)decidable. Or trying to redefine what it means to be well-typed so that it is (semi)decidable! One interesting case of a programming language without a semidecidable typechecking problem is Lean. The typechecker they've implemented will both reject or time out on valid programs (so the typechecker is at least a computable function in a sense), but in practice these cases don't really occur.
jcelerier 5y ago
> There are exceptions of course for a definition of "exceptions" being "virtually all languages with a non-trivial static type system and non-zero userbase" as shown in your link. Java (https://arxiv.org/abs/1605.05274 https://arxiv.org/abs/1605.05274), C# (https://blog.hediet.de/post/how-to-stress-the-csharp-compiler https://blog.hediet.de/post/how-to-stress-the-csharp-compile...), Scala (https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/ https://michid.wordpress.com/2010/01/29/scala-type-level-enc...), Haskell, Rust (https://sdleffler.github.io/RustTypeSystemTuringComplete/ https://sdleffler.github.io/RustTypeSystemTuringComplete/), Typescript (https://github.com/Microsoft/TypeScript/issues/14833 https://github.com/Microsoft/TypeScript/issues/14833) ... Having a type system with generics and not being turing-complete as a result is the exception, not the rule.
- arianvanp 5y ago
  Haskell's System-F is definitely completely is decidable. You need to opt in to undecidable features like RankNTypes (n>=3) explicitly. (which are GHC; and not Haskell specific). Even then; Undecidability is a bit spectrumy. e.g. RankNTypes become sort of decideable again in the presence of explicit type annotations
  - smaddox 5y ago
    AFAIK, Haskell requires explicit types for higher-rank types specifically because inference is decidable for them.
- gnulinux 5y ago
  For an example of contrary, one can check Agda. It is not Turing complete, but a useful language (I personally wrote many parsers in it and its Haskell FFI is pretty good so you can essentially write unsafe parts of your programs in Haskell, and safe parts in Agda then prove correctness).
- octachron 5y ago
  Generics is not really the right cutting point: parametric polymorphism is perfectly decidable. However, few languages stop at just parametric polymorphism. For instance, the OCaml issue in the linked blog post happens at the module level, which mixes parametric polymorphism and subtyping. And typically, while SML has parametric polymorphism, it lacks the OCaml extension that makes the module type system undecidable.
LadyCailin 5y ago
Sort of a side track, but there’s a great layman’s intro to this in this Veratasium video https://m.youtube.com/watch?v=HeQX2HjkcNo https://m.youtube.com/watch?v=HeQX2HjkcNo

thaumasiotes 5y ago

> It's sound (Rejects all incorrect programs), decidable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect). Isn't that the definition of "semidecidable" as distinct from "decidable"? A decidable question is one where you can determine the answer, whatever that answer may be. A semidecidable question is one where, if the answer is yes, you can determine that, and if the answer is no, you may not be able to determine that. If you can always show that a program is incorrect, but you can't necessarily show that a program is correct, then the correctness of a program isn't decidable.

cedilla 5y ago
Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. It's the same as having a generator that generates every correct formula eventually. In my opinion, OP is incorrect and those systems are sound but indecidable.
- thaumasiotes 5y ago
  > Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. By this definition, program incorrectness isn't semidecidable either - the compiler will accept all correct [incorrect] formulas, and will either reject or accept incorrect [correct] formulas.
  - ThreeFx 5y ago
    Not really, because for undecidable problems semidecidability can only hold one-way. If it held in both ways then the language would be decidable. Take the Halting program for example: For a program p which halts, you can determine whether it will halt in finite time (because by definition it halts). However, there is no semidecidable algorithm for "this program runs infinitely long".
    - thaumasiotes 5y ago
      I don't understand what you're trying to say. What are you contradicting with "Not really"? The claim above you is "by this definition, program incorrectness isn't semidecidable either". You're saying that it is?
arianvanp 5y ago
Decide-ability here means "Can we come to an answer in a known amount of steps". If you have an algorithm for type checking; then that answer is yes! You're _always_ able to come up with an answer that is yes or no. For example the following algorithm is for typechecking is decideable: typechecks :: Program -> Bool typechecks _ = false We always come to decision. There is no "semi" here. Just a clear yes/no answer. The algorithm is even sound. It rejects all incorrect programs. However it is not complete. It might also reject correct programs (In this case it rejects all correct programs). Of course you want a as little conservative typechecker without getting into trouble. But it's always conservative to some extent. Preferably you would both be sound _and_ complete. But the problem is that any reasonable logic system can't proof its own consistency. Hence we can't have both. However we can get "as close as we possibly can".
- thaumasiotes 5y ago
  > We always come to decision. There is no "semi" here. That's not really how I understand the "semi" in the terminology. For a decidable question, you can recognize when the answer is yes, and you can recognize when the answer is no. For a semidecidable question, you can recognize when the answer is yes. It doesn't take much of a stretch to describe that as cutting your capabilities in "half". The way I usually think about this is that with full decidability, you can rule something in or out. With semidecidability, you can rule something in, but you can't rule things out. That framework extends well to the situation described above, where if the compiler chooses to compile a program, then the typing in that program was valid, and if the compiler chooses to complain about the typing, we can't draw any conclusions. It doesn't match your example; you can't rule anything in or out.
- kmill 5y ago
  I believe you're explaining what a computable function is. A decidable set S of a type T is defined to be one for which there is a computable function f : T -> Bool such that the set of values x with f x = true is equal to S. A semidecidable set S of a type T is defined to be one for which there is a partial computable function f : T -> Bool such that whenever x is in S, then f x is computable and equals true. Given a definition for a well-typed program, you get a set W of Program of the well-typed programs. You can ask whether W is decidable or semidecidable -- i.e., whether there is some (partial) computable function f : Program -> Bool with the above properties. The example you give is certainly computable, but it has nothing to do with the set W, so it says nothing about (semi)decidability of the typechecking decision problem. However, it is a valid trying to find the largest subset of W that is (semi)decidable. Or trying to redefine what it means to be well-typed so that it is (semi)decidable! One interesting case of a programming language without a semidecidable typechecking problem is Lean. The typechecker they've implemented will both reject or time out on valid programs (so the typechecker is at least a computable function in a sense), but in practice these cases don't really occur.

jcelerier 5y ago

> There are exceptions of course for a definition of "exceptions" being "virtually all languages with a non-trivial static type system and non-zero userbase" as shown in your link. Java (https://arxiv.org/abs/1605.05274 https://arxiv.org/abs/1605.05274), C# (https://blog.hediet.de/post/how-to-stress-the-csharp-compiler https://blog.hediet.de/post/how-to-stress-the-csharp-compile...), Scala (https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/ https://michid.wordpress.com/2010/01/29/scala-type-level-enc...), Haskell, Rust (https://sdleffler.github.io/RustTypeSystemTuringComplete/ https://sdleffler.github.io/RustTypeSystemTuringComplete/), Typescript (https://github.com/Microsoft/TypeScript/issues/14833 https://github.com/Microsoft/TypeScript/issues/14833) ... Having a type system with generics and not being turing-complete as a result is the exception, not the rule.

arianvanp 5y ago
Haskell's System-F is definitely completely is decidable. You need to opt in to undecidable features like RankNTypes (n>=3) explicitly. (which are GHC; and not Haskell specific). Even then; Undecidability is a bit spectrumy. e.g. RankNTypes become sort of decideable again in the presence of explicit type annotations
- smaddox 5y ago
  AFAIK, Haskell requires explicit types for higher-rank types specifically because inference is decidable for them.
gnulinux 5y ago
For an example of contrary, one can check Agda. It is not Turing complete, but a useful language (I personally wrote many parsers in it and its Haskell FFI is pretty good so you can essentially write unsafe parts of your programs in Haskell, and safe parts in Agda then prove correctness).
octachron 5y ago
Generics is not really the right cutting point: parametric polymorphism is perfectly decidable. However, few languages stop at just parametric polymorphism. For instance, the OCaml issue in the linked blog post happens at the module level, which mixes parametric polymorphism and subtyping. And typically, while SML has parametric polymorphism, it lacks the OCaml extension that makes the module type system undecidable.

LadyCailin 5y ago

Sort of a side track, but there’s a great layman’s intro to this in this Veratasium video https://m.youtube.com/watch?v=HeQX2HjkcNo https://m.youtube.com/watch?v=HeQX2HjkcNo