Understanding contravariance
typeclasses.com
typeclasses.com
[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-...
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).
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
{-# 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
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.
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.
bool contains(other) { ... }
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.
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.
Simple 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:
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
func f(x: (<T> (List<T> => List<T>)) => int): int {
return x(list => list.drop(1));
}
func g(y: List<int> => List<int>): int {
return y([1, 2, 3]).sum();
}
func h(z: <T> (T => T)): int {
return z(5);
}
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
f h
f (\ z -> z 5)
(\ z -> z 5) (drop 1)
drop 1 5Well, 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!
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());
}
}
}
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:
pipe :: A -> B
lmap (modifyInput :: A' -> A ) pipe :: A' -> B
rmap (modifyOutput :: B -> B') pipe :: A -> B'
'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
itertools.imap(function_a_to_b, stream_of_as)
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:
generate_b = lambda: function_a_to_b(generate_a())
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)]
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.