nLab strong dinatural transformation

Redirected from "strong dinatural transformations".

Contents

Idea

The notion of strong dinatural transformation is a notion of natural transformation between pairs of functors C op×CDC^{op}\times C\to D that is stronger than that of dinatural transformations.

Unlike dinatural transformations, strong dinatural transformations can always be composed. They have close connections to parametricity in computer science.

Definition

Let F,G:C op×CDF,G:C^{op}\times C\to D be functors. A strong dinatural transformation α:FG\alpha :F\to G consists of, for each cCc\in C, a component α c:F(c,c)G(c,c)\alpha_c : F(c,c) \to G(c,c), such that for any morphism f:ccf:c\to c' in CC and any span F(c,c)WF(c,c)F(c',c') \leftarrow W \to F(c,c) in DD, if the square on the left commutes, then the outer hexagon also commutes:

F(c,c) α c G(c,c) F(c,f) G(c,f) W F(c,c) G(c,c) F(f,c) G(f,c) F(c,c) α c G(c,c). \begin{array}{ccccccc} & & F(c,c) & \overset{\alpha_{c}}{\to} & G(c,c)\\ & \nearrow & & \overset{\mathclap{F(c,f)}}{\searrow} & & \overset{\mathclap{G(c,f)}}{\searrow}\\ W & & & & F(c,c') & & G(c,c')\\ & \searrow & & \underset{\mathclap{F(f,c')}}{\nearrow} & & \underset{\mathclap{G(f,c')}}{\nearrow}\\ & & F(c',c') & \underset{\alpha_{c'}}{\to} & G(c',c') \end{array}\,.

If the pullback F(c,c)× F(c,c)F(c,c)F(c,c) \times_{F(c,c')} F(c',c') exists in DD, it suffices to assert this when the square on the left is the defining one of that pullback. On the other hand, if DD has a separator (such as 1Set1\in Set), it suffices to assert this when WW is the separator.

By comparison, a dinatural transformation asserts this condition only when W=F(c,c)W = F(c',c) with the span consisting of F(c,f)F(c',f) and F(f,c)F(f,c).

Connection to relational model

We can regard strong dinatural transformations as a variation on the relational approach to parametric polymorphism, as follows.

If F:C op×CDF:C^{op}\times C\to D and DD has finite limits then for every f:ccf:c\to c' in CC we can regard the pullback F(c,c)× F(c,c)F(c,c)F(c,c) \times_{F(c,c')} F(c',c') as a relation

R F,fF(c,c)×F(c,c). R_{F,f} \subseteq F(c,c) \times F(c',c').

From this point of view, the family {α c:F(c,c)G(c,c)} c\{\alpha_c:F(c,c)\to G(c,c)\}_c is strong dinatural if and only if it preserves these relations, i.e.

(x,y)R F,fimplies(α c(x),α c(y))R G,f. (x,y) \in R_{F,f} \;implies\; \big( \alpha_{c}(x), \alpha_{c'}(y) \big) \in R_{G,f} \,.

As shown by Vene (2006), for a class of types, the usual relational interpretation corresponds to a strong dinaturality interpretation.

However, the strong dinatural transformations don’t form a Cartesian closed category in general (e.g. Uustalu 2010) so might not serve to interpret all types, including function types.

References

Originally introduced (as “strong dinatural transformations”) in Definition 2.7 of:

Further developments:

  • Philip S. Mulry: Strong monads, algebras and fixed points, Applications of Categories in Computer Science 177 (1992) 202–216 [doi:10.1017/CBO9780511525902.012]

  • Robert Paré, Leopoldo Román: Dinatural numbers. Journal of Pure and Applied Algebra 128 1 (1998) 33–92 [doi:10.1016/S0022-4049(97)00036-4]

  • A. Eppendahl, Parametricity and Mulry’s Strong Dinaturality, Department of Computer Science Technical Report No 768, Queen Mary (1999) [pdf, ISSN:1369-1961]

  • Varmo Vene: Parametricity and Strong Dinaturality, talk notes (2006) [pdf, archive:pdf]

  • Jennifer Hackett, Graham Hutton: Programs for cheap!, In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 115–126 [doi:10.1109/LICS.2015.21]

  • Tarmo Uustalu: Strong dinaturality and initial algebras 12th Nordic Wksh. on Programming Theory, NWPT 2 (2000).

  • Tarmo Uustalu: A Note on Strong Dinaturality, Initial Algebras and Uniform Parameterized Fixpoint Operators, In: FICS 2010. 77–82 [pdf, pdf]

Strong dinatural transformations are called paranatural transformations in:

Last revised on July 25, 2024 at 16:58:39. See the history of this page for a list of all contributions to it.