3 ms·

The problem with Go is that the type system is too dumb to actually enforce such things First of all, if there is one problem that is the problem with Go, I do

The problem with Go is that the type system is too dumb to actually enforce such things First of all, if there is one problem that is the problem with Go, I doubt that many Go programmers would agree that what you describe is it. Secondly, what you describe as a problem with Go's type system is actually a problem with all type systems for appropriate values of such things. A type is nothing more than a statement about an interesting property of a program which can be checked by a computer. Unfortunately, there are many interesting properties that would be desirable to check, which cannot be checked by a computer. Whether or not the program halts is the most famous. Some type systems are obviously more capable than others, but it's a spectrum. There is no divide between type safe and type unsafe.

catnaroek 10y ago
> what you describe as a problem with Go's type system is actually a problem with all type systems for appropriate values of such things. Not really. In a language with abstract data types, such as ML, an ordered set type only has actual ordered sets as its values. Languages without abstract types (not the same thing as abstract classes) are hobbled. > Unfortunately, there are many interesting properties that would be desirable to check, which cannot be checked by a computer. Who says everything has to be machine-verified? Let machines verify what they can easily verify, then verify the rest by hand. Optimal division of labor. You'd be surprised how much can be machine-verified if you arrange things properly. > Whether or not the program halts is the most famous. The lack of a general procedure for determining termination doesn't prevent you from proving it manually. For instance, a recursive function defined by structural induction on its argument is guaranteed to terminate. This covers most of the code I want to write in practice.
- adamlett 10y ago
  Not really. […] You seem to have missed the last part where I wrote "for appropriate values of such things". I didn't claim that all type systems have the exact limitations of Go, but merely that all type systems have limitations. Who says everything has to be machine-verified? I don't know. Certainly not I. But I'm sure you agree that it would be nice if more things were. Let machines verify what they can easily verify, then verify the rest by hand. Optimal division of labor. Yeah, unfortunately there are some things that neither machines nor humans are great at checking. But I agree of course. My point is still simply that you are drawing the line between type safe and not type safe arbitrarily. There are type systems that are more advanced than ML's. Does that mean that ML's type system is not type safe? No, because the term type safe has no agreed upon meaning! It is, as I said to begin with, a subjective value judgment. It means simply a type system which you find comfortable and trust.
  - catnaroek 10y ago
    > There are type systems that are more advanced than ML's. Does that mean that ML's type system is not type safe? No, because the term type safe has no agreed upon meaning! It is, as I said to begin with, a subjective value judgment. It means simply a type system which you find comfortable and trust. It's not about power. It's about fulfilling your promises. For instance, neither ML nor Go promises to prevent you from trying to use files after closing them. But C++ and Rust do, and it turns out only Rust actually fulfills this promise. Go is actually type safe for single-threaded use. However, it doesn't deliver on its promise of safe concurrency. If you send an object to another goroutine, say, via a channel, nothing prevents you from mutating the same object from both the sender and the receiver, without any sort of concurrency control. Of course, a corollary of all the above is that type safety buys you different things in different languages.
    - adamlett 10y ago
      So, if I understand you correctly, your definition of a type unsafe language is one in which the type checker claims to be able to verify some statement about the program, but is actually not reliable? Is that what you mean by fullfilling promises?
      - catnaroek 10y ago
        Yes.
        adamlett 10y ago
        I see that I have been mistaken in my claim that there is no objective definition of what type safety means. I read the Wikipedia article after reading your previous comment, because I think I finally understood what you meant. I was convinced that type safe was a different way of saying strongly typed, but now I see that they are not the same thing. Having now read various definitions of type safety, I still do not agree with your initial statement that type safe languages automatically precludes violations of the LSP. The Rectangle > Square problem does not happen because the programmer is not able to specify the necessary type constraints, but because she chooses not to. If by Rectangle one really means "A Rectangle which can mutate its width and height independently" and that can be encoded as a type then yes, a type safe language will enforce the LSP in this instance. But the requirement that a Rectangle has this particular behavior is not something that most programmers would think to enforce with a type, even if their language allowed it. When we model the world, we usually strive to only include what we consider to be essential, and the requirement that width and height should be independently adjustable would not be one many programmers would think essential to what is a Rectangle. But that one's model of a Rectangle has this particular feature is something that is easy to take for granted, and come to rely on once it is there. I.e. a model of a Rectangle is more useful with this feature, but without it, it is still a Rectangle. The problem is not the types. The errors you get when you violate LSP are not type errors, but logic errors.

catnaroek 10y ago

> what you describe as a problem with Go's type system is actually a problem with all type systems for appropriate values of such things. Not really. In a language with abstract data types, such as ML, an ordered set type only has actual ordered sets as its values. Languages without abstract types (not the same thing as abstract classes) are hobbled. > Unfortunately, there are many interesting properties that would be desirable to check, which cannot be checked by a computer. Who says everything has to be machine-verified? Let machines verify what they can easily verify, then verify the rest by hand. Optimal division of labor. You'd be surprised how much can be machine-verified if you arrange things properly. > Whether or not the program halts is the most famous. The lack of a general procedure for determining termination doesn't prevent you from proving it manually. For instance, a recursive function defined by structural induction on its argument is guaranteed to terminate. This covers most of the code I want to write in practice.

adamlett 10y ago
Not really. […] You seem to have missed the last part where I wrote "for appropriate values of such things". I didn't claim that all type systems have the exact limitations of Go, but merely that all type systems have limitations. Who says everything has to be machine-verified? I don't know. Certainly not I. But I'm sure you agree that it would be nice if more things were. Let machines verify what they can easily verify, then verify the rest by hand. Optimal division of labor. Yeah, unfortunately there are some things that neither machines nor humans are great at checking. But I agree of course. My point is still simply that you are drawing the line between type safe and not type safe arbitrarily. There are type systems that are more advanced than ML's. Does that mean that ML's type system is not type safe? No, because the term type safe has no agreed upon meaning! It is, as I said to begin with, a subjective value judgment. It means simply a type system which you find comfortable and trust.
- catnaroek 10y ago
  > There are type systems that are more advanced than ML's. Does that mean that ML's type system is not type safe? No, because the term type safe has no agreed upon meaning! It is, as I said to begin with, a subjective value judgment. It means simply a type system which you find comfortable and trust. It's not about power. It's about fulfilling your promises. For instance, neither ML nor Go promises to prevent you from trying to use files after closing them. But C++ and Rust do, and it turns out only Rust actually fulfills this promise. Go is actually type safe for single-threaded use. However, it doesn't deliver on its promise of safe concurrency. If you send an object to another goroutine, say, via a channel, nothing prevents you from mutating the same object from both the sender and the receiver, without any sort of concurrency control. Of course, a corollary of all the above is that type safety buys you different things in different languages.
  - adamlett 10y ago
    So, if I understand you correctly, your definition of a type unsafe language is one in which the type checker claims to be able to verify some statement about the program, but is actually not reliable? Is that what you mean by fullfilling promises?
    - catnaroek 10y ago
      Yes.
      - adamlett 10y ago
        I see that I have been mistaken in my claim that there is no objective definition of what type safety means. I read the Wikipedia article after reading your previous comment, because I think I finally understood what you meant. I was convinced that type safe was a different way of saying strongly typed, but now I see that they are not the same thing. Having now read various definitions of type safety, I still do not agree with your initial statement that type safe languages automatically precludes violations of the LSP. The Rectangle > Square problem does not happen because the programmer is not able to specify the necessary type constraints, but because she chooses not to. If by Rectangle one really means "A Rectangle which can mutate its width and height independently" and that can be encoded as a type then yes, a type safe language will enforce the LSP in this instance. But the requirement that a Rectangle has this particular behavior is not something that most programmers would think to enforce with a type, even if their language allowed it. When we model the world, we usually strive to only include what we consider to be essential, and the requirement that width and height should be independently adjustable would not be one many programmers would think essential to what is a Rectangle. But that one's model of a Rectangle has this particular feature is something that is easy to take for granted, and come to rely on once it is there. I.e. a model of a Rectangle is more useful with this feature, but without it, it is still a Rectangle. The problem is not the types. The errors you get when you violate LSP are not type errors, but logic errors.