2

In typescript intersection types of function, there's a statement:

Contravariance turns things into their dual; If F<T> is contravariant in T, then F<T | U> is equivalent to F<T> & F<U>, and F<T & U> is equivalent to F<T> | F<U>.

I'm confused about how to prove this equivalency.

Playground

type Contra<T> = (arg: T) => any
type T1 = Contra<string> & Contra<number>
type T2 = Contra<string | number>
type T3 = Contra<string> | Contra<number>

declare let f1: T1;
declare let f2: T2;

f1(1); f1('1')
f2(1); f2('1')

f1 = f2;
f2 = f1; // Can't assign f1 to f2

declare let f3: T3;
f3(1) // It's `never` as expected, but how to make sense of it intuitively?
Deerhound
  • 31
  • 4
  • 3
    Please for the love of all that is holy [do not post pictures of code on Stack Overflow](https://meta.stackoverflow.com/questions/285551/why-should-i-not-upload-images-of-code-data-errors). – Jared Smith Dec 12 '22 at 16:28
  • 2
    [Please choose one question](https://meta.stackexchange.com/a/222741/511366) to be your primary question. While both questions are about contravariance, they are not the same question... so they belong in separate posts. Which one do you want to see answered here? – jcalz Dec 12 '22 at 16:40
  • @JaredSmith Thank you for pointing this out. Removed. – Deerhound Dec 13 '22 at 04:57
  • 1
    @jcalz I edited the post with the primary question. I would like to know how to prove this equivalency. – Deerhound Dec 13 '22 at 04:59
  • You want to *prove* the equivalency? That doesn't have much to do with TypeScript per se. You could take the definition of contravariance and that will probably get you halfway (I think you can prove that `F extends F & F` and that `F | F extends F`) but the rest would need some extra assumptions about `F`. Even if you do prove it, it doesn't mean TypeScript would demonstrate it always; TypeScript is not a fully sound or complete language and there are plenty of holes. – jcalz Dec 13 '22 at 16:15
  • @jcalz Yes I want to prove the equivalency. Thank you for the hint! From the definition I figured out `F extends F & F`. For the other direction `F & F extends F`, could you clarify what are the "extra assumptions"? I understand TypeScript is not fully sound, but just curious about the proof. Shall I remove the typescript tag? – Deerhound Dec 14 '22 at 03:57
  • 1
    Ugh I'm not really sure what a minimal assumption would be or how to phrase it. I'd probably handwave something about "symmetry" or "linearity" and point to [some paper or other](https://www.pauldownen.com/publications/interunion.pdf#page=22). The intuition is that function parameters act like complements and therefore turn unions into intersections and vice versa, and also lead to contravariance, but I don't know how to formalize that offhand. – jcalz Dec 14 '22 at 04:53
  • @jcalz Thank you for the hints and paper. That's exactly what I want. Sorry, I admit this question is off-topic for this site. – Deerhound Dec 15 '22 at 08:40

1 Answers1

0

The answer is contained within the question itself:

F<T & U> is equivalent to F<T> | F<U>

which means that

type F1 = ((s: string) => any) | ((n: number) => any);

(sorry I find your helper type a little distracting, YMMV) is equal to

type F2 = (x: string & number) => any;

And now the reason for never is clear: there is no value that can satisfy both string and number, so there can't be a function that accepts a non-existent string-and-number.

More abstractly, I think your understanding of variance is a bit off: covariance and contravariance are about subtype relationships, and how they affect functions on the types.

interface Animal ...;
interface Cat extends Animal ...;

So far so good. But now we have functions that take a parameter, and functions that return a thing:

const getAnimal: () => Animal;
const getCat: () => Cat;

const feedAnimal: ((a: Animal) => void) => void;
const feedCat: (cat: Cat) => void;

feedCat(getAnimal()); // ERROR
feedAnimal(feedCat);  // ERROR

and here we see variance at play with the substitutability of the types: we can pass a Cat to any function that expects an Animal and we can pass a function that returns a Cat to anything that expects () => Animal but crucially you can't do the reverse: the farmer might try to feed the cat grain or return a goat instead of a cat.

Playground

For how that plays out generically I will defer to this explanation by jcalz here:

Contravariance means that F<T> and T contra-vary. That is, F<T> varies counter to (in the opposite direction from) T. In other words, if T extends U, then F<U> extends F<T>

which we see in the example above, albeit with the concrete type and subtype rather than generically: Cat extends Animal so (a: Animal) => any extends (c: Cat) => any, not the other way around. To be fair this seems counter intuitive (or at least it did to me) until one actually sees it walked through with concrete examples in code, as I've tried to do here.

Jared Smith
  • 19,721
  • 5
  • 45
  • 83
  • Thanks Jared. Sorry for being unclear, but my actual question is how do we prove `F is equivalent to F | F` is true. I understand we get `never` if we follow this assumption, but would like a proof. I edited my post again to avoid confusion. – Deerhound Dec 14 '22 at 03:45
  • @Deerhound there's a few different things going on here, so lets be precise: do you want a *formal proof* of the equivalency (in which case this is no longer about TS or even necessarily programming) or do you want Typescript examples showing how that plays out in this particular programming language to give the intuition? One of those questions I can probably answer, the other you'll have to take up with a mathemetician. – Jared Smith Dec 14 '22 at 13:24
  • @kaya3 The [definition](https://www.wikiwand.com/en/Covariance_and_contravariance_(computer_science)#/Formal_definition) of contravariance is A ≤ B, then I ≤ I, but I believe the statement above requires additional proof. See comments above by jcalz. – Deerhound Dec 15 '22 at 08:39
  • @JaredSmith I want a formal proof. Sorry, I admit this is off-topic for this site. – Deerhound Dec 15 '22 at 08:39