Comment by codygman | Hacker News Reader

Comment by codygman | Hacker News Reader

Parent Full thread

> Go model a square and a rectangle in your favorite statically typed language. Okay.

    data Shape = Square Int | Rectangle Int Int deriving (Show)

> You will find that square extends rectangle and setting the length on a square also sets the width. Why? I don't really see a need for square to extend a rectangle.

> So if I have a collection of rectangles which contains an unknown number of squares of which I set the width on each of them. Like this?

    > let unknowns = [(5,4),(3,2),(4,4)]
    > let toShape (x,y) = if x == y then Square x else Rectangle x y
    > map toShape unknowns
    [Rectangle 5 4,Rectangle 3 2,Square 4]

Tomorrow I'll see if I can make this type-safe by using dependent typing as shown in: [0][1][2]

This was easily solvable in my staticly typed language as you can see. In something like Idris I could have very easily encoded the toShape function the the type signature.

0: http://www.alfredodinapoli.com/posts/2014-10-13-fun-with-dep... 1: https://www.fpcomplete.com/user/konn/prove-your-haskell-for-... 2: http://jozefg.bitbucket.org/posts/2014-08-25-dep-types-part-...

Thats cool. Here's the somewhat equivalent in C++:

    struct square
    {
        int x;
    };

    struct rectangle
    {
        int x;
        int y;
    };

    boost::variant<square, rectangle> to_shape(int x, int y)
    {
        if (x == y) return square(x);
        else return rectangle(x, y);
    }

    std::vector<std::pair<int, int>> unknowns = {
        {5, 4},
        {3, 2},
        {4, 4}
    };

    auto shapes = unknowns | boost::adaptors::transformed(boost::fusion::make_fused(to_shape));

Of course, the structs are not polymoprhic and can't be printed out. I just left that out because it requires a little more code to do that. Obviously with haskell its much less code.

I would very much be interested in the dependently typed version.

Cool, it's always good to see other languages approaches (especially when idiomatic) to try out their way of thinking.

> I would very much be interested in the dependently typed version.

I'll try to get to it later today, I'm pretty busy until then.

And the same thing in D:

    struct Square
    {
        int sideLength;
    }

    struct Rectangle {
        int length;
        int width;
    }

    import std.variant;
    alias Shape = Algebraic!(Square, Rectangle);

    import std.typecons;
    auto to_shape(Tuple!(int, int) shape) pure nothrow
    {
        if (shape[0] == shape[1]) return Shape(Square(shape[0]));
        else return Shape(Rectangle(shape.expand));
    }

    void main() {
        auto unknowns = [
            tuple(5, 4),
            tuple(3, 2),
            tuple(4, 4)
        ];

        import std.stdio;
        import std.algorithm;
        writeln(unknowns.map!(to_shape));
    }

[Rectangle(5, 4), Rectangle(3, 2), Square(4)]

I've been debating whether or not to choose C++ or D to learn as my "when performance really matters" language. I'm still going to learn Rust, but I'm very interested in D. I also like that it has a pure keyword ;)

> I don't really see a need for square to extend a rectangle.

Except that a square is-a rectangle! Especially in terms of geometry. So you should be able to use this isomorphism in a type system as a perfect isomorphic mapping this is the entire purpose of the Liskov Substitution Principle. But the polymorphic result doesn't work polymorphically in a way that helps people reason about how the system works. It does things that are "correct" from a LSP and static typing system POV, but isn't helpful.

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.

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?

> 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.

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?

> 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.

> 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.

Mathematically, a rectangle and a square are entities that do not have mutable state; any particular square in mathematics has a fixed width and height.

If you define something that has a setWidth method, then it is not isomorphic to anything in mathematics! "is-a" is defined in terms of the operations that are valid.

What semantics would you specify for the setWidth of a rectangle?

The only reasonable contract for a general Rectangle is that setWidth sets the width but does not affect the height. Your proposed implementation of setWidth on a Square would violate that contract, and any other implementation would violate the invariant of the Square, and so it's clear that mutable Square "is-a" mutable Rectangle is simply not true.

Basically the problem you are looking at is a variant of the reference typing problem, where you have, given S <: T, for writing Ref S <: Ref T and for reading Ref T <: Ref S, and in the general case of the read-write reference there is no subtype relationship between Ref S and Ref T.

> Except that a square is-a rectangle! Especially in terms of geometry.

The thing in geometry that is called a "square" which is a special case of the thing in geometry which is called a "rectangle" is an immutable object whose side lengths and other features are part of its defining identity.

Modeling this relationship works perfectly fine in an OO language -- but squares and rectangles of this type are immutable objects.

A mutable square with operations which mutate the side lengths while preserving squareness is not a special case of a mutable rectangle with operations which mutate side lengths while preserving rectangleness without also preserving aspect ratio.

The analytical problem here is mistakenly assuming an is-a relationship that applies to immutable entities in geometry applies to mutable objects whose mutation operations are defined in such a way that the is-a relationship does not logically hold.

> So you should be able to use this isomorphism in a type system as a perfect isomorphic mapping this is the entire purpose of the Liskov Substitution Principle.

Actually, the entire purpose of the Liskov Substitution Principle is to provide an analytical basis for excluding mistakes like subclassing a mutable "Rectangle" class for a mutable "Square" class with operations that aren't consistent with an is-a relationship simply because of an intuition about an is-a relationship between squares and rectangles in geometry which doesn't actually hold when you analyze the operations on the particular entities you are modelling (which are outside of the geometric definitions of squares and rectangle.) The LSP defines what can and cannot be a subclass, and it rules out the kind of mutable square to mutable rectangle relationship you have proposed in this thread.

If LSP defines this why do people keep modeling things this way? More importantly, why do all the type systems let me create models this way. They have one job: to help me with correctness. Looks like that failed. So you see my point.

Reply on news.ycombinator.com