Not sure I get the point. The existence of a 1-argument function that takes type A to type B is semantically identical to a subtype/inheritance relationship. All the same problems pop up in basically the same ways. I genuinely thought that was what the article was talking about, but then my Haskell fu is very weak so maybe I've misunderstood the problem.

I thought your comment was specifically about co/contraviance in type parameters with subtyping, because industry has explored the idea of making this unsound (e.g. the Google Dart team). But yes, co/contravariance pops up everywhere and so an unsound type system (or no type system at all) is not the answer. We had best all understand it!

> so an unsound type system (or no type system at all) is not the answer

And my unpopular opinion is precisely that. "Sound" typesystems enforced at the expense of the kind of cognitive load we see here will hurt rather than help the expression of real world problems in code.

Literally, casting a C function pointer through a void* is a better answer. I'm serious.

But the problem of correct program construction does not go away. There is certainly a middle ground somewhere, beyond which proofs become too expensive for most users. For the sorts of systems I work on, the sweet spot is close to Haskell 98, for others it may well be Python (no types at all).

Structural row typing I hadn't heard about. Elm is on my to-learn list, so I'll look it up separately, but...

Coming from Haskell, what's the elevator pitch for it?

In a system with subtyping {x:int, y:int} is a subtype of {x:int}. You can have a function that receives {x:int} and you can pass a {x:int, y:int} to it. The subtype can be freely used whenever the supertype is expected.

With row typing instead of subtyping you have "row variables". That function that would receive a {x:int} is typed as "forall p. {x:int; p}". You can pass the function a {x:int, y:int} because it unifies p with {y:int}. But you cannot freely convert a {x:int, y:int} to a {x:int}, it is all based around parametric polymorphism.

This system with row variables works much better with hindley-milner type inference but it is a bit more restrictive. For example, you cannot use subtype polymorphism to have a heterogeneous list of objects. If you have a function that receieves a "forall p. [{x:int; p}]" you can have a list of {x:int} or a list of {x:int, y:int} but every element of the list must have the same type.

> you cannot use subtype polymorphism to have a heterogeneous list of objects

You can by using an existential type parameter, which 'forgets' the types in much the same way as an upcast.

[exists p. {x:int; p}]

IMHO, structural types are a better starting point. Nominal types can always be created by wrapping a structural type, but it is difficult to go the other way round. A language with row types can give a type to a query or have named function arguments. Extensible row types allow even more forms of composition, for example functions that require the presence of certain fields but will ignore others, very similar to subtyping.

structural vs nominal typing is orthogonal to row polymorphism vs subsumption rule.

Well not really as row polymorphism is a form of structural typing.

The elevator pitch for Elm is that it helps you build UIs which is just never easy. And mostly prescribes its own architecture instead of having you picking between vanilla React, Redux, Mobx, etc.

I never knew how amazing "if it compiles, it works" could be when building a UI.