8
$\begingroup$

It is well known that a set of natural transformations can be expressed as an end:

$$\int_{A \in \mathcal{A}} \mathcal{B}(FA, GA) =_{\operatorname{Set}} \operatorname{Nat}(F, G)$$ This holds for functors $F, G \colon \mathcal{A} \to \mathcal{B}$.

Now in polymorphic lambda calculus (such as System F), there is a very similar phenomenon. Terms satisfy free theorems. As a special case of this, terms of type $\forall A. F A \to G A$ satisfy naturality. Now if we interpret this statement with semantics in $\operatorname{Set}$, it seems like well-typed terms of the above type again correspond to natural transformations from $F$ to $G$!

In Martin-Löf type theory, a similar statement should hold for types of the form $\Pi_{A : \operatorname{Set}} F A \to G A$.

Is there a connection between ends and parametricity? E.g. are ends the semantics of polymorphic types (or $\Pi$-types)?

Bonus: Is there a similar phenomenon for coends? (E.g. $\Sigma$-types or existential quantification?)

$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.