8 ms·

Following Godel:- my intuition suggests to me that for a sufficiently powerful programming language (Turing complete?), any type system will preclude otherwise

Following Godel:- my intuition suggests to me that for a sufficiently powerful programming language (Turing complete?), any type system will preclude otherwise valid statements in the language. Such illegal but valid statements will be much more numerous than legal statements. These statements may not just be valid, they may be useful, and perhaps even elegant!

naasking 7y ago
Sure, and our structural engineering tools and processes no doubt similarly rule out many highly artistic and potentially safe architectural designs. Notice how this argument only seems compelling to programmers when applied to programming. If you want to go beyond the safe norms, you would have to pay the cost of validating the safety of your design. The analog in programming might be theorem proving that your elegant design was still safe.
- somewhereoutth 7y ago
  Indeed, a type system is a great tool for producing correct code, and I cannot advocate doing away with type safety. However, my counter-argument would be that important failures often occur due to unforeseen interactions in complex systems, perhaps more so than due to actual defects. If a type system precludes simple solutions ("obviously no bugs"), then that may cause problems in itself. My feeling is that type systems should be separate from the language, and should statically validate in a progressive manner (eg Typescript on Javascript). As the type system is evolved to become more expressive, the amount of unsafe code can be reduced - but never quite eliminated (if my conjecture is correct).
- marcosdumay 7y ago
  > Sure, and our structural engineering tools and processes no doubt similarly rule out many highly artistic and potentially safe architectural designs. Once in a while, civil engineering has a revolution exactly because somebody proves that a class of new designs is safe. The argument is compelling on every field.
  - deleted 7y ago
    [deleted]
  - pas 7y ago
    There is already finite element analysis. It basically works on arbitrarily complex structures their internal connections, loads, etc. (It enabled the current boom in super skinny high rises and various fancy structures.) We don't really have that for programming, but it's not like we shouldn't try. (Eg we have TLA+ for processes, we can use Coq and others for proving some parts of programs.)
    - naasking 7y ago
      > We don't really have that for programming, but it's not like we shouldn't try. We do in the form of abstract interpretation and various other global static analyses. Unfortunately, these analyses are non-compositional, where small code changes can lead to dramatic and unpredictable long-range effects in the properties of your code. Finite-element analysis has similar non-compositional properties. A type system is a compositional form of static analysis, and composition obviously has considerable reuse and cost reduction benefits, which is probably why most programming doesn't use static analysis tools beyond type systems.
      - pas 7y ago
        Finite-element analysis - as far as I know - has the advantage of being able to estimate its own errors with some practically useful local upper bound. Because physics at that level is very much local. (Though it can't really help with higher level problems, like cyclic dynamical load and resonance problems, but there are other tools for that.) > [...] most programming doesn't use static analysis tools beyond type systems. Yes, unfortunately. :( It'd be great to have access to much better/stricter tools to be able to check just some interesting/important parts of programs (eg. pure business logic modules/functions) without resorting to reimplementing them in static-analysis systems.
        naasking 7y ago
pjc50 7y ago
And how do you prove that those statements are correct?
- somewhereoutth 7y ago
  That is the point - perhaps you can't, in the same way there are true statements in Peano arithmetic that cannot be proved (if my understanding is correct). The concern is that these statements may still be useful and elegant, and ruling them out may weaken a language significantly.
  - abathologist 7y ago
    CTT addresses this line of thinking: http://www.scholarpedia.org/article/Computational_type_theory#A_foundation_for_computer_science http://www.scholarpedia.org/article/Computational_type_theor... btw, I think you're missing an important qualification, which is that a given formalism can always be enriched with new axioms to increase the scope of what it's able to prove. This is relevant for type theoretic approaches, which generally have a mechanism for adding new axioms.
  - pjc50 7y ago
    .. at the cost of shipping products which have an higher chance of certain kinds of failures? Types are not just an engineering technology, they are a QA tool. (also, at no stage have you provided an example for such "more elegant" statements)
abathologist 7y ago
iiuc, the dichotomy "programming language vs. type system" doesn't hold for type-theoretic programming. E.g., languages based on System F (like Haskell) are based on a programming language that is inherently typed.
- somewhereoutth 7y ago
  Would I be correct to say that System F, and thus Haskell, has been effectively built on the untyped lambda calculus? If so there are many (very many!) statements in the LC that are illegal under System F. Certainly whole classes of pathological statements have been disqualified, but perhaps some baby has gone out with the bathwater? To take a much simpler example, the Simply Typed Lambda Calculus precludes non-terminating programs, but is not generally useful.
  - 6gvONxR4sf7o 7y ago
    No I don’t think it’s accurate to say they’re built on untyped lambda calculus, any more than simply typed lambda calculus is built on utyped lambda calculus. They’re very much related, and there’s a strong sense in which they are built on each other, but the kinds of programs available and what can be proved or guaranteed are different.
    - somewhereoutth 7y ago
      but (for the simply typed LC anyway) the 'mechanism of action' is just the untyped LC under beta reduction surely? I mean, the type annotations don't actually do anything when the program is run/reduced?
      - throwaway17_17 7y ago
        You are essentially identifying the semantic divergence between Church and Curry style types. Church-style or Intrinsically typed Lambda Calculus does not give any meaning to ill-typed expressions and there for beta-reduction can not proceed for these invalid expressions. Where as Curry-style or Extrinsically typed lambda calculus gives meaning to expression that do not consider the type alleged to be possessed by that expression.
dwohnitmok 7y ago
I've never really bought this argument. Casting is the way a programmer can selectively bypass the type system and every typed language I've ever used includes casting. For Church-typed languages as opposed to Curry-typed languages, it's not even apparent what it would would mean to "preclude otherwise valid statements" because types are a part of the language. It's akin to saying structured programming precludes otherwise valid statements in the language because the lack of goto precludes otherwise valid statements in the language. Sure, but the lack of goto is precisely a facet of the language! For a Church-typed language the types are just another part of syntax (this is more than just theory, Racket shows that a type system can in fact be implemented simply as macros). Invoking Godel here I don't think makes sense. Godel's incompleteness theorems apply to what you can prove about a program with types. The majority of typed programming languages have type systems that are too weak for Godel's incompleteness theorems to apply. And there is no need for a type system to be sound (if thought of as a logical system with programs as proofs via the Curry-Howard isomorphism), again most programming languages' type systems are not sound in this manner. Even with a Curry-style system of semantics, the presence of casting is enough to allow any type system to allow every valid statement in the language (the proof of this is to cast every term to the same type). That being said I am sympathetic to the feeling that "I'm just doing this to satisfy the type checker," a feeling that can show up increasingly frequently for languages with increasingly sophisticated type systems. I would argue this often happens precisely when you take the power of casting away. This is the dark side of "correct by construction" techniques where if the construction technique is devilishly complex, then you're forced to deal with that complexity. But this usually only applies to languages with some amount of dependent typing, which the majority of languages do not have.
- UncleMeat 7y ago
  Casting is not always permitted in all contexts. In C++, many casts that would be valid on the real machine are undefined behavior in the language, for example.
  - dwohnitmok 7y ago
    That's sort of the point though. Contexts where casting is not permitted in that sense are where the types are an integral part of the semantics of the language and for which it doesn't make sense to speak of "otherwise valid statements" (as indeed is the case here with C++). The original comment's "otherwise valid statements" are precisely UB in C++.
gliese1337 7y ago
That is more than just your intuition--with minor tweaking, it is a theorem that was taught in my Programming Language Theory course when I was in college! The tweak is that any safe type system will preclude programs that are otherwise semantically valid. You can have a type system that catches some errors and lets others through, or you can have a type system that catches all errors but also excludes some valid formulas (or even, and most commonly, a type system that catches most errors, also prohibits some valid formulas, but nevertheless still lets other errors through), but you can't have a decidable type system that permits all semantically valid programs and excludes all erroneous programs.
- hinkley 7y ago
  It’s also a multidimensional problem, so sometimes people improve the state of the art in one dimension, but either at the expense or the neglect of another. I think it’s a bit like any applied science. There’s a theoretical limit to the efficiency of an internal combustion engine. We grow closer to it, often with more complicated machinery, occasionally with better construction (ie, the manufacturing becomes more complex so the product is less complex). And we balance the consequences (pollution, reliability, cost) against the benefits. Once in a while we substitute a different model (E.g., Atkinson) with small but important differences in the theoretical limits, by looking at the problem differently.
throw149102 7y ago
This seems somewhat of a silly critique. By the same logic, we know that the vast majority of problems can not be solved by any program, yet we write programs to solve problems everyday. Or we know that the vast majority of mathematical statements cannot be proven or disproven, yet we can do math proofs just fine. I think we don't suffer from this because we end up asking questions that are relatively simple. Technically, there are many more uncomputable numbers than computable ones, but we are much more interested in the infinitely smaller set of the computable numbers than the uncomputables. (Furthermore, we are much more interested in rationals than we have any right to be, considering that there are many more real numbers than rationals). There should be a similar premise for type systems. Perhaps any type system will disallow valid statements, but we can try to make it so that those valid statements are above a certain length, say 100,000. Then, there are still infinitely many valid statements that are illegal, and they may be much more elegant than their counterparts, but they're so long that it is irrelevant for practical purposes. Now, actually building a type system like that is a whole 'nother beast. I imagine you would give up some notion of completeness for a level of "predisposition", that is, the type system predisposes programmers to making legal statements in the same way that normal number systems(reals, rationals) predisposes mathematicians to making provable statements. A slight nudge towards writing programs in a certain style can go a long way in terms of avoiding "illegal but valid" statements.

naasking 7y ago

Sure, and our structural engineering tools and processes no doubt similarly rule out many highly artistic and potentially safe architectural designs. Notice how this argument only seems compelling to programmers when applied to programming. If you want to go beyond the safe norms, you would have to pay the cost of validating the safety of your design. The analog in programming might be theorem proving that your elegant design was still safe.

somewhereoutth 7y ago
Indeed, a type system is a great tool for producing correct code, and I cannot advocate doing away with type safety. However, my counter-argument would be that important failures often occur due to unforeseen interactions in complex systems, perhaps more so than due to actual defects. If a type system precludes simple solutions ("obviously no bugs"), then that may cause problems in itself. My feeling is that type systems should be separate from the language, and should statically validate in a progressive manner (eg Typescript on Javascript). As the type system is evolved to become more expressive, the amount of unsafe code can be reduced - but never quite eliminated (if my conjecture is correct).
marcosdumay 7y ago
> Sure, and our structural engineering tools and processes no doubt similarly rule out many highly artistic and potentially safe architectural designs. Once in a while, civil engineering has a revolution exactly because somebody proves that a class of new designs is safe. The argument is compelling on every field.
- deleted 7y ago
  [deleted]
- pas 7y ago
  There is already finite element analysis. It basically works on arbitrarily complex structures their internal connections, loads, etc. (It enabled the current boom in super skinny high rises and various fancy structures.) We don't really have that for programming, but it's not like we shouldn't try. (Eg we have TLA+ for processes, we can use Coq and others for proving some parts of programs.)
  - naasking 7y ago
    > We don't really have that for programming, but it's not like we shouldn't try. We do in the form of abstract interpretation and various other global static analyses. Unfortunately, these analyses are non-compositional, where small code changes can lead to dramatic and unpredictable long-range effects in the properties of your code. Finite-element analysis has similar non-compositional properties. A type system is a compositional form of static analysis, and composition obviously has considerable reuse and cost reduction benefits, which is probably why most programming doesn't use static analysis tools beyond type systems.
    - pas 7y ago
      Finite-element analysis - as far as I know - has the advantage of being able to estimate its own errors with some practically useful local upper bound. Because physics at that level is very much local. (Though it can't really help with higher level problems, like cyclic dynamical load and resonance problems, but there are other tools for that.) > [...] most programming doesn't use static analysis tools beyond type systems. Yes, unfortunately. :( It'd be great to have access to much better/stricter tools to be able to check just some interesting/important parts of programs (eg. pure business logic modules/functions) without resorting to reimplementing them in static-analysis systems.
      - naasking 7y ago

pjc50 7y ago

And how do you prove that those statements are correct?

somewhereoutth 7y ago
That is the point - perhaps you can't, in the same way there are true statements in Peano arithmetic that cannot be proved (if my understanding is correct). The concern is that these statements may still be useful and elegant, and ruling them out may weaken a language significantly.
- abathologist 7y ago
  CTT addresses this line of thinking: http://www.scholarpedia.org/article/Computational_type_theory#A_foundation_for_computer_science http://www.scholarpedia.org/article/Computational_type_theor... btw, I think you're missing an important qualification, which is that a given formalism can always be enriched with new axioms to increase the scope of what it's able to prove. This is relevant for type theoretic approaches, which generally have a mechanism for adding new axioms.
- pjc50 7y ago
  .. at the cost of shipping products which have an higher chance of certain kinds of failures? Types are not just an engineering technology, they are a QA tool. (also, at no stage have you provided an example for such "more elegant" statements)

abathologist 7y ago

iiuc, the dichotomy "programming language vs. type system" doesn't hold for type-theoretic programming. E.g., languages based on System F (like Haskell) are based on a programming language that is inherently typed.

somewhereoutth 7y ago
Would I be correct to say that System F, and thus Haskell, has been effectively built on the untyped lambda calculus? If so there are many (very many!) statements in the LC that are illegal under System F. Certainly whole classes of pathological statements have been disqualified, but perhaps some baby has gone out with the bathwater? To take a much simpler example, the Simply Typed Lambda Calculus precludes non-terminating programs, but is not generally useful.
- 6gvONxR4sf7o 7y ago
  No I don’t think it’s accurate to say they’re built on untyped lambda calculus, any more than simply typed lambda calculus is built on utyped lambda calculus. They’re very much related, and there’s a strong sense in which they are built on each other, but the kinds of programs available and what can be proved or guaranteed are different.
  - somewhereoutth 7y ago
    but (for the simply typed LC anyway) the 'mechanism of action' is just the untyped LC under beta reduction surely? I mean, the type annotations don't actually do anything when the program is run/reduced?
    - throwaway17_17 7y ago
      You are essentially identifying the semantic divergence between Church and Curry style types. Church-style or Intrinsically typed Lambda Calculus does not give any meaning to ill-typed expressions and there for beta-reduction can not proceed for these invalid expressions. Where as Curry-style or Extrinsically typed lambda calculus gives meaning to expression that do not consider the type alleged to be possessed by that expression.

dwohnitmok 7y ago

I've never really bought this argument. Casting is the way a programmer can selectively bypass the type system and every typed language I've ever used includes casting. For Church-typed languages as opposed to Curry-typed languages, it's not even apparent what it would would mean to "preclude otherwise valid statements" because types are a part of the language. It's akin to saying structured programming precludes otherwise valid statements in the language because the lack of goto precludes otherwise valid statements in the language. Sure, but the lack of goto is precisely a facet of the language! For a Church-typed language the types are just another part of syntax (this is more than just theory, Racket shows that a type system can in fact be implemented simply as macros). Invoking Godel here I don't think makes sense. Godel's incompleteness theorems apply to what you can prove about a program with types. The majority of typed programming languages have type systems that are too weak for Godel's incompleteness theorems to apply. And there is no need for a type system to be sound (if thought of as a logical system with programs as proofs via the Curry-Howard isomorphism), again most programming languages' type systems are not sound in this manner. Even with a Curry-style system of semantics, the presence of casting is enough to allow any type system to allow every valid statement in the language (the proof of this is to cast every term to the same type). That being said I am sympathetic to the feeling that "I'm just doing this to satisfy the type checker," a feeling that can show up increasingly frequently for languages with increasingly sophisticated type systems. I would argue this often happens precisely when you take the power of casting away. This is the dark side of "correct by construction" techniques where if the construction technique is devilishly complex, then you're forced to deal with that complexity. But this usually only applies to languages with some amount of dependent typing, which the majority of languages do not have.

UncleMeat 7y ago
Casting is not always permitted in all contexts. In C++, many casts that would be valid on the real machine are undefined behavior in the language, for example.
- dwohnitmok 7y ago
  That's sort of the point though. Contexts where casting is not permitted in that sense are where the types are an integral part of the semantics of the language and for which it doesn't make sense to speak of "otherwise valid statements" (as indeed is the case here with C++). The original comment's "otherwise valid statements" are precisely UB in C++.

gliese1337 7y ago

That is more than just your intuition--with minor tweaking, it is a theorem that was taught in my Programming Language Theory course when I was in college! The tweak is that any safe type system will preclude programs that are otherwise semantically valid. You can have a type system that catches some errors and lets others through, or you can have a type system that catches all errors but also excludes some valid formulas (or even, and most commonly, a type system that catches most errors, also prohibits some valid formulas, but nevertheless still lets other errors through), but you can't have a decidable type system that permits all semantically valid programs and excludes all erroneous programs.

hinkley 7y ago
It’s also a multidimensional problem, so sometimes people improve the state of the art in one dimension, but either at the expense or the neglect of another. I think it’s a bit like any applied science. There’s a theoretical limit to the efficiency of an internal combustion engine. We grow closer to it, often with more complicated machinery, occasionally with better construction (ie, the manufacturing becomes more complex so the product is less complex). And we balance the consequences (pollution, reliability, cost) against the benefits. Once in a while we substitute a different model (E.g., Atkinson) with small but important differences in the theoretical limits, by looking at the problem differently.

throw149102 7y ago

This seems somewhat of a silly critique. By the same logic, we know that the vast majority of problems can not be solved by any program, yet we write programs to solve problems everyday. Or we know that the vast majority of mathematical statements cannot be proven or disproven, yet we can do math proofs just fine. I think we don't suffer from this because we end up asking questions that are relatively simple. Technically, there are many more uncomputable numbers than computable ones, but we are much more interested in the infinitely smaller set of the computable numbers than the uncomputables. (Furthermore, we are much more interested in rationals than we have any right to be, considering that there are many more real numbers than rationals). There should be a similar premise for type systems. Perhaps any type system will disallow valid statements, but we can try to make it so that those valid statements are above a certain length, say 100,000. Then, there are still infinitely many valid statements that are illegal, and they may be much more elegant than their counterparts, but they're so long that it is irrelevant for practical purposes. Now, actually building a type system like that is a whole 'nother beast. I imagine you would give up some notion of completeness for a level of "predisposition", that is, the type system predisposes programmers to making legal statements in the same way that normal number systems(reals, rationals) predisposes mathematicians to making provable statements. A slight nudge towards writing programs in a certain style can go a long way in terms of avoiding "illegal but valid" statements.