[_halgari]

Author here, a few things to keep in mind:

Firstly, I wrote this about 3.5 years ago. I was wondering why people were suddenly commenting on it and now it all makes sense.

Part of the fun of writing articles about this is watching everyone argue about what language can be forced into representing types in a given way. Yes, I assume in any situation that if I want a feature X in a type system, that somehow Haskell can be forced to give me that feature, but that doesn't necessarily mean it will fit with the ecosystem of the language or that that's the only feature I'm looking for in the language. So saying "someone hasn't done their homework if they think X can't be done" isn't relevant, what is relevant that I'm not aware of a language that provides the type system features I want combined with acceptable set of trade-offs.

So anyways, I'll stick around for awhile and see if I can answer any questions. Thanks for the discussion, all!

[contravariant]

I'm somewhat curious why you'd want both (2) and (3) to hold. Isn't it somewhat contradictory to want types to not just merely denote the structure, while requiring that everything with the same structure satisfies the type?

Maybe it's because I'm influenced by C# but viewed from that perspective it would be like requiring you to explicitly declare that e.g. some value is a ProductID but when you're declaring a type you wouldn't need to declare it is a Person, provided it simply implements the right fields (in C# you would have to explicitly implementing some interface to clarify that first-name and last-name do indeed refer to a person and not, for example, the head and tail of a list of names). This does mean that any external code can't implement your interfaces though, which is a bit annoying, though fixable.

[jdmichal]

That's commonly called "duck-typing". And since you're discussing C#, I'll throw in that Typescript (another MS language) has duck-typing for interfaces. You can explicitly implement an interface, in which case the compiler will enforce that the interface is implemented. But you can also implicitly meet an interface.