5 ms·

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 exac

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
        > 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. The rectangle-square problem arises because there's no such thing as a type of rectangles in Go to begin with. Rectangles are mathematical objects, and mathematical objects don't mutate or have a physical identity in computer memory. If you change the width or the height of a rectangle, what you get is a different rectangle. > The problem is not the types. The errors you get when you violate LSP are not type errors, but logic errors. Types and logic are two different ways to look at essentially the same thing: https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

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
      > 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. The rectangle-square problem arises because there's no such thing as a type of rectangles in Go to begin with. Rectangles are mathematical objects, and mathematical objects don't mutate or have a physical identity in computer memory. If you change the width or the height of a rectangle, what you get is a different rectangle. > The problem is not the types. The errors you get when you violate LSP are not type errors, but logic errors. Types and logic are two different ways to look at essentially the same thing: https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...