What You Needa Know about Yoneda

Transcript

1 What You Needa Know about Yoneda Profunctor Optics and the Yoneda Lemma (Functional Pearl) Department of Computer Science, University of Oxford, UK GUILLAUME BOISSEAU, JEREMY GIBBONS, Department of Computer Science, University of Oxford, UK are a neat and composable representation of bidirectional data accessors, including lenses, Profunctor optics and their dual, prisms. The profunctor representation exploits higher-order functions and higher-kinded type constructor classes, but the relationship between this and the familiar representation in terms of ‘getter’ and ‘setter’ functions is not at all obvious. We derive the profunctor representation from the concrete representation, making the relationship clear. It turns out to be a fairly direct application of the Yoneda Lemma, arguably the most important result in category theory. We hope this derivation aids understanding of the profunctor representation. Conversely, it might also serve to provide some insight into the Yoneda Lemma. • Theory of computation → Program constructs ; Categorical semantics ; Type theory ; CCS Concepts: • Software and its engineering → Abstract data types ; Data types and structures ; Patterns ; Polymor- phism Semantics ; ; Additional Key Words and Phrases: Lens, prism, optic, profunctors, composable references, Yoneda Lemma. ACM Reference Format: Guillaume Boisseau and Jeremy Gibbons. 2018. What You Needa Know about Yoneda: Profunctor Optics and 84 Proc. ACM Program. Lang. the Yoneda Lemma (Functional Pearl). 2, ICFP, Article 84 (September 2018), 27 pages. https://doi.org/10.1145/3236779 1 INTRODUCTION you can tell a lot about a person by the company they keep . Similarly, There is a saying in English that zeg me wie uw vrienden zijn, dan zeg ik wie u bent —“tell me who your friends are, the Dutch say  , constructed from the and I will tell you who you are”; and the Japanese for ‘human being’ is   (‘nin’, meaning ‘person’) and (‘gen’, meaning ‘between’), conveying the idea that two kanji “you as a human being only exist through your relations with others” [Matsumoto 2018]. The sentiment that we are defined by our relationships with others evidently transcends national boundaries. Indeed, it transcends human interaction altogether: one might say that it is the essence of the Yoneda Lemma , which has been called “arguably the most important result in category theory” [Riehl 2016, p57]. The formal statement Yoneda Lemma: For C a locally small category, [ C , S et ] ( C ( A , − ) , F ) ≃ F ( A ) , naturally C in C and F ∈ [ ∈ , S et ] . A of the result is quite formidably terse—we explain it gently in Section 2—but roughly speaking, it says that a certain kind of object (on the right of the isomorphism) is fully determined its relationships (on the left). Authors’ addresses: Guillaume Boisseau, [email protected], Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK; Jeremy Gibbons, [email protected], Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). © 2018 Copyright held by the owner/author(s). 2475-1421/2018/9-ART84 https://doi.org/10.1145/3236779 Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

2 84:2 Guillaume Boisseau and Jeremy Gibbons The high level of abstraction in the statement of the Yoneda Lemma means that it can be applied in many contexts, some of which are actually quite familiar. For example, it explains Cayley’s Theorem for monoids (which is the trick that enables the use of an accumulating parameter, which can often turn a quadratic-time program into a linear-time one), proofs by ‘indirect equality’ (that b a if and only if ∀ c . ( a ⩽ c ) ⇒ ( b ⩽ c ) , an important technique in program calculation), ⩽ is, and the correctness of both closure conversion and translation to continuation-passing style. We discuss these applications in detail in Section 3. More broadly, one might see shadows of Yoneda in the Euclidean axiom that there is nothing more to a geometrical point than the lines that meet there, and in the way that artificial intelligence can attribute its successes to the position that there is nothing more to the ‘semantics’ of an entity than syntactic references to other entities. Mazzola [2002, Chapter 9] identifies a whole Yoneda Philosophy in the arts: understanding a thing through its relationships with other things. Mazzola cites Paul Valéry’s dictum that “c’est l’exécution du poème qui est le poème” [Valéry 1937] (that is, the essence of a poem is determined by its readings, public or private, and not just its text), Theodor Adorno’s statement that “die Idee der Interpretation gehört zur Musik selber und ist ihr nicht akzidentiell” [Adorno 1956] (that is, performance is an essential aspect of a composition’s identity), and the common experience of walking around a sculpture to see it from all angles in order fully to appreciate it. Our goal in this paper is to use the Yoneda Lemma to derive profunctor optics , a surprisingly flexible higher-order datatype-generic representation of data accessors such as lenses and prisms. We define these notions properly in Section 2.3, but summarize briefly here for accessibility. Concretely, a of type Lens S T A B provides access via a ‘getter’ and a ‘setter’ onto a component of type A lens S within a composite product structure of type , allowing that component to be replaced by one of type B , yielding a new composite of type T [Foster et al. 2005; Pickering et al. 2017]: Lens a b s t = Lens { view :: s → data , update :: s × b → t } a The Profunctor class class Profunctor p where dimap :: ( c → a ) → ( b → d ) → p a b → p c d represents ‘transformer’ type constructors P P A B ‘consumes’ , such that a transformer of type values and ‘produces’ B cartesian (also called strong ) profunctor is one that is in addition A values. A coherent with products: Profunctor p ⇒ Cartesian p where class :: p a b → second ( c × a )( c × b ) p Now, a profunctor lens of type LensP A B S T is a mechanism to lift a component-transformer of type P A B to a composite-transformer of type P S T , for any cartesian profunctor P : p s t type ∀ p . Cartesian p ⇒ p a b → = LensP a b s t The somewhat surprising fact is that Lens A B S T and LensP A B S T are naturally isomorphic types. (To be precise, one usually imposes ‘well-behavedness’ or ‘round-tripping’ laws on lenses. These laws appear to be completely orthogonal to the choice of representation, and to the isomorphism, so we do not address them in this paper.) prisms , which provide access onto a component in a composite sum type, There is a dual story for in terms of cocartesian profunctors . Lenses and prisms are particular kinds of optic . The profunctor representation LensP has a number of benefits over the concrete representation Lens [Pickering et al . 2017]. For one thing, the profunctor representation is in terms of ordinary functions, and so profunctor optics compose using ordinary function composition. For a second, the profunctor Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

3 What You Needa Know about Yoneda 84:3 heterogeneous optics, providing access onto components of a sum- representation readily supports of-products composite, which cannot be captured using the concrete representations. We provide a new proof of the equivalence of the concrete and profunctor representations of optics. The proof depends heavily on the Yoneda Lemma. It can be expressed in great generality, applying to lenses, prisms, and other kinds of optic too. It is considerably simpler and more straightforward than previous proofs—both our own [Pickering et al . 2017] and others’ [Milewski 2017b]. The remainder of this paper is structured as follows. In Section 2, we introduce the necessary background in category theory, and more precisely define profunctor optics. Section 3 describes a number of more or less familiar concrete applications of the Yoneda Lemma, in order to provide some intuition for what follows. The main content of the paper is Section 4, presenting our proof using the Yoneda Lemma that profunctor optics are equivalent to their concrete cousins. Section 5 concludes, with a summary, discussion, and thoughts for future work. 2 BACKGROUND 2.1 Notational Conventions We conduct our proofs using categorical notations, for generality, but translate the ideas into a programming language for concreteness. We choose Haskell as that language, but the choice is not particularly important. We do use types as partial specifications; in order to express various abstractions at the type level, one does require generics of higher kind—so Scala would also suffice for this aspect, but Java would not. But static types are not essential, and the ideas would also work in a dynamically typed language. Although we use Haskell as a programming notation, we make some simplifications. We ignore non-termination and partially defined values, treating Haskell types as sets and Haskell programs × B ’ for the Haskell pair type ( A , B ) A A + B ’ for the sum type as total functions. We write ‘ , and ‘ A B . We sometimes subscript methods of a type class, to give a hint as to which instance is Either fmap ’ to indicate the being used; for example, we might write ‘ List instance of fmap . Where in List Haskell one would write ‘ ’ outside a datatype constructor to indicate what is effectively an forall ∃ ’; for example, existential quantification, we actually write ‘ , = a . Boolable data a ∃ a → Bool ) Boolable ( f : We write ‘ ≃ B : g ’ to indicate that f : A → B and g : B → A form an isomorphism. A 2.2 Categorical Prerequisites Categories. A category C consists of: • a collection C | of objects ; | ; a set ( A , B ) of arrows from A to B for each pair of objects A , • ∈ | C | C B • identity arrow id ; ∈ C ( A an A ) for each object A ∈ | C | , A , the composition g ◦ f ∈ C ( A , C ) for each pair of compatible arrows f ∈ C ( A , B ) and g ∈ C ( B , C ) • such that • composition is associative; and • appropriate identity arrows serve as neutral elements for composition. The sets C ( A , B ) are called homsets . (Technically, this is the definition of a locally small category; for cardinality reasons, sometimes the collection of arrows between a pair of objects can be too large to be a set. We gloss over such technicalities.) Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

4 84:4 Guillaume Boisseau and Jeremy Gibbons S et S et ( A , B ) One very familiar example is the category , whose objects are sets, with the homset to consisting of the set of total functions from B A ; we can see the objects and arrows as representa- tions of types and programs, respectively. But we will also draw inspiration (and later illustrations) , ) induces a category P re ( A ⩽ ⩽ ) , whose objects ( , A from two other examples. Any preordered set P re ( A , ⩽ )( a , b ) consisting of a single element when a ⩽ are the elements of A , with the homset b accounts for the identity arrows, and transitivity of for and empty otherwise; reflexivity of ⩽ ⩽ , , , e ) induces a category M M ( M ⊕ ⊕ , e ) , with a single object ∗ , ( composition. And any monoid on on ( M , ⊕ , e )( ∗ and sole homset ∗ ) consisting of the elements of M ; the neutral element e of the M , ⊕ monoid forms the identity arrow, and composition is given by . Indeed, one can see category theory as a kind of common generalization of preorders and monoids. op category C C , with the same objects but reversed arrows: has an Any category opposite op | | are the objects | C C ; • the objects | op op ( A , B ) from A • B the arrows C C are the arrows C ( B , A ) from B to A in C ; to in composition is backwards. • , D , the Given two categories C × D has pairs of objects and pairs of arrows: C product category an object ( A , B ) • C × D | for each pair of objects A ∈ | C | and B ∈ | D | ; ∈ | • D ( g ) ∈ ( C × D )(( A , B ) , ( C , D )) for each pair of arrows f ∈ C ( A , C ) and g ∈ , ( B , D ) ; an arrow f composition is pointwise. • Categories are evidently structured entities, so one should consider the structure- Functors. F : C . Formally, a functor D from preserving mappings between categories, called functors → to category D is a mapping from the objects and arrows of C to those of D , respecting category C the structure: an object F ( A ) ∈ | D | for each object A • C | ; ∈ | • F ( f ) ∈ D ( F ( A ) , F ( B )) for each arrow f ∈ C ( A , B ) , an arrow such that • ( id F ) = id ; | C ∈ | for each object A A ) ( F A F ( g ◦ f ) = F • g ) ◦ F ( f ) for each pair f , g of compatible arrows. ( One class of functors F : S et → S et on S et are the container types ; for example, the functor List : et → S et takes the set A of elements to the set List ( A ) of finite lists of elements drawn S A , and acts on arrows as the ‘map’ operation, taking : A → B to List ( f ) : List ( A ) → List ( B ) . from f : from a category to itself is called an → C F endofunctor .) (A functor C B and objects , B ∈ | C | C C ( A , A ) is a set of arrows; so C ( A , − ) is a For any category , the homset | C | to | S et | , taking object B to set C ( function from , B ) . This function on objects can be extended A to a function on arrows too, taking ∈ C ( B , C ) to ( f ◦ ) ∈ S et ( C ( A , B ) , C ( A , C )) , that is, the function f , that takes C ( A , B ) to f ◦ g ∈ C ( A ∈ C ) . This makes C ( A , − ) a functor from C to S et , called the g homfunctor . Similarly, C ( − , B ) is a functor, taking arrow f to ( ◦ f ) ; but this action on arrows is op contravariant, so this homfunctor is a functor from to S et . C ( P A , ⩽ ) → P re ( B , ⊑ ) correspond to monotonic functions between preordered sets, Functors re ′ on ( M , ⊕ , e ) → M on ( N and functors ⊗ , e M ) correspond to homomorphisms between monoids. , A functor : M on ( M , ⊕ , e ) F S et takes the sole object ∗ to some set S ∈ | S et | and each arrow → m : ∗ → ∗ to a function S → S in a way that respects ⊕ and e , so amounts to a left action of the → monoid M , ⊕ , e ) on S . In particular, the homfunctor M on ( M , ⊕ , e )( ∗ , − ) : M on ( M , ⊕ , e ) ( S et takes → sole object to the set M , and each arrow m : ∗→∗ to the function ( m ⊕− ) : M ∗ M , so it is the e left action of M , ⊕ , ( ) on M itself. It is a worthwhile exercise to verify all of these assertions. Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

5 What You Needa Know about Yoneda 84:5 Functors too are evidently structured entities, so one should consider the Natural Transformations. . Formally, structure-preserving mappings between them, which are called natural transformations , a natural transformation C D between the same two categories C G D → : , given two functors F and . G from F to G φ D , indexed by objects in C : : F is a family of arrows in → ) f F ( / / A ) F ( B F ) ( • ∈ | C | , an arrow φ A ∈ D ( F ( A ) , G ( A )) for each object A φ φ B A     naturality condition satisfying the / / ( A ) ( G B ) G ) f ( G ◦ for each arrow f ∈ C ( A , B ) . ◦ F ( f ) = G ( f ) • φ φ A B et The natural transformations between endofunctors on correspond to polymorphic functions. S . List → For example, reverse is a natural transformation from the list functor to itself; and if : List is the S et functor representing finite node-labelled binary trees of elements, then the function Tree . Tree → inorder List . The naturality that computes the in-order traversal is a natural transformation inorder condition for : A → B over a Tree ( A ) and then traversing states that mapping a function f ( ) : the tree yields the same result as traversing and then mapping over the ensuing List A ◦ Tree ( f ) = List ( inorder ) ◦ inorder f A B → g : P re ( A , ⩽ ) f P re ( B , ⊑ ) —that is, monotonic functions—between two Given two functors , . : f ⊑ preorders, a natural transformation g is a witness to the pointwise ordering f φ g between → the functions, in the sense that φ : f ( a ) ⊑ g ( a ) for each a ∈ A . a ] D , the functor category [ C , D , has as objects the functors from C to D , For any two categories C . C , D ] ( F , and as arrows ) between objects F , G ∈ | [ C , D ] | the natural transformations F [ → G . G The Yoneda Lemma. The Yoneda Lemma states that for (locally small) category C , there is a bijection F A , F , A , S ] ( C ( A , − ) , F ) ≃ F ( A ) : ⌊−⌋ C : [ ⌈−⌉ et A ∈ and functor F ∈ [ C , S et ] . Let us unpack what that says, following Leinster natural in object C , the two free C [2000]. The lemma asserts a bijection between two sets. Apart from category ∈ C and the functor F : variables are the object → S et . In addition to functor F , also appearing A C C ( A , − ) , another functor C → S et . On the left of the bijection is a homset in is the homfunctor . [ , S et ] ; that is, the set of natural transformations φ : C the functor category A , − ) ( → F , namely C . φ : C ( A , B ) ( → F families of functions B ) in S et satisfying an appropriate naturality condition. On B the right is simply the set ( A ) . F The proof of the lemma amounts to constructing the two functions that form the bijection. From . A , F ( left to right, the function : C ⌈−⌉ A , − ) should take a natural transformation → F and yield an φ element of the set F ( A ) . That is achieved by picking the A th component φ of : C ( A , A ) → F ( A ) A the family , and applying this to the identity arrow id φ ∈ C ( A , A ) : A A , F ( = φ ⌈ ⌉ id ) φ A A A , F From right to left, the function should take an element x of the set ⌊−⌋ ( A ) and yield a natural F . ( A , − ) transformation C F . We construct such a natural transformation φ from x as follows. For → object B ∈ | C | , the B th component φ ) should be an arrow in S et —that is, a function—from C ( A , B B ) ( B ) . Given an f ∈ C ( A , B F , we can map f over x using the functorial action of F to yield a value to of the correct type: A , F ⌊ x ⌋ ) ( f ) = F ( f )( x B It is worth noting the essence of this construction: in the ⌈−⌉ direction, there is an ‘application to the identity arrow’, and in the ⌊−⌋ direction, ‘use of the functorial action’. We will see this essence also in the various applications of the Yoneda Lemma in the rest of the paper. Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

6 84:6 Guillaume Boisseau and Jeremy Gibbons g The two naturality conditions amount to the following. Given an arrow A , C ) and a natural ∈ C ( . A , F A , F → , , it does not matter whether one uses the isomorphism : ⌊−⌋ ⌈−⌉ F G ) at φ transformation ( and functor F , then transforms A and F to C and G using g and φ , or one transforms A , F object A C , G C , G and functor ( ⌈−⌉ , using g , ⌊−⌋ , φ then uses the isomorphism ) at object C G G . However, to C we will make no further explicit use of these naturality conditions, so we do not attempt to spell them out in greater detail. A , F x ⌋ really is a natural transformation ⌊ To complete the proof, we would need to show that A , F A , F , that ⌈−⌉ x ∈ F and ⌊−⌋ for any A ) are each other’s inverses, and that the two additional ( naturality conditions hold. The proofs are standard, so we direct the curious reader to the literature [Awodey 2006; Mac Lane 1971]. We present a number of illuminating examples in Section 3. There is a dual version of the Yoneda Lemma, expressed in terms of the other homfunctor − , B ) C ( which is obtained by fixing the target rather than the source object of the homset. This homfunctor op op S et is contravariant, that is, a functor from F : C C → S et . Then Yoneda to ; so we must also have states that op , , S et ] ( C ( − [ C ) , F ) ≃ F ( B ) B (Equivalently, this contravariant version of the Yoneda Lemma is obtained immediately by consid- op C . So this is not a separate result, but an alternative ering the covariant version in the category presentation of the original result.) op ( − , = ) of a category The whole homfunctor is a functor C C × C → S et . Since it is a functor C op C et → [ C , S from a product category, we can curry it; doing so yields a functor ] , sometimes • written ‘ ’. Then we have: H op • The functor C H → [ C , S et ] is full and faithful, and Theorem 2.1 (Yoneda Embedding). : injective on objects. A functor is called faithful when it is injective. The full when it is surjective on each homset, and ‘full and faithful’ part of the theorem is a corollary of Yoneda, obtained by instantiating the functor in the statement of the Yoneda Lemma also to a homfunctor C F B , − ) to yield the equivalence ( C , S et ] ( C ( A [ − ) , C ( B , − )) ≃ C ( B , A ) , A ) − , B ( C , ∈ | = A ⌊ . Indeed, the mapping | C ⌋ B , from right to left takes an arrow f ∈ for all objects C ( B , A ) to C ( f , − ) = ( ◦ f ) , and the Yoneda Lemma proves that this mapping forms an isomorphism. The ‘injective on objects’ part of the theorem is automatic, since by convention distinct homsets of a category are disjoint. 2.3 Profunctor Optics As already summarized briefly in Section 1, a lens provides access onto component within a A B S T Lens of type-varying lenses composite product data structure. The concrete representation :: S consists of a pair of functions: a ‘getter’ A which extracts a view of type A from a source view → S of type update :: S × B → T which inserts an updated view of type B (possibly ; and a ‘setter’ different from A ) into an old source of type S to yield an updated source of type T (correspondingly, possibly different from S ). } data = Lens { view :: s → a , update :: s × b → t Lens a b s t For example, there is an obvious lens onto the second component of a pair: c :: Lens a b ( c × a )( sndLens × b ) sndLens = Lens vw up where Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

7 What You Needa Know about Yoneda 84:7 c vw ) = a , ( a ′ ′ , , a a ) = ( c , c ) ) up a (( up vw The view function extracts the second component, and the update function replaces that component with a new one. provides access onto a component within a composite sum data structure. The prism Dually, a Prism A B S T of type-varying prisms consists of a pair of functions: a concrete representation :: S → T + A which ‘downcasts’ the source of type S to a view of type A , if possible; ‘getter’ match build B → T which ‘upcasts’ an updated view of type B (possibly different from S ) and a ‘setter’ :: T (correspondingly, possibly different from ). When the getter back to an updated source of type S , then the source must inhabit another variant of the sum A cannot downcast the source to type match to the updated source type T . structure, and so it can be directly coerced by Prism a b s t = Prism { match :: s → t + a , build :: b → t } data For example, there is a prism onto an optional value: the ( Maybe a )( Maybe b ) :: Prism a b Prism mt bd = the where Just a ) = Right a mt ( Left Nothing mt Nothing = bd b = Just b The match function mt extracts the optional value when it is present, and yields the complement Nothing ) when it is absent; and the build function bd injects an updated value. (that is, Lenses and prisms turn out to be divergent generalizations of a common specialization, called adapters , which provide access onto a value via a change of representation: Adapter a b s t = Adapter { from :: s → a , to :: b → t } data For example, there is an adapter allowing one to act on a nested pair as if it were a triple: ′ ′ ′ ′ ′ ′ b × c )( a flatten × b :: × c Adapter )(( a × b ) × c )(( a ( × b a ) × c × ) flatten = where Adapter fro to ( (( b ) , c ) = , a , b , c ) fro a ( a , b , c ) = (( a , to ) , c ) b (writing ‘ a × b × c ) ’ for a type of triples). An adapter is equivalent to a lens in which the view ( update function need not be provided with the old completely determines the source, so that the source; and conversely, an adapter is equivalent to a prism in which there is only one variant, so that the match downcast always succeeds. Functor class in Haskell The class Functor f where fmap :: ( a → b ) → f a → f b -- law: fmap g ◦ h ) = fmap g ◦ fmap h ( -- law: fmap id id = F , a value of type represents container types, in the sense that for a functor ‘contains’ elements F A of type A , and so might in principle deliver values of that type. They are analogous to categorical endofunctors on S et . The Profunctor class class where Profunctor p dimap :: ( c → a ) → ( b → d ) → p a b → p c d Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

8 84:8 Guillaume Boisseau and Jeremy Gibbons second 1 P )( 1 × B ) ( 1 P A B A × ′ dimap lunit lunit D × P A B )( D × B ) ( P A second D second second C × D C × D ) × B ) P ( C × ( D × A ))( C × ( D × B )) P (( C × D ) × A )(( C ′ dimap assoc assoc Fig. 1. Cartesian profunctor laws ′ ′ ′ ′ ◦ f )( g ◦ g ( ) = dimap f g ◦ dimap f f g -- law: dimap -- law: = id dimap id id generalizes this to ‘transformer’ types, which may both consume and produce values: for pro- functor P A B ‘consumes’ A values and ‘produces’ B values—note that P , a transformer of type operator which modifies the consumed and produced values is contravariant in the the dimap ‘consumed’ argument. The canonical Profunctor instance is the function type former, for which dimap is obtained simply by function composition: Profunctor ( → ) instance where dimap f g h g ◦ h ◦ f = P (or cartesian A profunctor strong ) if it is coherent with products, in the sense that there is is an operator that, for any type C , lifts a transformer of type P A B to a transformer of second type P ( C × A )( C × B ) that acts on pairs, transforming A s into B s but passing the C s around unchanged, respecting the isomorphisms ′ ( A × B ) × C ≃ A × ( B × C ) : assoc assoc : ′ : 1 A ≃ A : lunit lunit × of products: Profunctor p ⇒ Cartesian p where class :: )( → p ( c × a second c × b ) p a b ′ )) -- law: second h ( second second h dimap assoc assoc = ( D C × D C ′ dimap lunit lunit h -- law: = second h 1 These laws are illustrated by the commutative diagrams in Figure 1. The function type former is an instance: instance ( → ) where Cartesian ( c , a ) second f ( c , f a ) = (Given second , one can construct a symmetric operator first that transforms the first component of a pair.) Dually, a profunctor P is co-cartesian (sometimes called choice ) if it is coherent with the structure of sums ′ : ( A + B ) + C ≃ A + ( B + coassoc ) : coassoc C ′ A + A ≃ : 0 : lzero lzero in the same way: Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

9 What You Needa Know about Yoneda 84:9 right 0 P A )( 0 + B ) P A B 0 ( + ′ dimap lzero lzero P D A )( D + B ) ( + P A B right D right right C + D C + D ) + B ) P ( C P ( D + A ))( C + ( D + B )) (( C + D ) + A )(( C + ′ dimap coassoc coassoc Fig. 2. Cocartesian profunctor laws class Profunctor p ⇒ Cocartesian p where right p a b → p ( c + a )( c + b ) :: ′ -- law: ( right dimap coassoc coassoc ( right h h )) = right C + D C D ′ h dimap lzero lzero right h -- law: = 0 These laws are illustrated by similar commutative diagrams in Figure 2. Again, the function type former is an instance: Cocartesian ( → ) where instance ( = ) right f Left c Left c ( ) = Right ( f a ) right f Right a AdapterP A B S T The profunctor representation of an adapter is as a function lifting a component- transformer P A B to a composite-transformer P S T , that works uniformly for all profunctors P : type AdapterP a b s t = ∀ p . Profunctor p ⇒ p a b → p s t For example, the profunctor representation flattenP flatten is: of the concrete adapter ′ ′ ′ ′ ′ ′ × c )( a :: × b ( × c a )(( a × b ) × c )(( a flattenP × AdapterP × ) × c b ) b flattenP h dimap f t h where = = (( , b ) , f ) a ( a , b , c ) c t ( a , b , c ) = (( a , b ) , c ) which wraps its argument transformer in the two halves of the isomorphism. Similarly, the profunctor representation A B S T of a lens is as a function lifting a component- LensP P A B P S T , that works uniformly for all cartesian profunc- transformer to a composite-transformer tors P : LensP a b s t = ∀ type . Cartesian p ⇒ p a b → p s t p For example, the profunctor representation sndLensP of the concrete lens sndLens is: sndLensP :: LensP a b ( c × a )( c × b ) sndLensP h second h = which is simply an application of the second method. Dually, the profunctor representation PrismP A B S T of a prism is as a function lifting a component- transformer P A B to a composite-transformer P S T , that works uniformly for all co-cartesian profunctors : P type PrismP a b s t = ∀ p . Cocartesian p ⇒ p a b → p s t Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

10 84:10 Guillaume Boisseau and Jeremy Gibbons theP of is: For example, the profunctor representation the PrismP a b theP )( Maybe b ) ( :: Maybe a ( ) where dimap m2s s2m theP h = right h () m2s Nothing = Left Just x ) Right c m2s ( = Left = Nothing ( s2m ()) Right x ) = s2m ( Just x h P A B , we can lift it using right to a transformer of type P (() + A )(() + B ) , Given a transformer :: as required. to adapt this to one of type ( Maybe A )( Maybe B ) P and then use dimap 3 EXAMPLES OF YONEDA The power of the Yoneda Lemma comes from its high level of abstraction; but that also makes it difficult to get to grips with at first. To provide some intuition, in this section we present a number of more or less familiar concrete applications of the Yoneda Lemma and Yoneda Embedding. One way of gaining some intuition for an abstract result in category theory is to consider what it says in the two very special cases of preorder categories re ( A , ⩽ ) , where the homsets are all P either empty or singletons, and monoid categories on ( M , ⊕ , e ) , where there is only a single object; M these are the two simplest kinds of category. As noted in Section 2, one can see category theory as the least common generalization of preorders and monoids. For example, one common route to gaining some intuition for the rather abstract notions of adjunction and monad is through their specialization to preorder categories, where they simplify to the perhaps more familiar Galois connections and to closure operators respectively. 3.1 Indirect Inequality proof by One important technique in the mathematics of program construction is the method of rule of indirect order [Backhouse indirect inequality [Feijen 2001; von Karger 2002], also called the A , ⩽ ) , 2003]: for a preorder ( b ⩽ a ) ⇔ ( ∀ ( . ( a ⩽ c ) ⇒ ( b ⩽ c )) c The right-to-left direction is equivalent to reflexivity of , and the left-to-right direction to transi- ⩽ tivity [Dijkstra 1991]. In some situations, the right-hand side can be much easier to manipulate than the left. This equivalence is an instance of the Yoneda Embedding in the category P re A , ⩽ ) . In this ( category, the homset P re ( A , ⩽ )( b , a ) is a ‘thin set’—a singleton when b ⩽ a , and empty otherwise. The homfunctor P ( A , ⩽ )( a , − ) is a ‘thin function’, taking an element c ∈ A to a singleton set when re . ) and to the empty set otherwise. A natural transformation φ : P a ( A , ⩽ )( a , − c ⩽ → P re ( A , ⩽ )( b , − ) re is a family of functions φ between the thin sets. But the total : P re ( A , ⩽ )( a , c ) → P re ( A , ⩽ )( b , c ) c functions between thin sets and Y are highly constrained—indeed, they are completely deter- X X Y is empty, in which case no such function can exist. So the mined, unless is non-empty and φ of functions is a witness to the fact that for each c , if P re family A , ⩽ )( a , c ) is non-empty then so ( is P re ( A , ⩽ )( b , c ) ; that is, that a ⩽ c implies b ⩽ c . 3.2 Indirect Equality In a similar vein, Yoneda can yield elegant proofs of many equivalences, through the rule of indirect equality [Backhouse 2003; Feijen 2001]. One nice property of full and faithful functors is that they both preserve and reflect isomorphisms . Any functor preserves isomorphisms: Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

11 What You Needa Know about Yoneda 84:11 ( f ◦ F ( g ) = id F ) F ⇔ is a functor ]] [[ ◦ ) ) = F ( id F ( g f ⇐ [[ Leibniz ]] ◦ g = id f and g form an isomorphism, then so do F ( f ) and F ( That is, if ) . When F is faithful (injective on f g F f ) and F ( g ) form an isomorphism, arrows), then the last step is an equivalence; in that case, when ( f and . And when F is full (surjective on arrows), if F ( f ) does have an inverse h , then so too do g is in the range of F —there is a g such that h = F ( g h . Thus, for a full and faithful functor F , the ) arrow forms an isomorphism if and only if F ( f ) does. The Yoneda Embedding provides a full and f faithful functor; therefore we have ( ( B , − ) ≃ C ( A , − )) ⇔ ( A ≃ B ) ⇔ ( C ( − , A ) ≃ C ( − , B )) C U As Leinster [2000, §2.3] writes, if one regards − , A )( U ) = C ( U , A ) as ‘ A viewed from ( ’, then this C states that two objects , B are the same if and only if they look the same from all viewpoints U ; A this is Mazzola’s ‘Yoneda Philosophy’ as discussed in Section 1. ( A , ⩽ ) , this equivalence manifests itself as the rule of indirect equality that forms For a preorder a significant tool in Backhouse’s textbook [Backhouse 2003]: ( b = a ) ⇔ ( ∀ c . ( a ⩽ c ) ⇔ ( b ⩽ c )) For another example, following Awodey [2006, §8.4], the category S currying —a function et supports from a product type is equivalent to a function to an exponential, that is, a function of one argument that yields a function of the other argument: C et × C , B S ≃ S et ( A , B ( ) A ) and the sum type constructor satisfies the universal property that a function from a sum type is equivalent to a pair of functions with a common target: et ( A + B , C ) ≃ S et ( A , C ) × S et ( B , C ) S From these two properties we can calculate: S A + B ) × C (( X ) et , [[ currying ]] ≃ C ( A + B , X S ) et [[ sum ]] ≃ C C ( A , X ( ) × S et S B , X et ) ≃ [[ currying ]] et et × C , X ) × S A ( B × C , X ) S ( ≃ [[ sum ]] S (( A × C ) + ( et × C ) , X ) B and so by the rule of indirect equality we can conclude that ( A + B ) × C ≃ ( A × C ) + ( B × C ) (As an aside for the categorically wise: the only fact about product and exponential that we used C −× C is left adjoint to − ) ; the same calculation works to show that L ( A + B here is that ≃ L A + L B for any left adjoint L . Indeed, it works in any category C , for any colimit in place of + . As a result, we get a proof of the slogan ‘left adjoints preserve colimits’. Dually, right adjoints preserve limits.) Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

12 84:12 Guillaume Boisseau and Jeremy Gibbons 3.3 Cayley’s Theorem − 1 Cayley’s Theorem states that every group , e , ( − ) ( , ) is isomorphic to a group of endomor- ⊕ G : in one direction, each element g G phisms, a subgroup of the symmetric group acting on G ∈ ⊕− is taken ; in the opposite direction, the endomorphism f g is taken to the endomorphism ( ) e ) . Cayley’s Theorem is an instance of the Yoneda Embedding. But groups are f to the element ( not very familiar to functional programmers, so we will illustrate with the slight generalization to ( M , ⊕ , e ) is isomorphic to a monoid of endomorphisms, Cayley’s Theorem for Monoids : every monoid , a submonoid of the ‘full transformation monoid’ of transformation monoid sometimes called a M → . The construction and proof is entirely analogous, except that it M M consisting of all functions omits discussion of the inverse operation of a group. M , ⊕ , e ) Recall that a monoid M on ( M , ⊕ , e ) , with a single object ( can be represented as a category , and with sole homset M on ( M , ⊕ , e )( ∗ , ∗ ∗ consisting of the elements of M , with ⊕ serving as ) • op H composition and : M on ( M , ⊕ , e ) as the identity arrow. The functor → [ M on ( M , ⊕ , e ) , S et ] e ∗ e M on ( M , ⊕ , takes the sole object )( ∗ , − ) , and each arrow m : ∗ → ∗ to the to the homfunctor ( : ⊕− ) function M → M . Then the Yoneda Embedding in this category states that this mapping m m m M is taken to the endomorphism ( is a bijection; again, in one direction, each element ⊕− ) ∈ f (that is, the functorial action of the homfunctor), and in the opposite direction, an endomorphism f ( e is taken to (that is, application to the identity arrow). ) This construction is common in functional programming. It’s the essence of the accumulating parameter technique [Bird 1984], and of ‘the concatenate vanishes’ [Wadler 1987]. For example, Hughes’ ‘novel representation of lists’ [Hughes 1986] amounts to Cayley’s Theorem, substituting the monoid of endomorphisms ( [ A ] → [ A ] , ( ◦ ) , id ) for the monoid of lists ( [ A ] , ++ , [ ] ) , representing each list xs [ A ] by the endomorphism ( xs ++ ) :: [ A ] → [ A ] ; with this data representation, the :: reverse function becomes linear-time. formerly quadratic-time A of Cayley’s Theorem on monoids is essentially ⩽ ) The analogous construction on a preorder , ( a of an ↑ the rule of indirect inequality discussed in Section 3.1. If we define the upwards closure a ∈ A as { c ∈ A | a ⩽ c } element , then indirect inequality can be stated as follows: ( ⩽ a ) ⇔ ( ∀ c . ( c ∈↑ b ) ⇒ ( c ∈↑ b )) a ⇔↑ a ⊆↑ b This gives the representation of the preordered set ( A , ⩽ ) by its upward-closed sets . Thus, a preorder on any kind of carrier is equivalent to one on sets using inclusion, just as a monoid on any kind of carrier is equivalent to one on functions using composition. As Awodey [2006, §8.4] observes, it is often the case that the Yoneda Embedding is into a space with better structural properties, thereby simplifying reasoning. For example, the representation Dedekind Cut , and of a rational number as an upward-closed set under the usual ordering is a this mapping embeds the rationals into the real line, which admits solutions to more equations; a similar phenomenon happens for other instances of the Yoneda Embedding. (Formally, the functor [ C category S et ] has various kinds of limit, even when C does not.) , 3.4 Universal and Existential The Yoneda Lemma can be almost directly rendered into Haskell, via the following type declaration: data Yo f a = Yo { unYo :: ∀ r . ( a → r ) → f r } This declares a container datatype f for every f , with constructor Yo and deconstructor unYo ; Yo the body of a data structure of type Yo f a is a polymorphic function of type ∀ r . ( a → r ) → f r . The Yoneda Lemma states that Yo f a ≃ f a when f is a functor; the two halves of the isomorphism are given by the following two functions: Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

13 What You Needa Know about Yoneda 84:13 :: Yo f a f a fromYo → unYo y id fromYo y = ⇒ → Yo f a :: f a toYo Functor f ( λ h → fmap h x toYo x = Yo ) (Note again the essence: ‘application to the identity arrow’ in one direction, and ‘use of the functorial Yo f a can take an arbitrary function of type a → r , action’ in the other.) Informally, a value of type , and yield a value of type for any ; so it must in some sense have an f a stored inside [Piponi r f r 2006]. is the identity functor Id , we get Yo Id a , which is essentially a function In the special case that f → r ∀ a → r ) . r , the continuation-passing representation of the type a [Hinze and James of type ( b → a 2010; Stay 2008]. Or perhaps more precisely, the CPS transformation of a function of type is a function of type → Yo Id a ; and the correctness of the CPS transformation boils down to this b special case of the Yoneda Lemma. This rendering of the Yoneda Lemma into Haskell uses a universal type quantification. There is a complementary rendering, sometimes called ‘co-Yoneda’, using an existential quantification instead. To discover it, consider the following calculation with types: → f a → ( ∀ r . a a . r ) → g r ) ∀ ( [[ universal property of universal quantification ]] ≃ a . ∀ r . f a ∀ ( a → r ) → g r → ≃ [[ uncurrying ]] a a ∀ r . ( f a ∀ ( . → r )) → g r × ≃ [[ swapping the two quantifiers ]] ∀ r . ∀ a . ( f a × ( a → r )) → g r ≃ [[ universal property of existential quantification ]] → . ∃ a . ( f a × ( r ( r ))) → g r ∀ a Note that in the final step, it is the contravariant position of the function type that is being distributed over the quantifier, so the universal quantification turns into an existential. Let us define a datatype capturing the source type of the final function type above: CoYo f r = ∃ a . CoYo { unCoYo :: f a × ( a → r ) } data f r f a structure abstraction in terms of an Informally, this is an abstract datatype, representing an a , together with a function a → r . for some hidden type Yo ) the type of natural transfor- The first line of the type calculation is (modulo the constructor . . CoYo → Yo g , and now the last line is (again, modulo the constructor) the type mations f f → g ; so provided that f g are functors, we have: and . g f → [[ Yoneda Lemma: g ≃ Yo g for functor g ]] ≃ . → Yo g f ≃ [[ calculation above ]] . CoYo f → g and so, by indirect equality, it follows that f ≃ CoYo f . The components of this isomorphism between the abstraction and the representation CoYo f are as follows: f fromCoYo :: Functor f ⇒ CoYo f b → f b , fromCoYo CoYo ( x ( h )) = fmap h x Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

14 84:14 Guillaume Boisseau and Jeremy Gibbons :: f b CoYo f b toCoYo → CoYo ( , id ) toCoYo y = y CoYo CoYo is—to ‘map’ a function g :: is not a functor, → c over a f f b , it suffices to Even if f b with the function inside: g compose ( CoYo f ) where instance Functor CoYo ( x , h )) = CoYo ( x , g ◦ h ) ( fmap g This is sometimes called ‘the co-Yoneda trick’ [Manzyuk 2013]. It can be used to make a generalized algebraic datatype a functor when the type parameter is used only as an index, so cannot be notation on a GADT representing varied freely; for example, Gibbons [2016] uses it to enable do parameter is already a functor, this change of f monomorphic typed commands. Even when the representation can be an efficiency-improving transformation, because it turns a traversal over x into a simple composition with one function h [Avramenko each of the elements of the payload map fusion rule for free. New [2017] shows that the closure 2017]—that is, it implements the a conversion of a function of type b yields one of type a →∃ e . e × ( e → b ) , the result of which → e . That is, the closure conversion of function type → b is a closure with hidden environment type a → a b ; New describes closure conversion itself as a kind of dual to CPS, both being is CoYo Id applications of the Yoneda Lemma for the identity functor. 3.5 Representable Functors representation of a functor F : C → S et is an object X ∈ | C A together with a natural isomorphism | . C ( X , − ) t → F ; and functor : is called representable if it has such a representation. It is then a F corollary of the Yoneda Lemma that a representation of F is given equivalently by X ∈ | C | and a universal element ps ∈ F ( X ) such that, for any A ∈ | C | and x ∈ F ( A ) , there exists a unique arrow f ∈ ( X , A ) such that F ( f )( ps ) = x . That is, there is a one-to-one correspondence between pairs C ) X ) and pairs ( X , ps t . ( , Naperian functor [Gibbons 2017; This result explains part of the design of Hancock’s notion of Hancock 2005], expressed in Haskell as the type class Functor f ⇒ Naperian f where class Log f type :: f a → ( Log f → a ) -- each other’s. . . lookup -- . . . inverses :: tabulate → a ) → f a ( Log f positions :: f ( Log f ) tabulate h = fmap h positions positions = tabulate id f Log f of ‘positions’, such that The idea here is that a functor is Naperian if there is a type ≃ Log f → a . For example, the functor Pair is Naperian, with Log Pair f a Bool , because there = are two positions in a pair. The two halves of the isomorphism are given by and tabulate . lookup But there is an alternative presentation given instead by and positions , since tabulate and lookup positions are interdefinable; often positions is easier to define, but tabulate more convenient to True use. For pairs, = ( True , False ) and tabulate f = ( f positions , f False ) . The tabulate version corresponds to the presentation in terms of representable functors, and the positions version to that in terms of universal elements. The Yoneda Lemma shows that the two presentations are equivalent. Again, the construction involves ‘application to the identity arrow’ in one direction, and ‘use of the functorial action’ in the other. Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

15 What You Needa Know about Yoneda 84:15 The reader should by now have some intuition as to the structure of instances of the Yoneda Lemma, and in particular of the recurring pattern of ‘application to the identity arrow’ and ‘use of the functorial action’. 4 PROFUNCTOR OPTICS We now exploit the power of the Yoneda Lemma in order to understand the isomorphisms between profunctor optics and their concrete analogues. The key result is the Double Yoneda Embedding, presented in Section 4.1. We apply the Double Yoneda Embedding to adapters in Section 4.2, to lenses in Section 4.3, and to prisms in Section 4.4. The proofs are all very similar; so in Section 4.5 we present an abstraction that covers all three specific cases, and use it in Sections 4.6 and 4.7 to cover more optics. 4.1 Double Yoneda The key insight to understanding the profunctor representation of optics is the following general Double Yoneda Embedding ; the name is ours, but the result is due to result, which we dub the Milewski [2017a,b]. , B ∈ C , we have the following isomor- A For arbitrary Lemma 4.1 (Double Yoneda Embedding). phism: A , B ) ≃ [[ C , S et ] , S et ] ( − ( A ) , − ( B )) C ( and , and respects composition and identity. B A The isomorphism is natural in A ∈ C , the operation of applying a functor F : C → S et to A , denoted − ( A ) , Proof. For an object . C , S et ] to is indeed a functor from et : it maps F ∈ [ C , S et ] to F ( A ) ∈ S et , and φ : F [ → G to φ . S A C states that: Now, the Yoneda Lemma in C X ≃ [ C , S et ] F ) ( X , = ) , F ) ( ( F and X (naturally in − ( X ) is isomorphic to [ C , S et ] ( C ( X , = ) , − ) , naturally ). Therefore the functor in X . Then using the Yoneda Embedding twice, we get the following: [[ C , S et ] , S et ] ( − ( A ) , − ( B )) ≃ [[ as noted above: ( X ) ≃ [ C , S et ] ( C ( X , = ) , − ) ]] − , C S et ] , S et ] ( [ C , S [[ ] ( C ( A , = ) , − ) , [ C , S et ] ( C ( B , = ) , − )) et ≃ [[ Yoneda Embedding in [ C , S et ] ]] [ C , S et ] ( C ( B , = ) , C ( A , = )) ≃ [[ Yoneda Embedding in ]] C ( ) , B C A All the isomorphisms used are natural in the relevant variables, hence the overall isomorphism is A and B . From the proof of the isomorphism we extract one of its components: natural in η : C ( A , B ) → [[ C , S et ] , S et ] ( − ( A ) , − ( B )) ) ( ) f : = F ( f η F Because the index F is a functor, η clearly respects composition and identity; and therefore so too does its inverse. Therefore the isomorphism respects composition and identity. □ For the particular case of Haskell endofunctors S et → S et , this result can be expressed as follows: . ( → b ) ≃∀ f a Functor f ⇒ f a → f b Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

16 84:16 Guillaume Boisseau and Jeremy Gibbons f other than that it is a functor, the only way Informally, this says that if we know nothing about to f a fmap a function a → b : f b to go from is to ⇒ a b ) → ( ∀ f . Functor f → f a → f b ) fromFun :: ( fmap f = fromFun f to f b for any functor and conversely, if we can go from , we can in particular do so for the f a f identity functor: ( ∀ f . Functor f ⇒ f a → f b ) → ( a → :: ) toFun b = ◦ h ◦ Id toFun h unId and moreover that these two transformations are each other’s inverses. Note again the recurring pattern: ‘use of the functorial action’ and ‘application to the identity’ (that is, to the identity functor). 4.2 Adapters We now show that concrete adapters and profunctor adapters are equivalent. The construction in this section is also originally due to Milewski [2017a,b]. Recall the datatype of concrete adapters: Adapter a b s t = Adapter { from :: s → a , to :: b → data } t In categorical language, this corresponds to a pair of arrows ( S , A ) × C ( B , T ) , that is, an arrow C op C C )(( A , B ) , ( S , T × . Adapters with matching types can be composed, and there is an identity ( )) op Adapter id id , in both cases adopting the structure of C × C . We therefore introduce the adapter op da for the category C synonym × C , and think of it as the category whose arrows are adapters. A Likewise, the profunctor representation of adapters was defined as follows: type = ∀ p . Profunctor p ⇒ p a b → p s t AdapterP a b s t op op ( : C P Categorically, a profunctor C → S et . It takes an object is a functor A , B ) in C P × C to × op P ( A , B ) , and an arrow ( C ) × C )(( A , B ) , ( C , D )) (that is, a pair of arrows C ( C , A ) × C ( B , D the set ) to a function P A , B ) → P ( C , D ) in S et . Thus, the action on arrows corresponds precisely to the ( op method of the C dimap × C precisely to the dimap Profunctor type class, and the functor laws on rof C ) to be the laws in the type class. We therefore define the category (over a base category P op C [ functor category , S et ] . × C cor- AdapterP Now, in categorical language, the universal quantification in the definition of responds to a natural transformation. We therefore define the category A daP whose arrows are op ): the objects C A , B ) are those of C profunctor adapters (over a base category × C , as before, but ( the arrows are natural transformations: S (( A , B ) , ( S , T A : = [ P rof , daP et ] ( − ( A , B ) , − ( S , T )) )) op [[ C × = C , S et ] , S et ] ( − ( A , B ) , − ( S , T )) Then the Double Yoneda Embedding states: op op S × C )(( A , B ) , ( S , T )) ≃ [[ C C × C , S et ] , S et ] ( − ( A , B ) , − ( ( , T )) that is, , da (( A , B ) , ( S , T )) ≃ A daP (( A A B ) , ( S , T )) On the left are arrows in A da , which are concrete adapters; on the right are arrows in A daP , which are profunctor adapters; and the Double Yoneda Embedding tells us that these are in one-to-one correspondence (moreover, with nice naturality and functoriality properties). Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

17 What You Needa Know about Yoneda 84:17 4.3 Lenses So much for adapters; what about lenses? Here, we take a different approach from Milewski [2017a,b]. Recall the definition of a concrete lens: = Lens a b s t view :: s → a , update :: s × b → t } { Lens data Translated into categorical language, this again corresponds to a pair of arrows, but now also ens C ), whose objects involving a product. We therefore introduce a category L (over a base category op × C as before, but whose arrows are concrete lenses: C are those of (( A , B ) , ( S , T )) : = C ( S , A ) × C L S × B , T ) ens ( Using the co-Yoneda Lemma, we can derive a more symmetrical characterization of the arrows: S , A ) × C ( S × B , T ) C ( [[ co-Yoneda (see below) ]] ≃ ) , A C ×∃ C . C ( S , C ( × C ( C × B , T ) S ) [[ first component is independent of the quantification ]] ≃ C . C ( S , ∃ ) × C ( S , C ) × C ( C × B , T ) A ≃ [[ universal property of products ]] C C ( S , C × A ) × C ( C × B , T ) ∃ . L ens (( A , B ) , ( S , T )) ≃∃ C . C ( S , C × A ) × C ( Thus × B , T ) . In Haskell, we might write: C data = ∃ c . LensC ( s → c × a , c × b → t ) LensC a b s t S Informally, a source A and its complement C , such that a new view B is factorized into a view C to make a new source T . (But note that this is not the can be combined with the complement constant complement . 2005]: there is encoding of lenses [Bancilhon and Spyratos 1981; Foster et al no requirement that this pair of functions be in any sense inverses.) The first step in the calculation uses the co-Yoneda Lemma from Section 3.4: F ( S ) ≃ ( ∃ C . C ( C , S ) × F ( C )) op but in the opposite category: for functor C F → S et , : op ≃ ≃ ( ∃ C . C ( ( C , S ) × F ( C )) ) ( ∃ C . C ( S , C ) × F ( C )) F S op is C ( −× B , T ) , which is indeed a functor C In the calculation, → S et F . In this symmetric form, it is easier to see that ens does indeed form a category. The identity lens L ′ ) lunit ) is ( lunit on object , , ( , the neutral B , where the complement chosen is the unit type 1 A B A element of product; composition works by taking the product of complements: S → C × ( ) × ( A → D × X ) 7→ ( S → ( C × D ) × X ) A ( C × B → T ) × ( D × Y → B ) 7→ (( C × D ) × Y → T ) Cartesian product forms a monoid only up to isomorphism; but those isomorphisms get quotiented out by the existential quantification, so composition of lenses forms a monoid up to equivalence of values of existential types. The approach we took for adapters in Section 4.2 involved profunctors, which are functors → S et . By analogy, let us investigate functors P : da ens → S et . Such a functor takes an object A L A , B ) of L ens ( P ( A , B ) , and an arrow L ens (( A , B ) , ( S , T )) (that is, a concrete lens) to a function to a set P ( A , B ) → P ( S , T ) in S et . Let us name that action on arrows: , mapLens A B S T . S et ( L ens (( A , B ) , ( S , T )) ∈∀ S et ( P ( A , B ) , P ( S , T ))) Then we calculate with the type of mapLens : Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

18 84:18 Guillaume Boisseau and Jeremy Gibbons A B S T ∀ et ( L ens (( A , B ) , ( S , T )) , S et ( P ( A , B ) , P ( S , T ))) . S L ]] [[ symmetric characterization of arrows in ens ≃ . S et (( ∃ C . C ( S , C × A ) × C ( C × B , T )) , S et ( P ( A , B ) , P ( S , T ∀ A B S T ))) [[ universal property of existential quantification ]] ≃ ) . et ( C ( S , C × A ) × C ( C × B ∀ T S , S et ( P ( A , B ) , P ( S , T ))) A B C S T , op [[ arrows in C × C ]] ≃ op S et (( C A B C S T × C )(( C × A , C × B ) , ( S , T )) , S et ( P ( A , B ) , P ( S , T ))) ∀ . [[ natural transformations in S et as polymorphic functions ]] ≃ op op [ C (( × C , S et ] ∀ C A B C . C )(( C × A , C × B ) , − ) , S et ( P ( A , B ) , P ( − ))) × op C ≃ × C ]] [[ Yoneda Lemma in P A B C S et ( P ( A ∀ B ) , . ( C × A , C × B )) , (To be precise, for these calculations to be valid, the functors mentioned must be functorial in op C × arrows of C and not only in arrows of Lens . For this to hold, we need an identity-on-objects op functor , the details of which will be spelled out in Section 4.5.) : C Lift × C → L ens ens L method of a Cartesian The final type in the calculation above is precisely the type of the second profunctor: Profunctor p Cartesian p where class ⇒ p a b → p ( c × a )( c second b ) :: × mapLens L ens maps respects composition and identity of arrows in Moreover, the property that respects the monoidal structure of products and the unit second precisely onto the property that type (this will be worked out in detail in Section 4.5). That is, Cartesian profunctors are precisely L ens → S et . the functors Profunctor lenses were defined in terms of Cartesian profunctors: type = ∀ p . Cartesian p ⇒ p a b → p s t LensP a b s t As with adapters, the universal quantification corresponds categorically to a natural transformation, ens ( A , B ) and − ( S between the functors T ) from [ L − , S et ] to S et . We therefore define the category , op L ensP , with objects from C × C , and profunctor lenses (natural transformations) as arrows: L ensP (( A , B ) , ( S , T )) : = [[ L ens , S et ] , S et ] ( − ( A , B ) , − ( S , T )) The Double Yoneda Embedding in category L states: ens , ens A , B ) , ( S , T )) ≃ [[ L ens , S L ] (( S et ] ( − ( A , B ) , − ( S , T )) et which immediately shows that L ens (( A , B ) , ( S , T )) ≃ L ensP (( A , B ) , ( S , T )) On the left are arrows in L , which are concrete lenses; on the right are arrows in L ensP , which ens are profunctor lenses; and the Double Yoneda Embedding tells us that these are in one-to-one correspondence (again, with nice naturality properties). 4.4 Prisms Prisms are to sums as lenses are to products; the development is entirely dual. Concrete prisms were defined as follows: data Prism a b s t = Prism { match :: s → t + a , build :: b → t } Categorically, we represent concrete prisms (over a base category ) as arrows in a category P rism , C op × C and whose arrows are pairs of base arrows: whose objects are those of C Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

19 What You Needa Know about Yoneda 84:19 rism (( , B ) , ( S , T )) = C ( S , T + A ) × C ( B , T ) P A Using co-Yoneda again, we can derive an equivalent but more symmetric characterization: ( T + A ) × C ( , , T ) S C B [[ co-Yoneda ]] ≃ . C ( S , C + A ) × C ( C , T ) × C ( ∃ , T ) C B [[ universal property of sum ]] ≃ , . ( S , C + A ) × C ( C ∃ B C T ) C + C S , − ( A ) . Thus, This time, the co-Yoneda Lemma is used covariantly, with the functor being + rism (( A , B ) , ( S , T )) ≃∃ C . C ( S , C + A ) × C ( C + B , T P . Informally, a prism downcasts a source S into ) either a view or its complement C , in such a way that either the complement or a new view B A T . may be upcast to a new source As with lenses, from the monoidal structure of sum we derive a composition operator and identity op C rism P : C Lift × into a category (as well as a functor → P rism ; we postpone that make rism P the details to Section 4.5, where we consider the general case having seen a couple of specific instances). : A functor rism → S et takes objects ( A , B ) to sets P ( A , B ) , and has action on arrows given by: P P ∈∀ A B S T . S et ( P rism (( A , B ) , ( S , T mapPrism , S et ( P ( A , B ) , P ( S , T ))) )) Using Yoneda, we can massage the type of : mapPrism et A B S T S et ( P rism (( A , B ) , ( S , T )) ∀ S . ( P ( A , B ) , P ( S , T ))) , ≃ [[ symmetric characterization of arrows in P rism ]] ∀ A B C S T . S et ( C ( S , C + A ) × C ( C + B , T ) , S et ( P ( A , B ) , P ( S , T ))) op ≃ [[ arrows in × C ]] C op S et (( C A B C S T × C )(( C + A , C + B ) , ( S , T )) , S et ( P ( A , B ) , P ( S , T ))) ∀ . [[ natural transformations in S et as polymorphic functions ]] ≃ op op [ C × × C , S et ] (( C ∀ A B C C )(( . + A , C + B ) , − ) , S et ( P ( A , B ) , P ( − ))) C op C ≃ × C ]] [[ Yoneda Lemma in + A B C S et ( P ( A , B ) ∀ P ( C . A , C + B )) , This is precisely the type of the right method of a co-Cartesian profunctor: class Profunctor p ⇒ Cocartesian p where right :: p a b → p ( c + a )( c + b ) Moreover, the property that mapPrism P rism maps respects composition and identity of arrows in right respects the monoidal structure of sums and the empty type precisely onto the property that rism → (see details in Section 4.5). That is, co-Cartesian profunctors are precisely the functors et . P S Profunctor prisms are defined in terms of co-Cartesian profunctors: PrismP a b s t = ∀ p . type ⇒ p a b → p s t Cocartesian p op rismP , with objects from C P × C , and profunctor prisms (natural transfor- We define the category mations) as arrows: P rismP (( A , B ) , ( S , T )) : = [[ P rism , S et ] , S et ] ( − ( A , B ) , − ( S , T )) The Double Yoneda Embedding in category rism states: P P rism (( A , B ) , ( S , T )) ≃ [[ P rism , S et ] , S et ] ( − ( A , B ) , − ( S , T )) which immediately shows that Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

20 84:20 Guillaume Boisseau and Jeremy Gibbons rism (( , B ) , ( S , T )) ≃ P rismP (( A , B ) , ( S , T )) P A —that is, concrete prisms are equivalent to profunctor prisms. 4.5 Arbitrary Profunctor Optics The proofs in Sections 4.3 and 4.4 both look very similar: they rely on a particular monoidal structure that induces both an associated structure on profunctors and an associated category whose arrows are characterized by existential quantification. We can define those generically as follows. D C with some additional structure, we define the category of profunctors over Given a category D ) as follows: rofOptic P ( ( D )( X , Y ) : = [ D , S et P ( − ( X ) , − ( Y )) rofOptic ] This corresponds to a profunctor optic of type: rofOptic type a b s t = ∀ p . P ∈ D ⇒ p a b → p s t p D shape as a family Σ Define a [ C , C ] that (up to isomorphism) is closed under compo- of functors in sition and contains the identity functor (i.e. is a ‘monoid up to isomorphism’ under composition). Σ , we can define a corresponding concrete existential optic: Given a shape xOptic ) (( A , B ) , ( S , T )) = ∃ F ∈ Σ . C ( S , F ( A )) × C ( F ( B ) , T E Σ a subclass of profunctors that respect the shape: Profunctor p Shaped p where class ⇒ Σ ) :: f ∈ Σ ⇒ p a b → p ( f a )( shape f b Σ and a corresponding profunctor existential optic: type xOpticP = P rofOptic E Σ Shaped Σ (The notation ‘ f ∈ Σ ’ is intended to suggest that the family Σ of functors be thought of as a type constructor class, and f an instance of this class.) The laws imposed on shape are: Σ ≃ shape id Σ Id ◦ shape shape shape ≃ g f ( g ◦ Σ ) Σ Σ f (Those equalities are to be understood modulo appropriate wrapping/unwrapping of constructors). Then we have the following theorem. Profunctor existential optics Theorem 4.2 (Representation theorem for profunctor optics). are isomorphic to concrete existential optics: E xOptic E ≃ xOpticP Σ Σ E xOptic Proof. whose objects are those of As with lenses and prisms, we introduce a category Σ op × C and whose arrows are concrete existential optics: C xOptic (( E A , B ) , ( S , T )) = ∃ F ∈ Σ . C ( S , F ( A )) × C ( F ( B ) , T ) Σ The identity and composition of arrows are inherited from the identity and composition on functors Σ in a similar way as they were for lenses: in id : id E xOptic id = B A B ) ( A , Id ′ ′ ′ ′ ◦ E E to ◦ fro to fro : = E xOptic )) fro ( ( F ( to xOptic ) xOptic to )( fro ◦ F G F F ◦ G op → C × : C Lift Using the identity functor we also build an identity-on-objects functor E xOptic Σ ) E . that takes an arrow from C ( S , A ) × C ( B , T xOptic to C ( S , Id A ) × C ( Id B , T ) Σ Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

21 What You Needa Know about Yoneda 84:21 P : xOptic A functor → Set takes objects ( A , B ) to P ( A , B ) , and has action on arrows given by: E Σ S S et ( E xOptic (( A , B ) , ( S , T )) A B S T . et ( P ( A , B ) , P ( S , T ))) mapExOptic , ∈∀ Σ Σ op By precomposing with Lift , P moreover acquires the structure of a profunctor C Set × C → E xOptic Σ with the same mapping on objects. This allows us to use the Yoneda Lemma to calculate with the mapExOptic : type of Σ . S et ( E xOptic )) (( A , B ) , ( S , T ∀ , A B S T et ( P ( A , B ) , P ( S , T ))) S Σ ≃ [[ arrows in E xOptic ]] Σ A B S T . S et ( ∃ F ∈ Σ . C ( S , F ( ∀ )) × C ( F ( B ) , T ) , S et ( P ( A , B ) , P ( S , T ))) A ≃ [[ universal property of existential quantification ]] , A B S T F ∈ Σ . S et ( C ( S , F ( A )) × C ( F ( B ) , T ) ∀ S et ( P ( A , B ) , P ( S , T ))) . ∀ op C × C ]] [[ arrows in ≃ op ∀ ∀ F ∈ Σ . S et (( C A B S T × C )(( F ( A ) , F ( B )) , ( S , T )) , S et ( P ( A , B ) , P ( S , T ))) . ≃ [[ natural transformations in S et as polymorphic functions ]] op op . ∀ F ∈ Σ . [ C ))) × C , S et ] (( C ∀ × C )(( F ( A ) , F ( B )) , − ) , S et ( P ( A , B ) , P ( − A B op ≃ × C ]] [[ Yoneda Lemma in C ( . ∈ Σ . S et ( P ( A , B ) , P F F ( A ) , F ( B ))) ∀ A B ∀ . shape —the latter type being the type of Σ To work out the correspondence between the functor laws of and the laws of mapExOptic Σ shape , we extract from the proof above the relationship between those two maps. The main step Σ of the proof is the application of the Yoneda Lemma, which gives us an idea of the components of the isomorphism: the Yoneda isomorphism in one direction involves applying to the identity, and the other direction involves mapping an arrow through a functorial action. Formally, and shape Σ mapExOptic are thus related as follows: Σ ) = mapExOptic id shape E ( id xOptic F ( A ) ) F ( B Σ F Σ F to fro ( E xOptic shape mapExOptic ) = dimap to fro ◦ F F Σ Σ mapExOptic The interaction between and composition of arrows is linked with the interaction Σ between and composition of functors: shape Σ ′ ′ xOptic mapExOptic to fro ) ◦ mapExOptic ) ( E xOptic ( to E fro G Σ Σ F mapExOptic shape and = [[ ]] Σ Σ ′ ′ dimap to fro shape ◦ dimap to ◦ fro shape ◦ F G Σ Σ [[ by naturality, shape α ]] ◦ dimap αβ = dimap F ( = ) F ( β ) ◦ shape Σ F F Σ ′ ′ dimap ( F ( to dimap to fro ))( F ( fro ◦ )) ◦ shape shape ◦ F Σ G Σ [[ laws ]] dimap = ′ ′ ( to shape ) ◦ to )( fro ◦ F ( fro dimap )) ◦ shape ( F ◦ F G Σ Σ and ′ ′ E xOptic ) to fro ◦ E xOptic mapExOptic to ( fro Σ G F [[ composition in E = ]] xOptic Σ ′ ′ ( E xOptic fro fro ( ( F ( to mapExOptic ) ◦ to )( ))) ◦ F G ◦ Σ F [[ and shape ]] = mapExOptic Σ Σ ′ ′ ( to dimap ( ◦ to )( fro ◦ F ( fro F )) ◦ shape ) Σ ( F ◦ G ) From this we see that respects composition of functors ( shape ◦ shape ≃ shape shape ) Σ G Σ F Σ ( F ◦ G ) Σ ′ = ◦ respects composition of arrows ( mapExOptic if and only if l mapExOptic mapExOptic l Σ Σ Σ Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

22 84:22 Guillaume Boisseau and Jeremy Gibbons ′ ( ◦ l ) ). A similar correspondence applies with relation to the identity of those mapExOptic l Σ compositions: ) mapExOptic ( E xOptic id shape id id = = mapExOptic B A ( , B ) A Σ Σ Id Σ Id A B shape mapExOptic respects the functor laws. Thus Therefore respects its laws if and only if Σ Σ P : xOptic functors P S et are in one-to-one correspondence with profunctors E ∈ Shaped . Using → Σ Σ the Double Yoneda Embedding, we deduce: xOptic )) (( A , B ) , E S , T )) ≃ E xOpticP T (( A , B ) , ( S , ( Σ Σ as required. □ E xOpticP captures most known profunctor optics. For lenses, the appropriate The general form of Σ Σ . By Cayley’s Theorem, this forms a monoid isomorphic to the : = { ( C ×− ) | C ∈ C } shape is × monoid C , ( × ) , 1 ) . Then, for that particular shape, the type of ( is the same as the type shape Σ × of second from the Cartesian typeclass, and the appropriate laws correspond as well. Thus the profunctors that respect shape Σ are precisely Cartesian profunctors, and profunctor lenses are × isomorphic to E xOpticP . By the representation theorem, we recover the isomorphism between Σ × E ≃ L ens that we derived in Section 4.3. Similarly, prisms are an xOptic profunctor lenses and Σ × Σ } : = { ( C + − ) | C ∈ C instance of this scheme for the shape , and we recover the isomorphism + } Σ = { Id : . from Section 4.4. Finally, adapters correspond to the trivial shape 1 4.6 Traversals and More Equipped with this representation theorem, we can now easily derive the isomorphism between profunctor optics and their concrete analogue for other known optics. For example, a common traversal optic used for container-like values is called Traversable class in the Haskell libraries . The is defined as follows: Functor t ⇒ Traversable t where class traverse :: Applicative f ⇒ ( a → f b ) → t a → f ( t b ) Informally, a finite container type T is traversable when one can iterate over the elements of a , in a fixed order, using an effectful operation of type → F B for some applicative structure A T A functor T B structure [Gibbons and dos Santos Oliveira 2009; McBride F , effectfully yielding a new and Paterson 2008]. The family of traversable functors is a valid shape, since the identity functor is traversable and traversable functors compose. We can therefore define concrete traversals as follows [O’Connor 2014]: raversal = E xOptic T Traversable of profunc- = Shaped Moreover, we immediately get the corresponding subclass Traversing Traversable tors that respect traversable, the associated profunctor optic E xOpticP , and a proof that the Traversing concrete and profunctor representations are isomorphic. This associated profunctor optic appears in profunctor optics libraries such as mezzolens [O’Connor 2015b]. We can also apply the representation theorem to some lesser-known optics, such as grates [O’Connor 2015a]. Concrete grates are defined by the rather un-enlightening type: data Grate a b s t = (( s → a ) → b ) → t O’Connor presents this type alongside an equivalent profunctor encoding, in terms of closed profunctors: data GrateP a b s t = ∀ p . Closed p ⇒ p a b → p s t Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

23 What You Needa Know about Yoneda 84:23 ( C ) for some Closed profunctors are profunctors that can lift through functors of the form →− —that is, through Naperian functors [Hancock 2005], or type representable functors C as discussed in F A F Section 3.5. A Naperian functor contains exactly is a container of fixed shape: a value of type profunctors can lift through Traversable one element for each position of type Traversing . Just as C Closed profunctors can lift through fixed-shape containers: containers, Closed p where class Profunctor p ⇒ c → ( c → a )( p → b ) p a b :: closed 1 →− ) Typical examples of Naperian functors are the identity functor, which is isomorphic to ( , ( →− ) . Naperian functors are also closed under composition, as can and pairs, isomorphic to Bool → ; therefore Naperian D → − ) ≃ ( C × D ) → − C be shown using the currying isomorphism ( . Using the = rofOptic functors form a valid shape, and we have ≃ E xOpticP GrateP P Naperian Closed representation theorem, we can derive a third isomorphic form for grates: E xOptic . Spelling Naperian out its definition, we get: xOptic ) (( A , B E , ( S , T )) = ∃ C . C ( S , C → A ) × C ( C → B , T ) Naperian Using the co-Yoneda lemma, we recover the concrete representation of grates: C C ( S , C → A ) × . ( C → B , T ) ∃ C [[ currying ]] ≃ C . C ( S × C , A ∃ × C ( C → B , T ) ) ≃ [[ currying ]] × C C ( C , S → ∃ ) . C ( C → B , T ) A ≃ [[ co-Yoneda lemma ]] C (( → A ) → B , T ) S [[ arrows in G ]] ≃ rate , (( , B ) , rate S A T )) G ( This existential form comes in useful for deriving properties of grates from properties of Naperian functors. Being of a fixed shape, different containers for the same Naperian functor can be zipped together. For example, three copies of such a container can be assembled into one copy containing triples: :: ( a × a × a → b ) → ( c → a ) zipWith3Naperian ( c → a ) × ( c → a ) → ( c → b ) × zipWith3Naperian op f , g , h ) c = ( ( f c , g c , h c ) op As O’Connor [2015a] explains, a grate can be used to perform a similar zipping. Using the existential encoding, it becomes apparent how this property on Naperian functors is lifted to work with grates: zipWith3Grate :: ( ∃ c . ( s → ( c → a )) × (( c → b ) → t )) → ( a × a × a → b ) → ( s × s × s → t ) = zipWith3Grate , fro ) op to fro ◦ zipWith3Naperian op ◦ map3 to ( where map3 :: ( a → b ) → a × a × a → b × b × b f y map3 f x , y , z ) = ( f x , ( , f z ) 4.7 Composing Profunctor Optics The main advantage of profunctor optics over concrete ones is their compositionality [Pickering et al . 2017]. They are just polymorphic functions, so may be combined using ordinary function composition; and the constraints for different kinds of optic simply conjoin, so even mixed compo- sitions work fine — thus forming a semilattice of those optics. In contrast, concrete optics do not Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

24 84:24 Guillaume Boisseau and Jeremy Gibbons compose nearly so well; in particular, mixed combinations, such as a lens with a prism, are not even expressible. To put it another way, a profunctor adapter is automatically also a profunctor lens and a profunctor , then it is certainly applicable for all Cartesian P prism: if it is applicable for all profunctors profunctors, and for all co-Cartesian ones. Less obviously, a lens is also a traversal, because the ) ) for lenses are instances of Traversable ; and similarly for prisms, because ( C shapes × is also C ( + . Traversable This in particular means that if we compose a lens and a traversal, by subsumption the resulting composition will be a traversal. What happens if we compose a lens and a prism? We know that the resulting optic will be a traversal, but it actually has a more precise type: it is the profunctor optic ( Cartesian ∧ Cocartesian ) for the intersection of the two typeclasses Cartesian P rofOptic Cocartesian and . Such optics are called affine traversals [Grenrus 2017]. We might capture this intersection via the following typeclass: ( Cartesian p , class ) ⇒ AffineTraversing p Cocartesian p This typeclass has just two members, inherited from the parent classes: second p a b → p ( c × a )( c × b ) :: right p a b → p ( c + a )( c + b ) :: This is equivalent to having a sole member: a p a b rightsecond p ( c + d × :: )( c + d × b ) → that respects the relevant monoidal structure (in one direction, compose the two methods; in the other direction, instantiate one of the extra types to be the appropriate neutral element). Following the route taken earlier, we define a category S A A , B ) , ( S , T )) = ∃ C , D . C ( (( , C + D × A ) × C ( C + D × B , T ) ffineTraversal and deduce from the representation theorem that: P rofOptic ( Cartesian ∧ Cocartesian ) ≃ A ffineTraversal When is closed, co-Yoneda implies: C A ffineTraversal (( A , B ) , ( S , T )) ≃ C ( S , T + A × ( B → T )) Such optics manipulate, as expected, structures made from both sums and products. 5 CONCLUSION 5.1 Summary We have presented a new and much simpler proof than any previously published of the correspon- dence between concrete optics (lenses, prisms, traversals, and so on) and their profunctor variants. The proof makes essential use of the Yoneda Lemma and its corollary the Yoneda Embedding; we hope to have inspired the reader to absorb this beautiful and powerful result, and hope also to have provided some intuition and guidance that will facilitate that outcome. 5.2 Related Work The correspondence between concrete and profunctor optics is not new. It was well known to people such as Kmett and O’Connor, who have written optic libraries [Kmett 2018; O’Connor 2015b], and publicly discussed their properties online in blogs and chat channels. A formal presentation of the correspondence was first published by Pickering et al . [2017]; however, their proof made no use of the Yoneda Lemma, and instead went back to first principles in terms of free theorems—and as Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

25 What You Needa Know about Yoneda 84:25 a result, their proofs are more complicated than ours. An online talk and blog post by Milewski [2017a,b] present a proof that does use Yoneda, and in particular introduced the Double Yoneda Embedding (Lemma 4.1), of which we make crucial use. Our presentation follows his as far as profunctor adapters—the construction in Section 4.2 is also originally his—but then we diverge; specifically, Milewski makes use of a somewhat complicated adjunction in order to deal with lenses and prisms, introducing ‘free Tambara modules for a tensor’, whereas we think our approach is much simpler. Matsuda and Wang [2015] present an approach to bidirectional programming in terms of the Yoneda Embedding of concrete (two-parameter) lenses into the higher-order space of functions between lenses. However, they do not make use of the isomorphism in the Yoneda Lemma for equational reasoning with lenses, or for proving equivalence with concrete lenses, reverting again to free theorems. Moreover, they only consider lenses, not prisms and other optics. Jaskelioff and O’Connor [2015] do make thorough use of the equational consequences of Yoneda for reasoning about a class of second-order functions, including some optics under the alternative van Laarhoven representation [van Laarhoven 2009], but they do not address the more convenient profunctor representation. 5.3 Discussion One should note that there are (at least) three different kinds of dual to the Yoneda Lemma, as it was stated formally in Section 1. Duality in one sense arises from currying the homfunctor, and fixing one of the two arguments; the main version we have stated fixes the contravariant argument, leaving a covariant homfunctor. There is also a contravariant version of the Yoneda Lemma, arising from fixing instead the covariant argument; but as discussed in Section 2, this is not a separate result, because it is equivalent to the covariant case in the opposite category. Duality in a second sense arises as in Section 3.4: a straightforward rendering into Haskell of the natural transformations in the statement of the Yoneda Lemma uses a universal quantification, but there is a related presentation using existential quantification. The existential presentation is sometimes called ‘co-Yoneda’ [Manzyuk 2013; New 2017]; but it is essentially a consequence of the same Yoneda Lemma, not a separate result. Duality also arises in a third sense: both the covariant and the contravariant readings of the Yoneda Lemma involve natural transformations a homfunctor from another functor, but one might ask instead about natural transformations to to a homfunctor. This has been discussed in passing by Mac Lane [1971, Exercise III.2.3], attributed by him to Kan and also called ‘co-Yoneda’; this really is a separate result, but it seems much less familiar, and less obviously useful. The reader familiar with the literature on lenses will have noticed that we did not discuss well-behavedness [Foster et al . 2005], sometimes called Put–Get and Get–Put or correctness and hippocraticness [Stevens 2010]: informally, if one puts a view and then immediately retrieves it, one obtains the view that was put (the view was correctly stored), and conversely, if one gets a view from a source and immediately puts it back, the source does not change (no unnecessary harm was done in restoring consistency). In fact, well-behavedness is an orthogonal issue to the profunctor representation: profunctor optics may be well-behaved or ill-behaved, just as concrete optics may [Pickering et al . 2017]. In particular, note that the existential encoding ∃ C . C ( S , C × A ) × C ( C × B , T ) of a concrete lens in Section 4.3 does not imply ‘constant complement’ [Bancilhon and Spyratos . 2005], which would imply well-behavedness: although this encoding entails two 1981; Foster et al functions that relate a source S to a view A and a complement C , it does not follow that these two functions are each other’s inverses, so we do not get hippocraticness. We leave for future work the question of precisely how the correctness properties of lenses and other optics manifest themselves in the profunctor representation. Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

26 84:26 Guillaume Boisseau and Jeremy Gibbons More categorically-inclined readers will have recognized the construction we used to make a category out of a homset with appropriate compositionality properties. Such a homset corresponds rof precisely to a monad in the bicategory of profunctors. A standard property of those monads P is that they can be identified with a category equipped with an identity-on-objects functor [nLab ens , rism , etc., and the associated L contributors 2018]. In our case, the constructed categories are P functors are Lift , Lift , etc. Note that we manipulate two different kinds of profunctors: rism P ens L profunctors over C , which are the ones mentioned explicitly, for which we consider additional op properties such as being Cartesian; and profunctors over C C , which are the homsets and are × P . As such, we do not encounter profunctors that would be both monads and strong, monads in rof as described by Asada [2010]. Further exploration of the links between optics and monads in P rof is left as a topic for future research. ACKNOWLEDGMENTS Profunctor optics were introduced by Edward Kmett, Elliott Hird, Shachaf Ben-Kiki and others in lens and profunctor libraries [Kmett 2015, 2018], and in some blog posts by Russell the Haskell mezzolens O’Connor describing his library [O’Connor 2015b]; that history is documented in our earlier paper [Pickering et al . 2017]. The inspiration for this particular paper came from a talk by Bartosz Milewski [Milewski 2017a,b], and the results in Sections 4.1 and 4.2 are due to him. We are grateful to members of the Algebra of Programming group at Oxford, especially Ohad Kammar and Sam Staton, and to Ichiro Hasuo and Thorsten Wißmann at NII, for helpful comments and discussion; and to Tara Stubbs, for help in tracking down the Valéry quotation. The first author is funded by the UK EPSRC, and the paper was mostly written while the second author was a Visiting Professor at the National Institute of Informatics in Tokyo; we thank both EPSRC and NII for their support. REFERENCES Gesammelte Schriften, Band 16: Musikalische Theodor Adorno. 1956. Fragment über Musik und Sprache. Reprinted in Schriften I–III , Suhrkamp Verlag, 1978, p251–256. Mathematically Structured Functional Programming . ACM. https: Kazuyuki Asada. 2010. Arrows are Strong Monads. In //doi.org/10.1145/1863597.1863607 Yoneda and Coyoneda Trick. (April 2017). Alexey Avramenko. 2017. https://medium.com/@olxc/ yoneda-and-coyoneda-trick-f5a0321aeba4. Category Theory . Oxford University Press. Steve Awodey. 2006. Roland Backhouse. 2003. Program Construction: Calculating Implementations from Specifcations . Wiley. F. Bancilhon and N. Spyratos. 1981. Update Semantics of Relational Views. ACM Trans. Database Syst. 6, 4 (Dec. 1981), 557–575. https://doi.org/10.1145/319628.319634 Richard S. Bird. 1984. The Promotion and Accumulation Strategies in Transformational Programming. ACM Transactions on Programming Languages and Systems 6, 4 (Oct. 1984), 487–504. https://doi.org/10.1145/1780.1781 See also [Bird 1985]. ACM Richard S. Bird. 1985. Addendum to “The Promotion and Accumulation Strategies in Transformational Programming”. 7, 3 (July 1985), 490–492. Transactions on Programming Languages and Systems Edsger W. Dijkstra. 1991. Why Preorders Are Beautiful. (June 1991). EWD1102; available from http://www.cs.utexas.edu/ ~EWD/ewd11xx/EWD1102.PDF. Inform. Process. Lett. 77 (2001), 89–96. https://doi.org/10.1016/ Wim Feijen. 2001. The Joy of Formula Manipulation. S0020-0190(00)00195-2 J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. 2005. Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View Update Problem. In Principles of Programming Languages . ACM Press, 233–246. https://doi.org/10.1145/1040305.1040325 Jeremy Gibbons. 2016. Free Delivery (Functional Pearl). In Haskell Symposium . ACM, 45–50. https://doi.org/10.1145/2976002. 2976005 Jeremy Gibbons. 2017. APLicative Programming with Naperian Functors. In European Symposium on Programming (Lecture Notes in Computer Science) , Hongseok Yang (Ed.), Vol. 10201. Springer Berlin Heidelberg, 556–583. https: //doi.org/10.1007/978-3-662-54434-1_21 Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

27 What You Needa Know about Yoneda 84:27 Journal of Functional Jeremy Gibbons and Bruno César dos Santos Oliveira. 2009. The Essence of the Iterator Pattern. Programming 19, 3,4 (2009), 377–402. https://doi.org/10.1017/S0956796809007291 Oleg Grenrus. 2017. Affine Traversal. http://oleg.fi/gists/posts/2017-03-20-affine-traversal.html Peter Hancock. 2005. What is a Naperian Container? (June 2005). http://sneezy.cs.nott.ac.uk/containers/blog/?p=14. Ralf Hinze and Daniel W. H. James. 2010. Reason Isomorphically!. In , Bruno C. d. S. Oliveira Workshop on Generic Programming and Marcin Zalewski (Eds.). ACM, 85–96. https://doi.org/10.1145/1863495.1863507 R. John Muir Hughes. 1986. A Novel Representation of Lists and Its Application to the Function ‘Reverse’. Inform. Process. Lett. 22 (1986), 141–144. https://doi.org/10.1016/0020-0190(86)90059-1 Journal of Functtional Mauro Jaskelioff and Russell O’Connor. 2015. A Representation Theorem for Second-Order Functionals. Programming 25 (2015). https://doi.org/10.1017/S0956796815000088 Edward Kmett. 2015. profunctor library, Version 5. https://hackage.haskell.org/package/profunctors-5 lens library, Version 4.16. https://hackage.haskell.org/package/lens-4.16 Edward Kmett. 2018. Tom Leinster. 2000. The Yoneda Lemma: What’s It All About? (Oct. 2000). http://www.maths.ed.ac.uk/~tl/categories/ yoneda.ps. Categories for the Working Mathematician Saunders Mac Lane. 1971. . Springer-Verlag. Oleksandr Manzyuk. 2013. Co-Yoneda Lemma. (Jan. 2013). https://oleksandrmanzyuk.wordpress.com/2013/01/18/ co-yoneda-lemma/. Kazutaka Matsuda and Meng Wang. 2015. Applicative Bidirectional Programming with Lenses. In International Conference on Functional Programming , Kathleen Fisher and John H. Reppy (Eds.). ACM, 62–74. https://doi.org/10.1145/2784731.2784750 Shoukei Matsumoto. 2018. I Clean, Therefore I Am. (5th January 2018). https://www.theguardian.com/ The Guardian commentisfree/2018/jan/05/buddhist-monk-cleaning-good-for-you. Guerino Mazzola. 2002. The Topos of Music . Birkhäuser. Conor McBride and Ross Paterson. 2008. Applicative Programming with Effects. Journal of Functional Programming 18, 1 (2008), 1–13. https://doi.org/10.1017/S0956796807006326 Bartosz Milewski. 2017a. Profunctor Optics: The Categorical Approach. https://www.youtube.com/watch?v=l1FCXUi6Vlw. Keynote at conference, Cadiz. Lambda World Bartosz Milewski. 2017b. Profunctor Optics: The Categorical View. (July 2017). https://bartoszmilewski.com/2017/07/07/ profunctor-optics-the-categorical-view/. Closure Conversion as CoYoneda. (Aug. 2017). http://prl.ccs.neu.edu/blog/2017/08/28/ Max New. 2017. closure-conversion-as-coyoneda/. nLab contributors. 2018. monad in nLab. https://ncatlab.org/nlab/revision/monad/72#other_examples [Online; accessed 16-March-2018]. Russell O’Connor. 2014. Mainline Profunctor Hierarchy for Optics. http://r6research.livejournal.com/27476.html Russell O’Connor. 2015a. Grate: A new kind of Optic. https://r6research.livejournal.com/28050.html mezzolens library, Version 0. https://hackage.haskell.org/package/mezzolens-0 Russell O’Connor. 2015b. Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. 2017. Profunctor Optics: Modular Data Accessors. The Art, Science, and Engineering of Programming 1, 2 (2017), Article 7. https://doi.org/10.22152/programming-journal.org/2017/1/7 Dan Piponi. 2006. Reverse Engineering Machines with the Yoneda Lemma. (Nov. 2006). http://blog.sigfpe.com/2006/11/ yoneda-lemma.html. Emily Riehl. 2016. Category Theory in Context . Dover Publications. Available from http://www.math.jhu.edu/~eriehl/ context.pdf . Mike Stay. 2008. The Continuation Passing Transform and the Yoneda Embedding. (Jan. 2008). https://golem.ph.utexas.edu/ category/2008/01/the_continuation_passing_trans.html. Perdita Stevens. 2010. Bidirectional Model Transformations in QVT: Semantic Issues and Open Questions. Software and System Modeling 9, 1 (2010), 7–20. https://doi.org/10.1007/s10270-008-0109-9 Paul Valéry. 1937. Leçon Inaugurale du Cours de Poétique du Collège de France. Reprinted in Variété V , Gallimard, 1944, p295–322. Twan van Laarhoven. 2009. CPS-Based Functional References. (July 2009). http://www.twanvl.nl/blog/haskell/ cps-functional-references Burghard von Karger. 2002. Temporal Algebra. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction (Lecture Notes in Computer Science) , Roland Backhouse, Roy Crole, and Jeremy Gibbons (Eds.), Vol. 2297. Springer-Verlag, 310–386. https://doi.org/10.1007/3-540-47797-7_9 Philip Wadler. 1987. The Concatenate Vanishes. (Dec. 1987). University of Glasgow. Revised November 1989. Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 84. Publication date: September 2018.

Related documents