Hacker News Reader

Comment by ajross | Hacker News Reader

Unpopular opinion: co/contravariant representations represent exactly the point at which formal typesafety starts hurting instead of helping as an engineering practice.

In all circumstances where you find the need to worry about this stuff to get your real-world code to build, your project would have been better served by an environment that just let you do trick with runtime validation, or even an unsafe typecast. The resulting code is cleaner, simpler, easier to maintain and more straightforward to evolve than the "correct" madness that results from proper functional analysis.

I'll take my downvotes, thanks.

View on HN

> co/contravariant representations represent exactly the point at which formal typesafety starts hurting instead of helping as an engineering practice.

I can't understand what you mean by this. The Python 'list' type is covariant in its contents and comparison functions such as 'operator.lt' are contravariant in their arguments regardless of whether Python has types or not.

Co- and contravariance just are. They're not things that dynamic languages somehow don't have. They do have them! It's just harder to see them (and harder to take advantage of them for your own benefit).

> The Python 'list' type is covariant in its contents

  l1 = [0,1,1,0] # list(unsigned)
  l2 = l2 # list(int) includes all list(unsigned)
  l2[1] = -42 # error: l1 is no longer all unsigned

Mutatable references are pretty much never covariant. Immutable containers like `tuple` might be, but/because there's no support for appending to or otherwise modifying them.

A mutable array in Haskell is most certainly covariant so you may have to rethink your counterexample.

Haskell's Data.Array.IO IOArrays (which I assume you're talking about) are not covariant; they are invariant, with a very nice type inference system to paper over this in most cases.

  {-# OPTIONS_GHC -W -XRankNTypes -XImpredicativeTypes -XFlexibleContexts #-}
  import Data.Array.IO
  
  type Subtype = (forall a . a->Int)
  type Suptype = (Int -> Int)
  
  esub = (\_ -> 0) :: Subtype
  esup = (\x -> x+1) :: Suptype
  wantsub = (\f -> f 'a') :: Subtype -> Int
  wantsup = (\f -> f 0) :: Suptype -> Int
  
  writeArraySup :: IOArray Int Suptype -> IO ()
  writeArraySup a = writeArray a 1 esup
  
  main = do asub <- newArray (1,1) esub
            writeArraySup asub
            a1sub <- readArray asub 1
            print $ wantsub a1sub

In the above code, asub can be either (ie, not both) `IOArray Int Suptype` (in which case wantsub will fail to typecheck) or `IOArray Int Subtype`, in which case writeArraySup will fail to typecheck, because A'Sub isn't actually a subtype of A'Sup, because IOArray Int isn't actually covariant. You can see, I hope, that if they were covariant, and writeArraySup did typecheck, then we would end up passing 'a' (a Char) into (+) (expects Int) in violation of type safety.

If you meant some other mutable array type, then the same reasoning applies, but I can't be arsed to work out another concise example.

That's not the sort of variance that was discussed in the article, where an explicit mapping function is applied, not an implicit subtying relationship.

Some languages intentionally have an unsound type system in respect to variance, and rely on runtime checks for safety. It is a facet of the old static typing vs dynamic typing tradeoff.

Counter-opinion.

I work on a language, Dart, where all generics are covariant. In Dart 1, invalid uses of covariance were not checked at runtime and were silently ignored. When that leads to wrong behavior down the road, it's profoundly confusing. Not checking this and sacrificing safety, also ties your hands when it comes to compile time optimization because you can longer take any of your type annotations seriously.

In Dart 2, we've moved to a sound type system, which involves checking these misuses at runtime. I have personally gone through and fixed hundreds of these runtime failures. Others at Google have done the same. It's grueling, difficult work. Figuring out where an object was constructed before it eventually wound up somewhere in a covariant position is not easy.

I would much rather have static control over variance even with the additional complexity if causes, and I've heard similar requests from many users.

You don’t have a debug allocator that just tells you what file and line made the allocation? Ouch.

I would expect the debug allocator would need to be a full stack trace, file and line on their own would probably not be helpful. This is probably doable if they cache the allocation paths. But it would be interesting to hear about what tooling they've added to track these issues.

We have a lot of different execution environments (compiled to JS with debug compiler, compiled to JS with optimizing compiler, JIT VM, AoT VM, bytecode interpreter, Android, iOS, etc.) so that makes it a little more complex.

We do have allocation tracking in some of those, but that doesn't always get you as much as you'd expect. Discovering that, say, "oh, this list was deserialized by the JSON API" still means it could have come from dozens of different regions of the program.

I thought soundness (when it comes to statically-typed languages) means that the static type checker won't pass a program that would raise runtime type errors. Your comment (and Dart's website) was the first time I've read a claim of soundness by combining static type checker and runtime checks. Doesn't your definition mean that most type systems (even those of weakly and dynamically-typed languages) are sound. Even JS and PHP will eventually give up and give you a type error. Can't think languages other than C (which might give you segfaults or whathaveyou) that won't fit that definition of soundness.

Sincere question, what am I getting wrong?

"Sound" is one of those words whose definition varies more than you think. Some people use it to mean only statically proven to be free of type errors.

But, I think in practice, most languages that we call "sound" do indeed rely on some amount of runtime checking in order to guarantee that. Java and C# are both widely considered sound — and need to be to preserve memory safety! — and they both use runtime checking to ensure that (on cast operators and covariant array usage). I think even Haskell defaults to runtime checking of non-exhaustive pattern matching, which could be considered a form of "type errors".

> Doesn't your definition mean that most type systems (even those of weakly and dynamically-typed languages) are sound.

Dynamically-typed languages detect the type error right at the point where you try to perform an invalid operation for that type. They are safe in that that doesn't generally lead you into a hard crash or scary undefined behavior.

C# and Java are similar with respect to array usage — you get the type error right when you attempt to do a covariant store. Dart is similar for covariant generics.

But in most other cases, Dart detects the error earlier, at the point that you attempt to cast a value to the wrong type, not when you later use it as that wrong type.

> I have personally gone through and fixed hundreds of these runtime failures.

An interesting question here would be how many of those hundreds of failures were actual bugs and how many were just were just side effect of changing "dynamic is both top and bottom" rule.

So far I have not encountered a single actual issue when migrating users' code to Dart 2 - I encountered "unsoundly" typed code, but it actually worked and did not contain bugs.

Some, but not many actual bugs, but note that the corpus in question:

1. Is developed at a company with a stronger-than-average culture around quality and tests.

2. Already has copious tests.

3. Is mostly in applications that have been shipped in production.

So most of the bugs were already flushed out before we got to the point where we started tightening things. The more interesting question, which we don't have data for, is how much time it took to flush those bugs out the first time and how much the stricter runtime checking affects that. Hopefully it helps users find these kinds of issues faster.

You are I think making a comment about type parameters in object-oriented languages with subtyping? But why give up on static types so easily? How about a type system without subtyping (e.g. Haskell, OCaml) or even better one with structural row typing (e.g. OCaml, Purescript, Elm)?

Type systems are a form of machine-checked proof of correctness, at least for certain classes of errors. Sometimes proving things is laborious and a pain, but it is worth it if one cares about correctness (and often less effort than writing more unit tests).

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?

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.

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

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

> The resulting code is cleaner, simpler, easier to maintain and more straightforward

I'd love to see the day when our profession invents and adopts objective metrics for attributes such as these so we don't have to rely on opinions.

We have metrics such as cyclomatic complexity, however they don't connect with software engineers yet to drive decision making from my experience.

That’s a synthetic benchmark based on a theory about reading comprehension.

GP is talking about trying to measure reading comprehension to see which patterns actually work.

I think the argument to be made here is that gathering such metrics is difficult. So that's why no one does it.

Should we/can we improve upon it is another question.

I disagree. The problem is with the difference between a source and a sink not being represented in the type system. With that difference represented properly, variance becomes very simple. A source is covariant, a sink is contravariant and something that is both a source and a sink is invariant. That is slightly harder for the language designer but much easier for the user.

That covers many cases, but not all. Consider:

    bool contains(other) { ... }

This looks like a sink operation — you're passing a value in, just like you do with add() — but is naturally covariant, not contravariant.

That's a source operation. You aren't putting values into the collection, you are examining values in the collection.

Yes, except the type argument appears in parameter position, which is typically contravariant.

Okay, but it's not. Make source vs. sink explicit and it will be obvious because the method will be defined on source and not on sink.

Unpopular opinion indeed. As things are now, you can downcast to object and get your runtime validation in languages that support co/contravariance like C# and Java.

No one actually does this because its a horror show.

co-/contra-variance is a fact about the underlying data structure, not an aberration of the type system. You need to reason about it even in an untyped language.

The number of hours I've spent debugging Python/PHP code written by developers who don't understand co-/contra-variance...

Yeah, I've got to agree here. The problem with constructs like generics and co/contravariance is that they can (not will, but can) make code very hard to read, so you start to lose the ability to completely understand your code as you're scanning it with your eyes, whereas a situation where a class instance is simply being "re-cast" from an ancestor type to a descendant type to "help" the compiler is very easy to understand (although, I would definitely recommend a healthy dose of comments around such code). And, as you say, you can always use a run-time "is-a" check to make sure that you properly handle any violations at run-time that could bring the whole application down.

Of course, there are different metrics for different types of applications, and I'm sure that there are applications that need this level of type soundness as a matter of safety. However, I would surmise that most LOB applications are primarily interested in coding productivity and, as you say, these types of issues start to work against that productivity past a certain point.

What does "co/contravariant representations" even mean?

It sounds from this and your other comments on this thread that you are preaching from a relative point of ignorance about type systems.

This kind of anti-progress attitude is why writing software is miserable and we leave trillions in productivity on the table. Understanding how to use languages with advanced type systems takes some time if you are not used to it, but it's significantly _less_ arbitrary bullshit to absorb than what you had to learn to use C or Java effectively and comes with far more added value in return.

You're fundamentally on shaky ground when you use your ignorance as the basis for deciding someone else's level of ignorance.

Notice you started your response with a question. You need the right answer to that question before you can meaningfully continue.

Huh? I'm pointing out that the phrase used by OP doesn't really make much sense. I'm not like a dank profunctor whiz or something but I think I know what co/contravariance are...

The OP's statement doesn't make sense to you.

That doesn't necessarily mean OP's point doesn't make sense or that OP doesn't know what he/she it talking about. It means you need more info before you can judge. (Also: I didn't mean to make any statement about your knowledge of type systems. I was referring to your understanding of what OP was attempting to communicate.)

OP's statement doesn't make much sense in context of the article under discussion. Perhaps it make sense in another context.

He's arguing that gp's opinion is, in fact, grounded in his opening question's exemplary ignorance.

> Unpopular opinion: co/contravariant representations represent exactly the point at which formal typesafety starts hurting instead of helping as an engineering practice.

Type safety? It's a way to maintain soundness. Covariance and contravariance expands the amount of valid programs you can write within a language while maintaining soundness. It's fundamentally important if you want to reason about programs and make claims about the validity of programs.

> your project would have been better served by an environment that just let you do trick with runtime validation

Are you talking about dynamic programming? Trick with runtime validation? Are you talking about Java and C# runtime failures for their object arrays before generics? What do you exactly mean by trick?

> The resulting code is cleaner, simpler, easier to maintain and more straightforward to evolve than the "correct" madness that results from proper functional analysis.

So you'd rather have cleaner, simpler programs that are incorrect? You don't care about soundness? Or are you saying that removing co and contravariance in a language is a valid trade off even if it limits the set of valid programs within a language? It's not exactly clear what you are saying.

> > let you do trick with runtime validation

> What do you exactly mean by trick?

As I read the parent, they're using "do [the] trick" in the idiomatic sense of "get the job done" (more commonly heard in phrases like "X did the trick"), not saying that there's a specific "trick with runtime validation" that they want to do.

Reply on news.ycombinator.com