Writing tests in static languages is still required. You just have to write a smaller amount of them. What's more, type checking is enforced in a more systematic way. With tests, you have to rely on people to write them. If a type system is well designed, people will use it to model their code, and the type checking is done automatically.

What's more, types should not be reduced to the type checking phase. Types are a way to provide a high level model/structure. You still need this if you are working in a medium/large project. With static types, this model have nicer semantics, and is more useful.

Of course it's contrived but since I've been programming (which is longer than I care to say here, because it really dates me) this is basically where I'm at with static type systems. AS long as I've spent with them I find they're not as useful as they should be. I haven't tried Haskell (I probably should) but I'm getting too much done with dynamic languages, especially Lisps, to look back right now. Too much power to look away. Tschau!

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

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

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

    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));

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

    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));
    }

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

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.

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.

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.

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.

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.

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.

I don't think you're actually working with a well-defined subset of geometry. What is breaking here is the notion of persistent identity over time - "take this square and change its width - leaving us with not a new square/rectangle but the same square changed" - which I don't recall encountering in geometry.

The coordinates of the vertices are part of the identity of a square and in any reasonable model of a square cannot be changed.

An object with mutable size that is constrained to always be a square probably cannot be a member of a class which extends a class representing objects with mutable length and width that is constrained to remain a rectangle (but necessarily a square), since the properties of the former under mutation are not a simple extension of the properties of the latter, so that the two do not really have an is-a relationship (unless the transformations applicable to the two are designed in an unusual way -- as might be the case where the transformations on the rectangle were constrained to preserve the aspect ratio in all cases.)

People often on initial analysis how mutability really destroys is-a relationships which are based on relations between immutable entities.

Therefore, it can be seen, that there might be other, better ways to assert your system is correct than using types.

"setting the length"?? Do you mean "making a copy with the length set to a different value"?

If you have a square, which is-a rectangle, you can of course use the rectangle's copy function, or a rectangle lens or some such, to make a copy with a different length. Which will be a rectangle. Utterly trivial.

When I was writing tests I felt busier because I spent more time typing; now I spend more time thinking and less time writing code, but I'm ultimately more productive.

I'd also argue that the divide between dynamic, and static typing systems has fallen down. Almost completely.

Java/C# and even Haskell have dynamic typing. They even sort of have a scripting feel.

However, you can also statically type dynamic languages, and dynamic languages are getting static typing too. For example, JavaScript with asm.js. Lots of type inference is done by IDEs and lint systems now. Even with python, static type checking is very possible (both at the C level, and at the python level).

These two sentences are contradictory. You are merely making up your own language-specific static type system rules instead of learning how to use the one already provided by static type systems.

I will agree that languages with less flexible type systems to get in the way, but languages like Haskell, Ocaml, and other ML do a lot of the work for you.

> If you're test-driven, you're basically building up your own, domain specific compiler as you go not having to play by a language-specific static type systems rules. Dynamic typing make writing code this way really easy. Static typing doesn't.

Dynamic typing makes this easier for you to start writing code, not necessarily to get your end result faster. Dynamic typing allows you to build your own "type system of merely a language (as applied to your system)", and you can apply your lines of thought to it.

Static typing will require that you think about the types/type system of the language you are using and will inevitably slow you down at first. However it's not much different than the trade-off of using an existing library for a programming task or writing your own.

The marked difference is that I don't trust myself or many others to recreate a comprehensive type system rivalling that of mature compilers and people most likely much smarter than us.

The end result is that you have an ad-hoc type or effect system that isn't well defined, and the quality/correctness is assured through brute force by way of writing all the unit tests you can think of.

I assure you that you can't brute force test more edge conditions than your computer.

This post is getting long, but I feel like it really hits on why many "real world programmers" use Haskell and stronger static type systems: We don't trust ourselves, have been slapped in the face by our limitations and mistakes, so we would like to offload a ton of complexity to the compiler.

And now you're busy writing tests instead?