5 ms·

> Types are there whether you want them to be or not But this only applies to typed programs, right? For every type system you come up with there will be some

by ufo 12y ago

> Types are there whether you want them to be or not But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system. There is also a minor thing that came to my mind. Types are most often associated with intuitionist logics, which are about constructive provability, as opposed to classical logics, which are about "truthyness" so the title of the post is a bit misleading :)

dllthomas 12y ago
"But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system." In theory, yes - I came here to make that same objection. In practice, there arises the question of whether such terms are actually ever encountered for a given type system when solving realistic problems.
- comex 12y ago
  For most type systems, they certainly are: most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc. that a compiler for a typical high-level language cannot emit under any circumstances (without being ridiculously intelligent). Languages like ATS and C-plus-formal-verification mostly avoid this problem at the expense of being really hard to write.
  - dllthomas 12y ago
    "most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc." I'm not sure what you're saying here with the "corresponding to" - obviously you can write "unsafe pointers", unions, etc, right in C, and I've not really ever encountered inline assembly for the purposes of subverting the type system. I'll respond to more of your content when I'm confident I've understood you (which I don't mean as a brush off...).
    - comex 12y ago
      My response was poorly worded, but what I meant is that compilers for other languages with higher level type systems (which make more guarantees) cannot emit the same assembly as a C compiler, not that assembly is needed to subvert C's type system.
      - steveklabnik 12y ago
        Why not? Can you show me an example of what you mean? EDIT: I think the difference here is between 'types' and 'tags'. Types are at compile time. Tags are at runtime.
        deleted 12y ago
        [deleted]
        comex 12y ago
        All right, let's see if I can express what I'm talking about properly. I don't have much background in theory, but what I'm trying to say is pretty trivial, so... The article talks about translating from a typed lambda calculus to the untyped variant. Real compilers typically translate from the original typed AST gradually through multiple IRs to assembly, which is more complicated since they're changing the form of the program rather than just dropping type annotations, but is generally analogous. What I care about is whether there are programs with "terms" - instruction sequences - which correspond to useful programs which cannot be "typed" in a particular language, i.e. they cannot be produced by a compiler following any kind of straightforward procedure to lower from that language. Of course you can always come up with an equivalent program as long as the language is Turing complete; in particular, just as untyped lambda calculus can also be considered unityped, you can do something like Emscripten where you mechanically translate low level IR into a tiny subset of a higher level language, and maybe the compiler will optimize that subset. But that's not that interesting, because the general case is changing the program to a completely different one, and the special case removes all of the benefits of the type system. Additionally, you can have a language like Rust that lets the programmer poke holes in the type system, which is useful in practice but makes the type system no longer guarantee what it says it guarantees. So, of course, with these limitations, not only are there correct programs which typical, non-dependent type systems cannot express, but, judging by the high performance of C (which has a type system, but one that provides barely any guarantees and thus has barely any limitations) in practice, these programs are quite common and useful in practice. Dependent type systems, along with their Curry-Howard mirror of theorem provers for low-level languages, can almost always make up for this (though by Gödel's incompleteness theorem there is some correct program somewhere that they can't prove correct), but they're a relative pain to program in and for that reason are uncommon in practice. Or to put it another way, you have a choice between delegating verification of complex properties about programs (the types which are there whether you want them to be or not) to computers, which have rather poor insight, or to humans, which are notoriously unreliable. The ultimate type system is a general AI you can explain the situation to in English.
- ufo 12y ago
  My impression is that these type system limitations start showing up once you need to mix and match different type systems. For most terms there is a reasonable type system that will type it but when you scale up to your whole program/system then any single type system might not be able to cover all the terms that you want to write. Some type system features such as parametric polymorphism, subtyping, intersection types, linear types, etc are hard to mix in practice, especially when you worry about decidability and type inference. I think this is one of the reasons why dynamic languages are popular. It kind of lets you mix different programming styles in a single program, at the cost of laxer type checking (something I hope will get better in the future).
  - mkesper 12y ago
    The type checking isn't lax at all, at least not in Python.
    - ufo 12y ago
      The problem in Python is that type errors end up being reported later than they would in a typed language. For example, if I have a function f that expects an object and call it with f(None) its not going to immediately give me an error. Its only going to give an error when I try to call a method on that `None` and depending on how my program is structured the line with the erroneous f(None) call might not even end up appearing in the final stack trace.
  - waps 12y ago
    No, this is not true at all. In practice every program is typed. There is no useful function that is fully general, so in practice there are limits on the types and the values of the inputs. All dynamic typing gets you is that you can ignore this fact, and then hit it head on when you make a mistake. It is possible to give programs that are truly dynamically typed, but they are not "real" programs. What can you do to a variable with zero information on what it contains ? Not much : return it, pass it around, ... that's about it. The real complaints are mostly about two things 1) it's hard to know what type an input parameter should be, so I just don't. This is just not a valid complaint. But type inference helps a lot here. Generic programming catches the other usecases. 2) many languages make it really hard to correctly specify types. This is a language flaw. Dynamic typing can be an improvement over C code, but not over Haskell code. Other languages are somewhere in between. Sometime, it's another flaw that may exist : the standard libraries are not correctly thought out to have a good algebraic structure (e.g. correct IS-A relationships for all number types, and the ability to generalize over them) These complaints basically boil down to people having constructed wrong type systems. It's a flaw in many, many languages. Python and Haskell are the only ones I know to get it close to right. 3) You want to eval() in your program (or, for example, read in arbitrary json). If you're doing this, you're doing something wrong. Even if you do manage to isolate things correctly (history says you are unlikely to get this right), you're open to trivial DDOSing.
- steveklabnik 12y ago
  I would actually argue the opposite: in theory, there is a type system that describes every system, even 'untyped' ones, which are really uni-typed. In practice, there are often types that your type system can't express. I didn't start to really grok this till I saw dependent types. Then again, I am an amateur type theory enthusiast...
  - mrbbk 12y ago
    I agree in re: "In practice, there are often types that your type system can't express." That's central.
  - ngrilly 12y ago
    You wrote "in theory, there is a type system that describes every system": I would be very surprised if this is true. It would a major turnaround in modern mathematics. What is this theory? Any link?
    - gizmo686 12y ago
      The fact that there exists such a type system, does not mean that we have constructed it. Having said that, the theoretical existence of such a theory seems highly plausible, but without a proof, it would not surprise me to learn that such is impossible. Without a constructivist proof, it would not suprise me to learn that the existence of such a system is irrelevent (to applied computer science).
    - steveklabnik 12y ago
      As I mentioned with my caveat, I'm an amateur type theorist, so I'm still digging into a lot of things. Do you have some relevant literature for me about this being impossible? My claim may have been too strong: I meant more that "it hasn't been disproven that type systems are inherently disjoint." Similar to how physicists believe there's a Grand Unified Theory of physics, but that doesn't mean we actually know it yet.
      - poof131 12y ago
- marcosdumay 12y ago
  Well, in practice we write programs that behave well within the type system we are using. Thus, no, you won't find those very often, but it also does not mean that there is no problem.

by ufo 12y ago

dllthomas 12y ago

"But this only applies to typed programs, right? For every type system you come up with there will be some valid and normalizing term that cannot be typed under that type system." In theory, yes - I came here to make that same objection. In practice, there arises the question of whether such terms are actually ever encountered for a given type system when solving realistic problems.

comex 12y ago
For most type systems, they certainly are: most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc. that a compiler for a typical high-level language cannot emit under any circumstances (without being ridiculously intelligent). Languages like ATS and C-plus-formal-verification mostly avoid this problem at the expense of being really hard to write.
- dllthomas 12y ago
  "most reasonably large C programs contain assembly corresponding to unsafe pointers, unions, etc." I'm not sure what you're saying here with the "corresponding to" - obviously you can write "unsafe pointers", unions, etc, right in C, and I've not really ever encountered inline assembly for the purposes of subverting the type system. I'll respond to more of your content when I'm confident I've understood you (which I don't mean as a brush off...).
  - comex 12y ago
    My response was poorly worded, but what I meant is that compilers for other languages with higher level type systems (which make more guarantees) cannot emit the same assembly as a C compiler, not that assembly is needed to subvert C's type system.
    - steveklabnik 12y ago
      Why not? Can you show me an example of what you mean? EDIT: I think the difference here is between 'types' and 'tags'. Types are at compile time. Tags are at runtime.
      - deleted 12y ago
        [deleted]
      - comex 12y ago
        All right, let's see if I can express what I'm talking about properly. I don't have much background in theory, but what I'm trying to say is pretty trivial, so... The article talks about translating from a typed lambda calculus to the untyped variant. Real compilers typically translate from the original typed AST gradually through multiple IRs to assembly, which is more complicated since they're changing the form of the program rather than just dropping type annotations, but is generally analogous. What I care about is whether there are programs with "terms" - instruction sequences - which correspond to useful programs which cannot be "typed" in a particular language, i.e. they cannot be produced by a compiler following any kind of straightforward procedure to lower from that language. Of course you can always come up with an equivalent program as long as the language is Turing complete; in particular, just as untyped lambda calculus can also be considered unityped, you can do something like Emscripten where you mechanically translate low level IR into a tiny subset of a higher level language, and maybe the compiler will optimize that subset. But that's not that interesting, because the general case is changing the program to a completely different one, and the special case removes all of the benefits of the type system. Additionally, you can have a language like Rust that lets the programmer poke holes in the type system, which is useful in practice but makes the type system no longer guarantee what it says it guarantees. So, of course, with these limitations, not only are there correct programs which typical, non-dependent type systems cannot express, but, judging by the high performance of C (which has a type system, but one that provides barely any guarantees and thus has barely any limitations) in practice, these programs are quite common and useful in practice. Dependent type systems, along with their Curry-Howard mirror of theorem provers for low-level languages, can almost always make up for this (though by Gödel's incompleteness theorem there is some correct program somewhere that they can't prove correct), but they're a relative pain to program in and for that reason are uncommon in practice. Or to put it another way, you have a choice between delegating verification of complex properties about programs (the types which are there whether you want them to be or not) to computers, which have rather poor insight, or to humans, which are notoriously unreliable. The ultimate type system is a general AI you can explain the situation to in English.
ufo 12y ago
My impression is that these type system limitations start showing up once you need to mix and match different type systems. For most terms there is a reasonable type system that will type it but when you scale up to your whole program/system then any single type system might not be able to cover all the terms that you want to write. Some type system features such as parametric polymorphism, subtyping, intersection types, linear types, etc are hard to mix in practice, especially when you worry about decidability and type inference. I think this is one of the reasons why dynamic languages are popular. It kind of lets you mix different programming styles in a single program, at the cost of laxer type checking (something I hope will get better in the future).
- mkesper 12y ago
  The type checking isn't lax at all, at least not in Python.
  - ufo 12y ago
    The problem in Python is that type errors end up being reported later than they would in a typed language. For example, if I have a function f that expects an object and call it with f(None) its not going to immediately give me an error. Its only going to give an error when I try to call a method on that `None` and depending on how my program is structured the line with the erroneous f(None) call might not even end up appearing in the final stack trace.
- waps 12y ago
  No, this is not true at all. In practice every program is typed. There is no useful function that is fully general, so in practice there are limits on the types and the values of the inputs. All dynamic typing gets you is that you can ignore this fact, and then hit it head on when you make a mistake. It is possible to give programs that are truly dynamically typed, but they are not "real" programs. What can you do to a variable with zero information on what it contains ? Not much : return it, pass it around, ... that's about it. The real complaints are mostly about two things 1) it's hard to know what type an input parameter should be, so I just don't. This is just not a valid complaint. But type inference helps a lot here. Generic programming catches the other usecases. 2) many languages make it really hard to correctly specify types. This is a language flaw. Dynamic typing can be an improvement over C code, but not over Haskell code. Other languages are somewhere in between. Sometime, it's another flaw that may exist : the standard libraries are not correctly thought out to have a good algebraic structure (e.g. correct IS-A relationships for all number types, and the ability to generalize over them) These complaints basically boil down to people having constructed wrong type systems. It's a flaw in many, many languages. Python and Haskell are the only ones I know to get it close to right. 3) You want to eval() in your program (or, for example, read in arbitrary json). If you're doing this, you're doing something wrong. Even if you do manage to isolate things correctly (history says you are unlikely to get this right), you're open to trivial DDOSing.
steveklabnik 12y ago
I would actually argue the opposite: in theory, there is a type system that describes every system, even 'untyped' ones, which are really uni-typed. In practice, there are often types that your type system can't express. I didn't start to really grok this till I saw dependent types. Then again, I am an amateur type theory enthusiast...
- mrbbk 12y ago
  I agree in re: "In practice, there are often types that your type system can't express." That's central.
- ngrilly 12y ago
  You wrote "in theory, there is a type system that describes every system": I would be very surprised if this is true. It would a major turnaround in modern mathematics. What is this theory? Any link?
  - gizmo686 12y ago
    The fact that there exists such a type system, does not mean that we have constructed it. Having said that, the theoretical existence of such a theory seems highly plausible, but without a proof, it would not surprise me to learn that such is impossible. Without a constructivist proof, it would not suprise me to learn that the existence of such a system is irrelevent (to applied computer science).
  - steveklabnik 12y ago
    As I mentioned with my caveat, I'm an amateur type theorist, so I'm still digging into a lot of things. Do you have some relevant literature for me about this being impossible? My claim may have been too strong: I meant more that "it hasn't been disproven that type systems are inherently disjoint." Similar to how physicists believe there's a Grand Unified Theory of physics, but that doesn't mean we actually know it yet.
    - poof131 12y ago
marcosdumay 12y ago
Well, in practice we write programs that behave well within the type system we are using. Thus, no, you won't find those very often, but it also does not mean that there is no problem.