Are there some good examples of problems for which these sorts of programming tools are particularly helpful, or yield a particularly elegant solution, or is their role more academic?
I've used covariance and contravariance in C# before. I can't say its particularly elegant because it has the code spell of being too exotic but the alternatives if we did not use the features would have been a lot worse.
A kind of subtyping does show up in Haskell with higher-rank polymorphism: the System F “generic instance” subtyping rule. Namely, for types A and B, A is a subtype of B iff A is a “generic instance” of B, meaning A is at least as polymorphic as B.
“Higher-rank polymorphism” sounds scarier than it is, too, by the way. It’s basically just a way to pass polymorphic functions as arguments. It’s what you really want any time you think you’re craving a “virtual template” in C++; the typical OOP solution in a language like C# is more convoluted, usually consisting of wrapping the function in a class with a generic method and invoking it through an interface.
The intuition is that you can pass a more polymorphic function (like the identity function of type “∀a. a → a”) as an argument to a function expecting a less polymorphic one (like “Int → Int”) and it’ll just be specialised—but you clearly can’t do the reverse because “Int → Int” doesn’t accept all the types that “∀a. a → a” does (like “String → String”, “Char → Char”, “Bool → Bool”, &c.).
However, the subtyping gets flipped every time you go to the left of a function arrow, because it’s contravariant. And you only notice this with higher-rank polymorphism because that’s the only place Haskell has a subtyping rule like this. My usual example, stolen from an SPJ paper, is:
f ∷ ((∀a. [a] → [a]) → Int) → Int
f x = x (drop 1)
g ∷ ([Int] → [Int]) → Int
g y = sum (y [1, 2, 3])
h ∷ (∀a. a → a) → Int
h z = z 5
Or, in pseudo-imperative notation for those not familiar with Haskell:
“f g” works because “([Int] → [Int]) → Int” (the type of g) is more polymorphic than “(∀a. [a] → [a]) → Int” (the type of x, the parameter of f), because “[Int] → [Int]” (the type of y, the parameter of g) is less polymorphic than “∀a. [a] → [a]” (the type of the parameter of x).
f g
f (\ y -> sum (y [1, 2, 3]))
(\ y -> sum (y [1, 2, 3])) (drop 1)
sum (drop 1 [1, 2, 3])
sum [2, 3]
5
But “f h” is a type error, because “(∀a. a → a) → Int” (the type of h) is less polymorphic than “(∀a. [a] → [a]) → Int” (the type of x), because “∀a. a → a” is more polymorphic than “∀a. [a] → [a]” (the type of the parameter of x). And indeed it’s easy to come up with a type-incorrect implementation as I’ve done here—if you could run it, you’d end up trying to call “drop” on a number instead of a list:
Good point, haha, I did see the irony while writing that. I’ve moved that paragraph up toward the top in the hope it helps somewhat. :P
The thing about a lot of these big scary concepts in Haskell is that they’re really simple, the kind of thing where, once it clicks, you go “Oh! That’s all?”, but that doesn’t mean they’re easy—you’ve got to get familiar with the notation and jargon, and spend time building intuition from examples and just trying things out.
Nowadays I think of my process of learning new things as “try to realise how simple it is”, i.e. “what do experts understand (or just have memorised) that makes this easy for them?” It’s been a lot more motivating and pleasant than my old tactic of “try to cram this into my head without ‘chewing’ and hope my brain can digest it”.
Haskell does make a great semi-formal language with which to communicate functional programming ideas, even if you have no plans to ever use an implementation of it.
Mainstream languages are beginning to borrow more and more ideas from it (albeit often with significantly more verbose syntax). Much of the research literature in functional programming also uses Haskell syntax, so IMHO it is worth any developer learning.
I find in C# you use it without thinking about it because it usually makes sense when you have specific things you are trying to do, you often don't think too much about the types.
public interface ITalker
{
string Talk();
}
public class Robot : ITalker
{
public string Talk() => "Beep Boop";
}
class Program
{
static void Main(string[] args)
{
var robots = new List<Robot>() {new Robot()};
MakeEmTalk(robots);
DoStuffWithRobots(MakeEmTalk, robots);
}
private static void DoStuffWithRobots(Action<List<Robot>> robotoStuff, List<Robot> robots)
{
robotoStuff(robots);
}
private static void MakeEmTalk(IEnumerable<ITalker> talkers)
{
foreach (var talker in talkers)
{
Console.WriteLine(talker.Talk());
}
}
}
so intuitively, with MakeEmTalk, a list of robots should be able to be used where a enumerable list of talkers is required.
conversely ( contraversely? ) with DoStuffWithRobots, an action on a list of robots should be able to use a more generic action that works on an enumerable of Italkers, while we are only dealing with a list of robots there shouldn't be anything that stops us using something designed to work on a broader set of things.
Standardised principled abstractions make for better program composition and better API design. In the Haskell world, APIs are much less adhoc, more consistent and easily understood because of such mathematical abstractions (and the laws they imply, relating operations). Principled abstractions enable many other possibilities too, such as automatic program derivation. In Haskell I do not need to write any code to aggregate nested maps or parse a sudoku board, the compiler knows how to assemble such code automatically from the types.
Contravariance, as shown here, is extremely helpful for a working programmer and (like much of strongly typed functional programming) becomes more so as you begin to let go of that type of concern and just learn the stuff.
Say you have a JSON encoder that knows how to turn Strings into JSON. You can make an encoder for UUIDs with that encoder and a simple contramap operation.
In Scala:
// First, summon a String encoder
val stringEncoder: Encoder[String] = Encoder[String]
// Now contramap
val uuidEncoder: Encoder[UUID] =
stringEncoder.contramap[UUID](_.toString)
Of course, you're free to do this inline so there's not usually so much val-binding involved.
Profunctors are another great example of variance in functional programming. A profunctor is a type constructor that takes two arguments, one contravariant, one covariant.
The simplest example of this is the function type constructor (->): you can lmap (contramap) the first type parameter by composing a function before the input, or rmap (fmap) the second type parameter by composing a function after the result:
pipe :: A -> B
lmap (modifyInput :: A' -> A ) pipe :: A' -> B
rmap (modifyOutput :: B -> B') pipe :: A -> B'
Profunctors are the class of types that behave like functions or “pipes”—anything that takes input of some type and produces output of another type, which you want to be able to stitch together in a pipeline. In fact I think the only way to have a contravariant type parameter in Haskell is to use it on the left of a function arrow, or not use it at all; all Profunctor instances are wrappers for something function-like.
Well, one example I like when people ask me "what's contravariant good for?" is the following intuition. Suppose we're doing stream processing. We might have a datatype 'Source a' which is a source that produces a stream of a's.
'Source' is an example of a Functor. We can use 'fmap :: Functor f => (a -> b) -> f a -> f b' as '(a -> b) -> Source a -> Source b'. So, if we a function 'a -> b' we can turn a source of a's into a source of b's. Nice.
In such a library we would obviously also want a 'Sink a', this is a datatype that consumes a stream of a's. For example, it might write these a's to disk. Now, clearly it doesn't make sense for 'Sink' to be a functor. Think about it, if we have a sink that writes a's to disk, how would a function 'a -> b' affect it? Sure, we could turn all a's into b's, but then what? We don't know how to do anything with b's.
However, 'Sink' is a Contravariant (Functor). So, let's have a look at that. 'contramap :: Contravariant f => (a -> b) -> f b -> f a', so '(a -> b) -> Sink b -> Sink a'. If we have a 'Sink' that writes 'b' to disk and a function that turns a's into b's we can obviously construct a 'Sink a' that consumes a stream of a's, converts them to b's and passes them to the original 'Sink'.
And then there's a third abstraction not mentioned in the original post. The 'Profunctor', a Profunctor is a type that has two arguments and is contravariant in the first one, while the second is a regular Functor. In other words, if we have 'Pipe a b' this type can be made a Profunctor which comes with 'dimap :: Profunctor p => (a -> b) -> (c -> d) -> p b c -> p a d', which hopefully looks very similar to both Functor and Contravariant. In our stream processing example 'Pipe a b' would correspond with a pipe that consumes a stream of a's and turns it into a stream of b's which we can use to plumb 'Sink' and 'Source' together. We can both contramap it's first type argument to change what we can feed into it, as well as fmap the second type argument to alter what it produces.
These are from the only cases where these classes show up, but I hope they give some relatively easy to follow example on how these classes can capture some common scenario.
Thanks for your reply, I'm going to try to read it and the others carefully.
I wonder whether it's possible to bridge the gap more for people who are used to more conventional programming paradigms. For example,
> 'Source' is an example of a Functor. We can use 'fmap :: Functor f => (a -> b) -> f a -> f b' as '(a -> b) -> Source a -> Source b'. So, if we a function 'a -> b' we can turn a source of a's into a source of b's. Nice.
In python that's just
itertools.imap(function_a_to_b, stream_of_as)
and many other languages will have a similar construction.
So I immediately hit a block as I'm struggling to understand why I need the notion of a Functor to understand what in the end looks like just lazy mapping of a function over a stream.
> So I immediately hit a block as I'm struggling to understand why I need the notion of a Functor to understand what in the end looks like just lazy mapping of a function over a stream.
You don't, for this one example.
You don't, for any one example.
But if you keep looking, you'll find more and more of these examples of functors embedded in the code you are already writing. You need the notion of functor when you want to abstract over all of these examples, or generalize one of your examples to handle things that it couldn't before.
>So I immediately hit a block as I'm struggling to understand why I need the notion of a Functor to understand what in the end looks like just lazy mapping of a function over a stream.
What you're calling "lazy mapping a function over a stream" is an example of a functor. To be precise the functor goes from "type a" to "stream of type a" (note that this isn't quite the same as a function since it operates on the level of types).
You don't need to understand Functors to understand how mapping over a stream works, however if you understand mapping over a stream then you can understand any other functor as being similar to mapping over a stream. Now functors are somewhat basic so it's hard to come up with a really nontrivial example, but you could for instance consider:
to be pretty much the same thing as mapping over a stream, even though those functions can't be iterated over and could just be generating random data, or sample some time series etc.
Note that here we're transforming the output, when you start transforming the input you get something contravariant, like when you do something as follows:
class CoMapped:
# ... #
def __index__(self, a):
return self.object_with_b_index[self.function_a_to_b(a)]
it looks a bit weird to do this in Python though as there's no way to denote types.
> So I immediately hit a block as I'm struggling to understand why I need the notion of a Functor to understand what in the end looks like just lazy mapping of a function over a stream.
You don't need to understand Functor to understand "map over stream", no. But it turns out that Functor (and to slightly lesser extent Contravariant and Profunctor) keep showing up everywhere. It's not just stream processing, they show up in writing parsers, data structures, DSLs, software transactional memory...
For example, "computation that produces either an error or a result" and "transforming the result IFF the operation was successful" is also captured by Functor. And so is "perform IO and then transform the result of that IO". And "apply this function to all elements in a datastructure".
So, once you 1) realise that all these cases can be generalised to functors and 2) write down what the lawful behaviour if Functor is (i.e. "the spec"), we can suddenly start writing generic code that works for any Functor. So when I make 'Source' a Functor, my users get all the generic code written for any Functor for free.
Similarly Monoid, Applicative, Monad, and all these other abstractions occur all over the place. And you get this positive feedback cycle. We have generic code that works for any type that's an instance, so if we make new types instances of them, we get all this generic code for free. But the more types are instances, the more incentive there is to write even more generic code using these abstractions. Which in turns encourages ever more instances, etc.
So you never need to "understand" the abstractions for any specific instance/operation. It's just that if you have a lot of use-cases described by the same abstraction, recognising that this abstraction captures all these cases lets you get a lot of code reuse. And not only that, but also a powerful toolkit that you can use for working with basically any other library/code you encounter supporting them.
In Haskell Monoid, Functor, Applicative, Monad, and co provide you a toolbox that you end up able to reuse again and again for tons of different libraries all supporting them. These abstractions didn't gain wide-adoption for the sake of "theoretical elegance" (though they are elegant), they gained wide adoption due to the sheer pragmatic benefit they provide when programming.
As an example, Applicative itself was only invented in 2004, I started learning Haskell in 2007 and by that time about 80-90% of libraries in the ecosystem had started using it. You don't get that kinda adoption if you don't have anything to show for it :)
There are some other good replies already, but I really want to highlight that contravariance and covariance are not Haskell concepts; they're programming language concepts. They come up in object-oriented programming languages all the time too, especially once generics get involved. (Understanding the issues around -variance and generics in OO is an important part of the path of understanding why those sets of features aren't a thing you "just" put in a language, and why you end up with some sort of tradeoff in every implementation.)
As is often the case, you can muddle through without an explicit understanding of the issues, but you'll be a better programmer (better designs, faster understanding why certain error messages come up, etc... I mean a practically better programmer, not just academically better) if you understand these issues well.
Though I will confess that I have a hard time keeping straight which is co- and which is contra- once I step away from the issues for a while. I understand the concepts and their application at a practically-useful level, but I've never loved the naming scheme.
Variance inevitable rears its ugly face when you introduce a subtyping relation to your type system.
Variance is most visible in languages that mix parametric polymorphism (generics) with subtyping (for example, OO subclassing) because when this happens you may need to write down explicit variance annotations to appease the type checker.
However, variance still matters even without parametric types. For example, it describes what types you can use when overriding a methof in a subclass. The subclass is allowed to be "more general" than the superclass so if you want you can change the input parameters of the method to a more general supertype and you can change the return type to a more specific subtype. The output types are covariant: in the subclass where you create the method you can use a subclass of the return type. The input types are contravariant: in the subclass where you create the method you use a superclass of the input types.
If you speak Scala, I recommend that you familiarise yourself with Scala's implicits. The latter are a generalisation of type classes. You can implement the latter using the former, see e.g. [1].
If you speak ML/OCaml/F#, then Oleg's [2] might also be easily accessible.
What does the property 'contravariant' or 'covariant' belong to: function, functor, class, type class, data type, function or method argument, function or method return value, generic type/collection or something else?
Type variable. Since data definitions can bind new type variables, it's necessary to consider variance there and in the resulting type constructor, too.
From a mathematics perspective, they're a property of mappings between two categories (called functors). I think part of the confusion us simple programmers have (aside from no knowledge of category theory) is that these words are used without explicitly stating what categories we're dealing with. In the case of typed functional programming (e.g. Haskell), we're usually thinking about functors as mappings from the category of types, where the morphisms are function types, back to itself. But in the object-oriented world, these words are usually used in the context of a category of types where the morphisms indicate a subtype relationship.
I’m a little surprised you only got two answers, because I’m pretty sure the answer depends on how you look at the problem. Mine is this:
A function has variance because the types of its inputs or outputs are in a hierarchy.
An object type system (or I suppose even a functor system?) with generics might leverage variance to make sure that the behavior of its own methods is consistent with the Substitution Principle (LSP).
And many people will tldr this into variance being the tool to give you a type system that is LSP compatible. But it’s all about the operations, consuming and emitting types.
I think like this too. Would only like to add that I believe a type parameter is *variant in relation to a function/method, not just by itself. That's why some people say "appears in a covariant position " and so on.
Variance is related to type parameters in type constructors.
For example, consider the -> function type constructor. It has two parameters, the input type and the output type. Examples of function types are int->int and bool->bool.
The first parameter of the -> constructor (the type of the input) is contravariant while the second (the type of the output) is covariant.
For another example, consider the type of a generic immutable list, List<T>. The T type parameter of the List constructor is covariant.
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.
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).
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.
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.
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).
> 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.
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.
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.
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...
I probably should have written "kerfufflery" or something more colorful. The point was that dicking around with your type system trying to "understand contravariance" is directly hurting your ability to write and ship working solutions to real problems. Typesafety is only one axis (and a minor one at that) required by correct software, and this kind of masturbatory obsession with it doing no one any good.
There's a reason why so little true world class software (in the sense of beating out the competition with the sheer force of its value to users) is written in Haskell.
If that's "anti-progress", then sign me up I guess.
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.)
> 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.
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.
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.
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.
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...
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.
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.
"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.
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.
84 comments
[ 3.3 ms ] story [ 162 ms ] threadSimple C# doc page explaining the language feature in less academic and more brass tacks terms: https://docs.microsoft.com/en-us/dotnet/csharp/programming-g...
“Higher-rank polymorphism” sounds scarier than it is, too, by the way. It’s basically just a way to pass polymorphic functions as arguments. It’s what you really want any time you think you’re craving a “virtual template” in C++; the typical OOP solution in a language like C# is more convoluted, usually consisting of wrapping the function in a class with a generic method and invoking it through an interface.
The intuition is that you can pass a more polymorphic function (like the identity function of type “∀a. a → a”) as an argument to a function expecting a less polymorphic one (like “Int → Int”) and it’ll just be specialised—but you clearly can’t do the reverse because “Int → Int” doesn’t accept all the types that “∀a. a → a” does (like “String → String”, “Char → Char”, “Bool → Bool”, &c.).
However, the subtyping gets flipped every time you go to the left of a function arrow, because it’s contravariant. And you only notice this with higher-rank polymorphism because that’s the only place Haskell has a subtyping rule like this. My usual example, stolen from an SPJ paper, is:
Or, in pseudo-imperative notation for those not familiar with Haskell: “f g” works because “([Int] → [Int]) → Int” (the type of g) is more polymorphic than “(∀a. [a] → [a]) → Int” (the type of x, the parameter of f), because “[Int] → [Int]” (the type of y, the parameter of g) is less polymorphic than “∀a. [a] → [a]” (the type of the parameter of x). But “f h” is a type error, because “(∀a. a → a) → Int” (the type of h) is less polymorphic than “(∀a. [a] → [a]) → Int” (the type of x), because “∀a. a → a” is more polymorphic than “∀a. [a] → [a]” (the type of the parameter of x). And indeed it’s easy to come up with a type-incorrect implementation as I’ve done here—if you could run it, you’d end up trying to call “drop” on a number instead of a list:Well, there's some irony of writing that after 6 paragraphs filled with obscured Haskellise.
(Even though it's just some basic functional stuff in the end, like map, drop, sum etc, they will definitely look alien to anyone uninitiated).
The thing about a lot of these big scary concepts in Haskell is that they’re really simple, the kind of thing where, once it clicks, you go “Oh! That’s all?”, but that doesn’t mean they’re easy—you’ve got to get familiar with the notation and jargon, and spend time building intuition from examples and just trying things out.
Nowadays I think of my process of learning new things as “try to realise how simple it is”, i.e. “what do experts understand (or just have memorised) that makes this easy for them?” It’s been a lot more motivating and pleasant than my old tactic of “try to cram this into my head without ‘chewing’ and hope my brain can digest it”.
It's not true. I've seen PhD students use it!
conversely ( contraversely? ) with DoStuffWithRobots, an action on a list of robots should be able to use a more generic action that works on an enumerable of Italkers, while we are only dealing with a list of robots there shouldn't be anything that stops us using something designed to work on a broader set of things.
Say you have a JSON encoder that knows how to turn Strings into JSON. You can make an encoder for UUIDs with that encoder and a simple contramap operation.
In Scala:
// First, summon a String encoder
val stringEncoder: Encoder[String] = Encoder[String]
// Now contramap
val uuidEncoder: Encoder[UUID] = stringEncoder.contramap[UUID](_.toString)
Of course, you're free to do this inline so there's not usually so much val-binding involved.
The simplest example of this is the function type constructor (->): you can lmap (contramap) the first type parameter by composing a function before the input, or rmap (fmap) the second type parameter by composing a function after the result:
Profunctors are the class of types that behave like functions or “pipes”—anything that takes input of some type and produces output of another type, which you want to be able to stitch together in a pipeline. In fact I think the only way to have a contravariant type parameter in Haskell is to use it on the left of a function arrow, or not use it at all; all Profunctor instances are wrappers for something function-like.'Source' is an example of a Functor. We can use 'fmap :: Functor f => (a -> b) -> f a -> f b' as '(a -> b) -> Source a -> Source b'. So, if we a function 'a -> b' we can turn a source of a's into a source of b's. Nice.
In such a library we would obviously also want a 'Sink a', this is a datatype that consumes a stream of a's. For example, it might write these a's to disk. Now, clearly it doesn't make sense for 'Sink' to be a functor. Think about it, if we have a sink that writes a's to disk, how would a function 'a -> b' affect it? Sure, we could turn all a's into b's, but then what? We don't know how to do anything with b's.
However, 'Sink' is a Contravariant (Functor). So, let's have a look at that. 'contramap :: Contravariant f => (a -> b) -> f b -> f a', so '(a -> b) -> Sink b -> Sink a'. If we have a 'Sink' that writes 'b' to disk and a function that turns a's into b's we can obviously construct a 'Sink a' that consumes a stream of a's, converts them to b's and passes them to the original 'Sink'.
And then there's a third abstraction not mentioned in the original post. The 'Profunctor', a Profunctor is a type that has two arguments and is contravariant in the first one, while the second is a regular Functor. In other words, if we have 'Pipe a b' this type can be made a Profunctor which comes with 'dimap :: Profunctor p => (a -> b) -> (c -> d) -> p b c -> p a d', which hopefully looks very similar to both Functor and Contravariant. In our stream processing example 'Pipe a b' would correspond with a pipe that consumes a stream of a's and turns it into a stream of b's which we can use to plumb 'Sink' and 'Source' together. We can both contramap it's first type argument to change what we can feed into it, as well as fmap the second type argument to alter what it produces.
These are from the only cases where these classes show up, but I hope they give some relatively easy to follow example on how these classes can capture some common scenario.
I wonder whether it's possible to bridge the gap more for people who are used to more conventional programming paradigms. For example,
> 'Source' is an example of a Functor. We can use 'fmap :: Functor f => (a -> b) -> f a -> f b' as '(a -> b) -> Source a -> Source b'. So, if we a function 'a -> b' we can turn a source of a's into a source of b's. Nice.
In python that's just
and many other languages will have a similar construction.So I immediately hit a block as I'm struggling to understand why I need the notion of a Functor to understand what in the end looks like just lazy mapping of a function over a stream.
You don't, for this one example.
You don't, for any one example.
But if you keep looking, you'll find more and more of these examples of functors embedded in the code you are already writing. You need the notion of functor when you want to abstract over all of these examples, or generalize one of your examples to handle things that it couldn't before.
What you're calling "lazy mapping a function over a stream" is an example of a functor. To be precise the functor goes from "type a" to "stream of type a" (note that this isn't quite the same as a function since it operates on the level of types).
You don't need to understand Functors to understand how mapping over a stream works, however if you understand mapping over a stream then you can understand any other functor as being similar to mapping over a stream. Now functors are somewhat basic so it's hard to come up with a really nontrivial example, but you could for instance consider:
to be pretty much the same thing as mapping over a stream, even though those functions can't be iterated over and could just be generating random data, or sample some time series etc.Note that here we're transforming the output, when you start transforming the input you get something contravariant, like when you do something as follows:
it looks a bit weird to do this in Python though as there's no way to denote types.You don't need to understand Functor to understand "map over stream", no. But it turns out that Functor (and to slightly lesser extent Contravariant and Profunctor) keep showing up everywhere. It's not just stream processing, they show up in writing parsers, data structures, DSLs, software transactional memory...
For example, "computation that produces either an error or a result" and "transforming the result IFF the operation was successful" is also captured by Functor. And so is "perform IO and then transform the result of that IO". And "apply this function to all elements in a datastructure".
So, once you 1) realise that all these cases can be generalised to functors and 2) write down what the lawful behaviour if Functor is (i.e. "the spec"), we can suddenly start writing generic code that works for any Functor. So when I make 'Source' a Functor, my users get all the generic code written for any Functor for free.
Similarly Monoid, Applicative, Monad, and all these other abstractions occur all over the place. And you get this positive feedback cycle. We have generic code that works for any type that's an instance, so if we make new types instances of them, we get all this generic code for free. But the more types are instances, the more incentive there is to write even more generic code using these abstractions. Which in turns encourages ever more instances, etc.
So you never need to "understand" the abstractions for any specific instance/operation. It's just that if you have a lot of use-cases described by the same abstraction, recognising that this abstraction captures all these cases lets you get a lot of code reuse. And not only that, but also a powerful toolkit that you can use for working with basically any other library/code you encounter supporting them.
In Haskell Monoid, Functor, Applicative, Monad, and co provide you a toolbox that you end up able to reuse again and again for tons of different libraries all supporting them. These abstractions didn't gain wide-adoption for the sake of "theoretical elegance" (though they are elegant), they gained wide adoption due to the sheer pragmatic benefit they provide when programming.
As an example, Applicative itself was only invented in 2004, I started learning Haskell in 2007 and by that time about 80-90% of libraries in the ecosystem had started using it. You don't get that kinda adoption if you don't have anything to show for it :)
As is often the case, you can muddle through without an explicit understanding of the issues, but you'll be a better programmer (better designs, faster understanding why certain error messages come up, etc... I mean a practically better programmer, not just academically better) if you understand these issues well.
Though I will confess that I have a hard time keeping straight which is co- and which is contra- once I step away from the issues for a while. I understand the concepts and their application at a practically-useful level, but I've never loved the naming scheme.
Variance is most visible in languages that mix parametric polymorphism (generics) with subtyping (for example, OO subclassing) because when this happens you may need to write down explicit variance annotations to appease the type checker.
However, variance still matters even without parametric types. For example, it describes what types you can use when overriding a methof in a subclass. The subclass is allowed to be "more general" than the superclass so if you want you can change the input parameters of the method to a more general supertype and you can change the return type to a more specific subtype. The output types are covariant: in the subclass where you create the method you can use a subclass of the return type. The input types are contravariant: in the subclass where you create the method you use a superclass of the input types.
[1] B. C. Oliveira, A. Moors, and M. Odersky. Type classes as objects and implicits. https://ropas.snu.ac.kr/~bruno/papers/TypeClasses.pdf
[2] O. Kieselyov, Implementing, and Understanding Type Classes. http://okmij.org/ftp/Computation/typeclass.html
https://github.com/functionalflow/brains/projects/9
Over 20 FREE FP books:
https://github.com/functionalflow/brains/tree/master/Zen-of-...
A function has variance because the types of its inputs or outputs are in a hierarchy.
An object type system (or I suppose even a functor system?) with generics might leverage variance to make sure that the behavior of its own methods is consistent with the Substitution Principle (LSP).
And many people will tldr this into variance being the tool to give you a type system that is LSP compatible. But it’s all about the operations, consuming and emitting types.
For example, consider the -> function type constructor. It has two parameters, the input type and the output type. Examples of function types are int->int and bool->bool.
The first parameter of the -> constructor (the type of the input) is contravariant while the second (the type of the output) is covariant.
For another example, consider the type of a generic immutable list, List<T>. The T type parameter of the List constructor is covariant.
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.
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).
Coming from Haskell, what's the elevator pitch for it?
I never knew how amazing "if it compiles, it works" could be when building a UI.
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 can by using an existential type parameter, which 'forgets' the types in much the same way as an upcast.
[exists p. {x:int; p}]
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.
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).
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.
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.
Notice you started your response with a question. You need the right answer to that question before you can meaningfully continue.
There's a reason why so little true world class software (in the sense of beating out the competition with the sheer force of its value to users) is written in Haskell.
If that's "anti-progress", then sign me up I guess.
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.)
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.
GP is talking about trying to measure reading comprehension to see which patterns actually work.
Should we/can we improve upon it is another question.
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.
> 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.
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.
The number of hours I've spent debugging Python/PHP code written by developers who don't understand co-/contra-variance...
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.
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.
Sincere question, what am I getting wrong?
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.
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.
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.
No one actually does this because its a horror show.