4 ms·

I'll admit I'm a little rusty on my geometry, but I'm fairly sure I was never told that a square is a rectangle. If you mean insofar as operations on rectangles

I'll admit I'm a little rusty on my geometry, but I'm fairly sure I was never told that a square is a rectangle. If you mean insofar as operations on rectangles should work on squares, this could be accomplished with typeclasses.

nickbauman 12y ago
Ah ha! Now you see the problem. Whether or not a square is a rectangle in a Euclidian sense it is a normal thing to use a type system in this way. And yet a discussion of it has emerged to whit this exchange. Gives one pause about the value of type systems for correctness eh?
- codygman 12y ago
  > Whether or not a square is a rectangle in a Euclidian sense it is a normal thing to use a type system in this way. Why do I care about whether or not it's normal way (for some people/languages) to use a type system in this way? I care about reality and having my types reflect it precisely. > Gives one pause about the value of type systems for correctness eh? I actually don't see how. It seems like you are saying "regardless of whether a square is a rectangle in reality, people (mis)use type systems to say this". Someone’s misuse of a tool doesn't call the tools value into question. Basically, I may not be able to model your exact relationships in the exact same way but I can model real world concrete things in the type-system which obtains the same or more flexibility and maintainability.
  - nickbauman 12y ago
    Exactly my point. This continuing misuse is VERY common even among experienced developers. The ongoing argument itself is a counterargument for type systems as being useful for correctness. At least it should give you some pause?
- dragonwriter 12y ago
  > Whether or not a square is a rectangle in a Euclidian sense It is. A square is a rectangle whose length and width are equal. > it is a normal thing to use a type system in this way. It is a common mistake to misuse an OO type system this way -- to take an intuition about is-a relations of immutable objects and infer an is-a relationship about mutable cousins of those objects, which is almost always wrong without careful constraints on the mutations. It is this kind of mistake which is addressed by the Liskov Substitution Principle. Of course, that's the reason the LSP is usually taught fairly early on in any OO programming course, because the mistake is well-known. > Gives one pause about the value of type systems for correctness eh? No, type systems are great for enforcing correctness, but they are no better than the analysis behind the definition of the types. Of course, violating the LSP with a bad subtyping relationship is just as problematic without a static type system.
  - nickbauman 12y ago
    > It is a common mistake to misuse an OO type system this way. So common, I would argue, that it suggests there is a fundamental problem or question of utility with using type systems for correctness. You're right that this has nothing to do with a _static_ type system specifically but they're almost always used together that when you say "static" you are almost always heard as "statically typed", so the point is moot in my experience.

nickbauman 12y ago

Ah ha! Now you see the problem. Whether or not a square is a rectangle in a Euclidian sense it is a normal thing to use a type system in this way. And yet a discussion of it has emerged to whit this exchange. Gives one pause about the value of type systems for correctness eh?

codygman 12y ago
> Whether or not a square is a rectangle in a Euclidian sense it is a normal thing to use a type system in this way. Why do I care about whether or not it's normal way (for some people/languages) to use a type system in this way? I care about reality and having my types reflect it precisely. > Gives one pause about the value of type systems for correctness eh? I actually don't see how. It seems like you are saying "regardless of whether a square is a rectangle in reality, people (mis)use type systems to say this". Someone’s misuse of a tool doesn't call the tools value into question. Basically, I may not be able to model your exact relationships in the exact same way but I can model real world concrete things in the type-system which obtains the same or more flexibility and maintainability.
- nickbauman 12y ago
  Exactly my point. This continuing misuse is VERY common even among experienced developers. The ongoing argument itself is a counterargument for type systems as being useful for correctness. At least it should give you some pause?
dragonwriter 12y ago
> Whether or not a square is a rectangle in a Euclidian sense It is. A square is a rectangle whose length and width are equal. > it is a normal thing to use a type system in this way. It is a common mistake to misuse an OO type system this way -- to take an intuition about is-a relations of immutable objects and infer an is-a relationship about mutable cousins of those objects, which is almost always wrong without careful constraints on the mutations. It is this kind of mistake which is addressed by the Liskov Substitution Principle. Of course, that's the reason the LSP is usually taught fairly early on in any OO programming course, because the mistake is well-known. > Gives one pause about the value of type systems for correctness eh? No, type systems are great for enforcing correctness, but they are no better than the analysis behind the definition of the types. Of course, violating the LSP with a bad subtyping relationship is just as problematic without a static type system.
- nickbauman 12y ago
  > It is a common mistake to misuse an OO type system this way. So common, I would argue, that it suggests there is a fundamental problem or question of utility with using type systems for correctness. You're right that this has nothing to do with a _static_ type system specifically but they're almost always used together that when you say "static" you are almost always heard as "statically typed", so the point is moot in my experience.