12
$\begingroup$

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

$\endgroup$
  • $\begingroup$ I'm not going to be of much help here, but it sounds category theoretic. $\endgroup$ – Anthony Nov 27 '12 at 9:31
8
$\begingroup$

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 cody 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.

$\endgroup$
  • $\begingroup$ 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)$? $\endgroup$ – Andrej Bauer Nov 28 '12 at 15:42
  • $\begingroup$ Ok, found the maps $v$ and $w$ with Coq. $\endgroup$ – Andrej Bauer Nov 28 '12 at 16:14
  • $\begingroup$ 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? $\endgroup$ – Andrej Bauer Nov 28 '12 at 16:23
  • 1
    $\begingroup$ 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. $\endgroup$ – C. A. McCann Nov 28 '12 at 19:31
  • $\begingroup$ In his note:homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/…, 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. $\endgroup$ – cody Nov 29 '12 at 23:21
7
$\begingroup$

The answer can be understood categorically through the lens of F-algebras. 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

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))$.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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? $\endgroup$ – Dominic Mulligan Nov 27 '12 at 10:16
  • 1
    $\begingroup$ 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. $\endgroup$ – Martin Berger Nov 27 '12 at 10:33
  • 1
    $\begingroup$ @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. $\endgroup$ – Neel Krishnaswami Nov 27 '12 at 16:25
  • $\begingroup$ @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. $\endgroup$ – Martin Berger Nov 27 '12 at 16:57
  • $\begingroup$ Bisimulation based characterisations are useful for practical reasoning, because they don't require closure under all contexts. $\endgroup$ – Martin Berger Nov 27 '12 at 17:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.