Let's say I define a type `x : A`. This means that subsequently we can feel as though we "have" an `A` called `x`. Let's say I define a type `f : A -> B`. This

Let's say I define a type `x : A`. This means that subsequently we can feel as though we "have" an `A` called `x`. Let's say I define a type `f : A -> B`. This means that subsequently we can feel as though we "have" a `B` so long as we can somehow provide an `A`. If that `A` is called `x` then our `B` is called `f x`. These are both normal concepts but I talk about them to emphasize a notion of "debt" and "ownership". Normal values are things we own and functions are things which allow us to trade that which we own for something new [0]. Another situation is available in continuation semantics where I have `k : {A}` which can be read as "a hole demanding an `A`". This means that subsequently, in order to move forward, I must "pay" an `A`. `k` is a "black hole" which consumes `A`s. Somehow, functions represent things like both `x` and `k`, a value we would have once we satisfy a debt. Ultimately, this is the source of covariance and contravariance. A covariant kind of thing is one that we have. A contravariant kind of thing is one that we owe. To wit, if I "have" a list of `A`s, `xs : [A]` then I "have" some number of `A`s. On the other hand, if I have a `Relation A` data Relation a = Relation (a -> a -> Bool) then I "owe" some `A`s (in order to receive a Bool). Finally, my "black hole" example above can be read as saying that if I "have" a black hole like `{A}` then I "owe" and `A`. This means that `[]` is covariant, while `Relation` and `{}` are contravariant. They indicate a notion of debt. Ultimately, the clearest way to express this idea of data types which have ownership or existence properties is the mapping properties of `Functor` and `Contravariant` (in Haskell terms anyway) instance Functor f where fmap :: (a -> b) -> (f a -> f b) instance Contravariant f where cmap :: (b -> a) -> (f a -> f b) But "owe" and "have" can go a long way as intuition. [0] This is all even more emphasized in linear logics.