In my experience, a good and operational way to understand duality of types
for $\lambda$-calculi is by going through $\pi$-calculus.
When you translate (decompose) types into process calculus, duality becomes simple: input is dual to output and vice versa. There is not (much) more to duality.
In $\pi$-calculus you have a straightforward (and almost symmetric)
duality between input and output. Say you have a type $\alpha = (Bool,
Int)^{\uparrow}$. Then $\alpha$ says that a channel having type $\alpha$ makes exactly one
output, carrying a boolean value and an integer. A process inhabiting
this type at channel $x$ would be $\overline{x}\langle
false,7\rangle$. The dual type, which we might write
$\overline{\alpha}$, would express that an input happens
of a pair $(v, w)$ where $v$ is a boolean and $w$ is an integer. We
write $\overline{\alpha}$ as $(bool,int)^{\downarrow}$. A process
inhabiting $\overline{\alpha}$ at $x$ would be $c(v,w).0$.
Naturally,
processes don't just communicate simple integer or boolean values, but
also channels. For example the type $\beta = (int,
(int)^{\uparrow})^{\downarrow}$ describes a channel that makes one
input of two values $(v, w)$ where $v$ is an integer and $w$ is a
channel that is used to make exactly one output (of an
integer). Clearly its dual must be $\overline{\beta} =(int,
(int)^{\downarrow})^{\uparrow}$, which describes a channel that
outputs two pieces of data, an integer and a channel used to input an
integer. The duality of $\alpha$ and $\overline{\alpha}$ means that we
can coherently parallel compose a process $P$ that has type $\alpha$
at a channel name $x$ with a process $Q$ that has type
$\overline{\alpha}$ at the same $x$ (assuming that the other shared
channels of $P$ and $Q$ are also dual). And likewise for $\beta$ and its dual $\overline{\beta}$.
This can easily be generalised to higher-order types, for example
$\forall X.(X,(X)^{\uparrow})^{\downarrow}$ is a type that inputs two
items $(v, w)$ where $v$ is of type $X$ and $w$ is a channel used for
outputting something of type $X$. An example of a process having this type
at a channel $x$ is the generic forwarder
$$
x(vw).\overline{w}v
$$
Simplifying a bit, this is essentially the only inhabitant of the type
$\forall X.(X,(X)^{\uparrow})^{\downarrow}$.
What does the universal quantification mean at the process level?
There is a straightforward interpretation: if data is typed by a
type-variable, it cannot be used as the subject of an output, only an
object. So we cannot inspect this data, we can only pass it on, or
forget it.
The type $\forall X.(X,(X)^{\uparrow})^{\downarrow}$ is dual to
$\exists X.(X,(X)^{\downarrow})^{\uparrow}$. How are we to interpret
the existential quantification? Quite simple: if data is typed by an
existentially quantified type variable, it can only be passed to
processes that do not inspect the data, but only pass it on (or forget
it). In other words, we can only pass it on to processes that use the
dual universally quantified type variable.
The theory of this has been worked out in some detail in [1, 2, 3] and
some other, harder to access work, and related very precisely to
polarised linear logic and its notion of duality in 4.
Now you many ask how this relates to type in $\lambda$-calculi. The
answer is that $\lambda$-calculi can be decomposed into $\pi$-calculus
in a precise way, following pioneering work by R. Milner 5, and each
$\lambda$-calculus type has a precise correspondence with
$\pi$-calculus types. The duality at the process type level translates back to
duality at the function type level. It's just that function application is less of a symmetric operation, and the simplicity of the duality at the process level is
hidden in the complications of $\lambda$-calculus.
1 N. Yoshida et al., Strong Normalisation in the $\pi$-Calculus.
2 K. Honda et al., Genericity and the $\pi$-Calculus.
3 K. Honda et al., Control in the $\pi$-Calculus.
4 K. Honda et al., An exact correspondence between a typed pi-calculus and polarised proof-nets.
5 R. Milner, Functions as Processes.
