<p>In this context the duality refers to taking the <em>least</em> fixed point in one case and the <em>greatest</em> fixed point in the other. We should try to understand in what sense $L = \forall X . (F(X) \to X) \to X$ and $G = \exists X . (X \to F(X)) \times X$ are the "least" and "greatest" solutions of recursive equation $F(X) \cong X$.</p>

<p>First of all, $L$ and $G$ are indeed fixed points (under certain technical assumptions which restrict the nature of $F$) because the comparison maps $v : F(L) \to L$ and $w : G \to F(G)$ given by
$$v \, x \, X \, g = g \, (F (\lambda h : L \,.\, h \,X\, g)\, x)$$
and
$$w (X, (f, x)) = F (\lambda y : X \,.\, (X, (f, y))) \, (f x)$$
are isomorphisms. Notice that we used the fact that $F$ is a functor, i.e., it is monotone, when we applied it to functions.</p>

<p>Suppose $Y$ is any solution to $F(Y) \cong Y$ with a mediating isomorphism $u : F(Y) \to Y$. Then we have canonical maps $$\alpha : L \to Y \text{  and } \beta : Y\to G$$ defined by
$$\alpha \, f = f\, Y\, u$$
and
$$\beta \, y = (Y, (u^{-1}, y)).$$
Therefore, $L$ is <em>least</em> because we can map from it to any other solution, and $G$ is <em>greatest</em> because we can map from any other solution to it. We could make all this more precise by talking about initial algebras and final coalgebras, but I want my answer to be short and sweet, and cody explained the algebras anyhow.</p>

<p>In practice the least solutions are <em>eager</em> datatypes and the greatest solutions are <em>lazy</em> datatypes. For example, if $F(X) = 1 + A \times X$ then in the first case we get <em>finite</em> lists of $A$'s and in the second finite and infinite lists of $A$'s.</p>

CC BY-SA 3.0
2012-11-28T15:42:28.943Z
My answer is missing proof that $L$ and $G$ are fixed points (under some assumptions about $F$, which may remain unstated). How do I write down the comparison maps $F(L) \to L$ and $G \to F(G)$?
Andrej Bauer
CC BY-SA 3.0
2012-11-28T16:14:06.083Z
Ok, found the maps $v$ and $w$ with Coq.
Andrej Bauer
CC BY-SA 3.0
2012-11-28T16:23:00.267Z
It seems like there is another candidate for $w$, namely $w' (X, (f, x)) = F (\lambda y : X \,.\, (X, (f, x))) \, (f x)$. Can someone explain what is going on?
Andrej Bauer
CC BY-SA 3.0
2012-11-28T19:31:38.837Z
I assume you proved that `w'` is an isomorphism, but does it give you a valid coalgebra? (I'm guessing that it should, but I could be wrong...) Doesn't look like the square would commute.
C. A. McCann
CC BY-SA 3.0
2012-11-29T23:21:32.563Z
In his note:http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt, Wadler gives the first version. He however writes it a bit differently: w(X, (f,x)) = F(unfold X k)(f x). This makes the structure of the coalgebra appear more clearly, and almost immediately gives commutation of the appropriate corecursion morphisms. As camcann says, I think that your other version does not make these squares commute.
cody
CC BY-SA 3.0
2012-11-28T14:55:34.040Z
2012-11-28T16:13:53.120Z
2012-11-28T16:13:53.120Z
Andrej Bauer
<p>The answer can be understood categorically through the lens of <a href="http://en.wikipedia.org/wiki/F-algebra" rel="nofollow noreferrer">F-algebras</a>. The categorical representation of a recursive type $I$ in a category $\cal C$ can roughly be specified using a functor $F:{\cal C}\rightarrow{\cal C}$. One then works in the category of $F$-algebras with</p>

<ul>
<li>as objects: objects $A$ of $\cal C$ along with a morphism
$$ \alpha:F(A)\rightarrow A$$</li>
<li><p>as arrows: squares</p>

<p><img src="https://i.sstatic.net/xlVdX.png" alt="F-algebra morphism"> </p></li>
</ul>

<p>Now for $I$ to be the recursive type represented by $F$, $I$ needs to be <em>initial</em> in this category: we need</p>

<ol>
<li>A morphism $in:F(I) \rightarrow I$</li>
<li>For each $F$-algebra $(A,\alpha)$ a morphism $fold: I\rightarrow A$ that makes the appropriate square commute.</li>
</ol>

<p>Now define $I=\forall X.(F(X)\rightarrow X)\rightarrow X$. It is pretty clear how to build $fold$: just take
$$fold=\lambda i:I. i\ A\ \alpha : I\rightarrow A$$
Building $in$ is a bit more tricky, Wadler explains it, so I won't try to. Note however that it requires the fact that $F$ is a <em>functor</em>, which can be seen as a positivity requirement.</p>

<p>Now in category theory, we often want to consider the situation in which all arrows are reversed. In this case, given $F$, we can consider the category of <em>$F$-coalgebras</em> with</p>

<ul>
<li>As objects: objects $Z$ of $\cal C$ along with a morphism
$$\omega: Z\rightarrow F(Z) $$</li>
<li>As arrows, squares as in the $F$-algebra case (but with $\alpha$ and $\beta$ reversed).</li>
</ul>

<p>Now we wish to examine the <em>terminal</em> object $T$ of this category. The requirements are now reversed:</p>

<ol>
<li>A morphism $out:T\rightarrow F(T)$</li>
<li>For each $F$-coalgebra $Z$, a morphism $cofold: Z\rightarrow T$.</li>
</ol>

<p>How do we do this? Well as Wadler prescribes, we take $T=\exists X.(X\rightarrow F(X))\times X$. In a similar manner than before, we have
$$ cofold = \lambda z:Z.(Z,\omega,z) : Z\rightarrow T$$
This construction would not have worked if we had instead taken $T=\exists X.X\rightarrow (X\rightarrow F(X))$.</p>

CC BY-SA 3.0
2012-11-27T16:47:02.527Z
2012-11-27T16:47:02.527Z
cody
<p>In my experience, a good and operational way to understand duality of types
for $\lambda$-calculi is by going through $\pi$-calculus.</p>

<p>When you translate (decompose) types into process calculus, duality becomes simple: <em>input is dual to output and vice versa</em>. There is not (much) more to duality.</p>

<p>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$.  </p>

<p>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}$.</p>

<p>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 <em>generic forwarder</em>
$$
   x(vw).\overline{w}v
$$
Simplifying a bit, this is essentially the only inhabitant of the type
$\forall X.(X,(X)^{\uparrow})^{\downarrow}$.</p>

<p>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.</p>

<p>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.</p>

<p>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 <a href="http://perso.ens-lyon.fr/olivier.laurent/picppn.pdf" rel="nofollow">4</a>.</p>

<p>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 <a href="http://hal.archives-ouvertes.fr/docs/00/07/54/05/PDF/RR-1154.pdf" rel="nofollow">5</a>, 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.</p>

<p><a href="http://www.sussex.ac.uk/Users/mfb21/publications/lics01/lics01.pdf" rel="nofollow">1</a> N. Yoshida et al., <em><a href="http://www.sussex.ac.uk/Users/mfb21/publications/lics01/lics01.pdf" rel="nofollow">Strong Normalisation in the $\pi$-Calculus</a></em>.</p>

<p><a href="http://www.sussex.ac.uk/Users/mfb21/publications/fossacs03/fossacs03-full.pdf" rel="nofollow">2</a> K. Honda et al., <em><a href="http://www.sussex.ac.uk/Users/mfb21/publications/fossacs03/fossacs03-full.pdf" rel="nofollow">Genericity and the $\pi$-Calculus</a></em>.</p>

<p><a href="http://www.sussex.ac.uk/Users/mfb21/publications/cw04/cw04.pdf" rel="nofollow">3</a> K. Honda et al., <em><a href="http://www.sussex.ac.uk/Users/mfb21/publications/cw04/cw04.pdf" rel="nofollow">Control in the $\pi$-Calculus</a></em>.</p>

<p><a href="http://perso.ens-lyon.fr/olivier.laurent/picppn.pdf" rel="nofollow">4</a> K. Honda et al., <em><a href="http://perso.ens-lyon.fr/olivier.laurent/picppn.pdf" rel="nofollow">An exact correspondence between a typed pi-calculus and polarised proof-nets</a></em>.</p>

<p><a href="http://hal.archives-ouvertes.fr/docs/00/07/54/05/PDF/RR-1154.pdf" rel="nofollow">5</a> R. Milner, <em><a href="http://hal.archives-ouvertes.fr/docs/00/07/54/05/PDF/RR-1154.pdf" rel="nofollow">Functions as Processes</a></em>.</p>

CC BY-SA 3.0
2012-11-27T10:16:29.080Z
re: Your point about the number of inhabitants of type ∀X.(X,(X)↑)↓.
Is there an analogue of "free theorems" then for the pi-calculus?  If so, where is this discussed?
Dominic Mulligan
CC BY-SA 3.0
2012-11-27T10:33:46.183Z
Hello @DominicMulligan, yes there are "free theorems" and we investigated this a bit in [1, 2]. I think a lot more could be said in this direction.
Martin Berger
CC BY-SA 3.0
2012-11-27T16:25:37.330Z
@MartinBerger: Can you use parametricity to figure out what the "right" notion of process equivalence for typed pi-calculus is? E.g., in System F the parametric logical relation corresponds to contextual equivalence. By analogy, I would expect whatever notion of process equivalence corresponds to the parametric logical relation for pi-calculus to be especially interesting.
Neel Krishnaswami
CC BY-SA 3.0
2012-11-27T16:57:19.477Z
@NeelKrishnaswami: Yes, that's an interesting question. We investigated this in [2] for the pi-calculus embedding System F fully abstractly and used the results in the full abstraction proof (e.g. a typed bisimulation characterisation).

I don't think this has been explored more generally. For a start there are infinitely many typed $\pi$-calculi. And as we move away from nice, deterministic typed fragments, it's probably going to get harder. Almost all concurrent type-theory so far is for deterministic fragments. It would be fascinating to attempt far-reaching generalisations.
Martin Berger
CC BY-SA 3.0
2012-11-27T17:00:35.107Z
Bisimulation based characterisations are useful for practical reasoning, because they don't require closure under all contexts.
Martin Berger
CC BY-SA 3.0
2012-11-28T15:00:44.540Z
This is all very nice and cool, but perhaps not the best first explanation of what is going on.
Andrej Bauer
CC BY-SA 3.0
2012-11-28T17:58:33.660Z
@AndrejBauer I guess that depends on your background. For a programmer with strong operational intuitions, process calculus is probably much easier to grasp than category theory. For a mathematician with a strong background in modern algebra, it's probably the other way around. There is another advantage to the process theoretic approach: it does not seem to fall apart when you leave the cozy world of pure functions.
Martin Berger
CC BY-SA 3.0
2012-11-28T18:00:29.387Z
Dualisation means output turns into input and vice versa. What could be simpler?
Martin Berger
CC BY-SA 3.0
2012-11-29T06:24:09.923Z
Dualization can mean many things. In any case, it is good to have several anwsers, each offering a slightly different view.
Andrej Bauer
CC BY-SA 3.0
2012-11-29T13:46:19.747Z
@AndrejBauer I agree that multiple perspective are good because mutually enriching. But I expect that all type-theoretic duality can be explained and unified as abstraction of input/output duality. I would be interested in counterexamples.
Martin Berger
CC BY-SA 3.0
2012-11-29T15:01:38.873Z
Here is a challenge: the duality between compuations and values, as exemplified by adjunctions and the call-by-push-value semantics of languages. No trace of input/output there, if you ask me.
Andrej Bauer
CC BY-SA 3.0
2012-11-29T16:30:44.863Z
@AndrejBauer In what sense is that a duality? Have you got a reference for this handy?
Martin Berger
CC BY-SA 3.0
2012-11-30T03:06:42.960Z
It is a duality because it is an adjunction, and adjunctions are a form of duality. I suppose on a tighter reading of duality it would not count as one. We're in the land of opinions anyhow.
Andrej Bauer
CC BY-SA 3.0
2012-11-30T11:32:24.750Z
@AndrejBauer I don't remember CBPV in detail, but [Paul's FAQ](http://www.cs.bham.ac.uk/~pbl/cbpv.html) suggests it's closed to polarised linear logic and game semantics, which leads me to conjecture that the duality you mention can be recovered using types as outlined in my post. Note in particular the extremely precise correspondence between polarised linear logic and typed pi-calculus, see [4] for details.
Martin Berger
CC BY-SA 3.0
2012-11-27T09:35:28.883Z
2012-11-28T18:03:01.867Z
2012-11-28T18:03:01.867Z
Martin Berger
<p>In Wadler's <em>Recursive Types for Free!</em> [1], he demonstrated two types, $\forall X . (F(X) \rightarrow X) \rightarrow X$ and $\exists X . (X \rightarrow F(X)) \times X$, and claimed they are <em>dual</em>.  In particular, he pointed out that the type $\exists X . X \rightarrow (X \rightarrow F(X))$ is <em>not</em> the dual of the former.  It seems the duality in question here is different from De Morgan duality in logic.  I wonder how the duality of types is defined, specfically for the three types mentioned, why the second is dual of the first while the third is not.  Thanks.</p>

<p>[1] <a href="http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt">http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt</a></p>

CC BY-SA 3.0
2012-11-27T09:31:04.400Z
I'm not going to be of much help here, but it sounds category theoretic.
Anthony
<lo.logic><type-theory>
How is duality of types defined?
day
# How is duality of types defined?

(Asked by: username_0 on 2012-11-26)

In Wadler's *Recursive Types for Free!* [1], he demonstrated two types, $\forall X . (F(X) \rightarrow X) \rightarrow X$ and $\exists X . (X \rightarrow F(X)) \times X$, and claimed they are *dual*. In particular, he pointed out that the type $\exists X . X \rightarrow (X \rightarrow F(X))$ is *not* the dual of the former. It seems the duality in question here is different from De Morgan duality in logic. I wonder how the duality of types is defined, specfically for the three types mentioned, why the second is dual of the first while the third is not. Thanks.

[1] <http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt>

**Tags:** lo.logic, type-theory

> **Comments:**
> **username_1**: I'm not going to be of much help here, but it sounds category theoretic.  

---

## 3 answers

### Answer by username_2 on 2012-11-28. Score: 8

In this context the duality refers to taking the *least* fixed point in one case and the *greatest* fixed point in the other. We should try to understand in what sense $L = \forall X . (F(X) \to X) \to X$ and $G = \exists X . (X \to F(X)) \times X$ are the "least" and "greatest" solutions of recursive equation $F(X) \cong X$.

First of all, $L$ and $G$ are indeed fixed points (under certain technical assumptions which restrict the nature of $F$) because the comparison maps $v : F(L) \to L$ and $w : G \to F(G)$ given by
$$v \, x \, X \, g = g \, (F (\lambda h : L \,.\, h \,X\, g)\, x)$$
and
$$w (X, (f, x)) = F (\lambda y : X \,.\, (X, (f, y))) \, (f x)$$
are isomorphisms. Notice that we used the fact that $F$ is a functor, i.e., it is monotone, when we applied it to functions.

Suppose $Y$ is any solution to $F(Y) \cong Y$ with a mediating isomorphism $u : F(Y) \to Y$. Then we have canonical maps $$\alpha : L \to Y \text{ and } \beta : Y\to G$$ defined by
$$\alpha \, f = f\, Y\, u$$
and
$$\beta \, y = (Y, (u^{-1}, y)).$$
Therefore, $L$ is *least* because we can map from it to any other solution, and $G$ is *greatest* because we can map from any other solution to it. We could make all this more precise by talking about initial algebras and final coalgebras, but I want my answer to be short and sweet, and username_4 explained the algebras anyhow.

In practice the least solutions are *eager* datatypes and the greatest solutions are *lazy* datatypes. For example, if $F(X) = 1 + A \times X$ then in the first case we get *finite* lists of $A$'s and in the second finite and infinite lists of $A$'s.

> **Comments:**
> **username_2**: My answer is missing proof that $L$ and $G$ are fixed points (under some assumptions about $F$, which may remain unstated). How do I write down the comparison maps $F(L) \to L$ and $G \to F(G)$?  
> **username_2**: Ok, found the maps $v$ and $w$ with Coq.  
> **username_2**: It seems like there is another candidate for $w$, namely $w' (X, (f, x)) = F (\lambda y : X \,.\, (X, (f, x))) \, (f x)$. Can someone explain what is going on?  
> **username_3**: I assume you proved that `w'` is an isomorphism, but does it give you a valid coalgebra? (I'm guessing that it should, but I could be wrong...) Doesn't look like the square would commute.  
> **username_4**: In his note:http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt, Wadler gives the first version. He however writes it a bit differently: w(X, (f,x)) = F(unfold X k)(f x). This makes the structure of the coalgebra appear more clearly, and almost immediately gives commutation of the appropriate corecursion morphisms. As camcann says, I think that your other version does not make these squares commute.  

---

### Answer by username_4 on 2012-11-27. Score: 7

The answer can be understood categorically through the lens of [F-algebras](http://en.wikipedia.org/wiki/F-algebra). The categorical representation of a recursive type $I$ in a category $\cal C$ can roughly be specified using a functor $F:{\cal C}\rightarrow{\cal C}$. One then works in the category of $F$-algebras with

* as objects: objects $A$ of $\cal C$ along with a morphism
  $$ \alpha:F(A)\rightarrow A$$
* as arrows: squares

  ![F-algebra morphism](https://i.sstatic.net/xlVdX.png)

Now for $I$ to be the recursive type represented by $F$, $I$ needs to be *initial* in this category: we need

1. A morphism $in:F(I) \rightarrow I$
2. For each $F$-algebra $(A,\alpha)$ a morphism $fold: I\rightarrow A$ that makes the appropriate square commute.

Now define $I=\forall X.(F(X)\rightarrow X)\rightarrow X$. It is pretty clear how to build $fold$: just take
$$fold=\lambda i:I. i\ A\ \alpha : I\rightarrow A$$
Building $in$ is a bit more tricky, Wadler explains it, so I won't try to. Note however that it requires the fact that $F$ is a *functor*, which can be seen as a positivity requirement.

Now in category theory, we often want to consider the situation in which all arrows are reversed. In this case, given $F$, we can consider the category of *$F$-coalgebras* with

* As objects: objects $Z$ of $\cal C$ along with a morphism
  $$\omega: Z\rightarrow F(Z) $$
* As arrows, squares as in the $F$-algebra case (but with $\alpha$ and $\beta$ reversed).

Now we wish to examine the *terminal* object $T$ of this category. The requirements are now reversed:

1. A morphism $out:T\rightarrow F(T)$
2. For each $F$-coalgebra $Z$, a morphism $cofold: Z\rightarrow T$.

How do we do this? Well as Wadler prescribes, we take $T=\exists X.(X\rightarrow F(X))\times X$. In a similar manner than before, we have
$$ cofold = \lambda z:Z.(Z,\omega,z) : Z\rightarrow T$$
This construction would not have worked if we had instead taken $T=\exists X.X\rightarrow (X\rightarrow F(X))$.


---

### Answer by username_5 on 2012-11-27. Score: 6

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](http://perso.ens-lyon.fr/olivier.laurent/picppn.pdf).

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](http://hal.archives-ouvertes.fr/docs/00/07/54/05/PDF/RR-1154.pdf), 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](http://www.sussex.ac.uk/Users/mfb21/publications/lics01/lics01.pdf) N. Yoshida et al., *[Strong Normalisation in the $\pi$-Calculus](http://www.sussex.ac.uk/Users/mfb21/publications/lics01/lics01.pdf)*.

[2](http://www.sussex.ac.uk/Users/mfb21/publications/fossacs03/fossacs03-full.pdf) K. Honda et al., *[Genericity and the $\pi$-Calculus](http://www.sussex.ac.uk/Users/mfb21/publications/fossacs03/fossacs03-full.pdf)*.

[3](http://www.sussex.ac.uk/Users/mfb21/publications/cw04/cw04.pdf) K. Honda et al., *[Control in the $\pi$-Calculus](http://www.sussex.ac.uk/Users/mfb21/publications/cw04/cw04.pdf)*.

[4](http://perso.ens-lyon.fr/olivier.laurent/picppn.pdf) K. Honda et al., *[An exact correspondence between a typed pi-calculus and polarised proof-nets](http://perso.ens-lyon.fr/olivier.laurent/picppn.pdf)*.

[5](http://hal.archives-ouvertes.fr/docs/00/07/54/05/PDF/RR-1154.pdf) R. Milner, *[Functions as Processes](http://hal.archives-ouvertes.fr/docs/00/07/54/05/PDF/RR-1154.pdf)*.

> **Comments:**
> **username_6**: re: Your point about the number of inhabitants of type ∀X.(X,(X)↑)↓. Is there an analogue of "free theorems" then for the pi-calculus?  If so, where is this discussed?  
> **username_5**: Hello @DominicMulligan, yes there are "free theorems" and we investigated this a bit in [1, 2]. I think a lot more could be said in this direction.  
> **username_7**: @MartinBerger: Can you use parametricity to figure out what the "right" notion of process equivalence for typed pi-calculus is? E.g., in System F the parametric logical relation corresponds to contextual equivalence. By analogy, I would expect whatever notion of process equivalence corresponds to the parametric logical relation for pi-calculus to be especially interesting.  
> **username_5**: @NeelKrishnaswami: Yes, that's an interesting question. We investigated this in [2] for the pi-calculus embedding System F fully abstractly and used the results in the full abstraction proof (e.g. a typed bisimulation characterisation).  I don't think this has been explored more generally. For a start there are infinitely many typed $\pi$-calculi. And as we move away from nice, deterministic typed fragments, it's probably going to get harder. Almost all concurrent type-theory so far is for deterministic fragments. It would be fascinating to attempt far-reaching generalisations.  
> **username_5**: Bisimulation based characterisations are useful for practical reasoning, because they don't require closure under all contexts.  
> **username_2**: This is all very nice and cool, but perhaps not the best first explanation of what is going on.  
> **username_5**: @AndrejBauer I guess that depends on your background. For a programmer with strong operational intuitions, process calculus is probably much easier to grasp than category theory. For a mathematician with a strong background in modern algebra, it's probably the other way around. There is another advantage to the process theoretic approach: it does not seem to fall apart when you leave the cozy world of pure functions.  
> **username_5**: Dualisation means output turns into input and vice versa. What could be simpler?  
> **username_2**: Dualization can mean many things. In any case, it is good to have several anwsers, each offering a slightly different view.  
> **username_5**: @AndrejBauer I agree that multiple perspective are good because mutually enriching. But I expect that all type-theoretic duality can be explained and unified as abstraction of input/output duality. I would be interested in counterexamples.  
> **username_2**: Here is a challenge: the duality between compuations and values, as exemplified by adjunctions and the call-by-push-value semantics of languages. No trace of input/output there, if you ask me.  
> **username_5**: @AndrejBauer In what sense is that a duality? Have you got a reference for this handy?  
> **username_2**: It is a duality because it is an adjunction, and adjunctions are a form of duality. I suppose on a tighter reading of duality it would not count as one. We're in the land of opinions anyhow.  
> **username_5**: @AndrejBauer I don't remember CBPV in detail, but [Paul's FAQ](http://www.cs.bham.ac.uk/~pbl/cbpv.html) suggests it's closed to polarised linear logic and game semantics, which leads me to conjecture that the duality you mention can be recovered using types as outlined in my post. Note in particular the extremely precise correspondence between polarised linear logic and typed pi-calculus, see [4] for details.  

---

