Tambara

Presents the unified definition of optic and generalized Tambara modules. This definition has been studied by Milewski ("Profunctor optics, the categorical view", 2016), then by Boisseau and Gibbons ("What you needa know about Yoneda", 2017), then by Riley ("Categories of optics", 2018), and in the mixed enriched case we implement by Clarke, Elkins, Gibbons, Loregian, Milewski, Pillmore and Román ("Profunctor optics, a categorical update", 2019).

Documentation

data Optic objc c objd d objm m o i f g a b s t where

Unified definition of a mixed optic, enriched over Hask (from "Profunctor optics, a categorical update", Definition 2.1).

Constructors

Optic :: (MonoidalAction objm m o i objc c f, MonoidalAction objm m o i objd d g, objc a, objc s, objd b, objd t, objm x) => c s (f x a) -> d (g x b) t -> Optic objc c objd d objm m o i f g a b s t

Instances

(MonoidalAction objm m o i objc c f, MonoidalAction objm m o i objd d g, objc a, objd b) => Tambara (objc :: k2 -> Constraint) (c :: k2 -> k2 -> Type) (objd :: k1 -> Constraint) (d :: k1 -> k1 -> Type) (objm :: k3 -> Constraint) (m :: k3 -> k3 -> Type) (o :: k3 -> k3 -> k3) (i :: k3) (f :: k3 -> k2 -> k2) (g :: k3 -> k1 -> k1) (Optic objc c objd d objm m o i f g a b :: k2 -> k1 -> Type)

Defined in Tambara

Methods

tambara :: (objc x, objd y, objm w) => Optic objc c objd d objm m o i f g a b x y -> Optic objc c objd d objm m o i f g a b (f w x) (g w y)

(MonoidalAction objm m o i objc c f, MonoidalAction objm m o i objd d g, objc a, objd b) => Profunctor (objc :: k2 -> Constraint) (c :: k2 -> k2 -> Type) (objd :: k1 -> Constraint) (d :: k1 -> k1 -> Type) (Optic objc c objd d objm m o i f g a b :: k2 -> k1 -> Type)

Defined in Tambara

Methods

dimap :: (objc x1, objc x2, objd y1, objd y2) => c x2 x1 -> d y1 y2 -> Optic objc c objd d objm m o i f g a b x1 y1 -> Optic objc c objd d objm m o i f g a b x2 y2

class (MonoidalAction objm m o i objc c f, MonoidalAction objm m o i objd d g, Profunctor objc c objd d p) => Tambara objc c objd d objm m o i f g p where

Generalized Tambara modules for a pair of monoidal actions on possibly different categories.

Methods

tambara :: (objc x, objd y, objm w) => p x y -> p (f w x) (g w y)

Instances

(MonoidalAction objm m o i objc c f, MonoidalAction objm m o i objd d g, objc a, objd b) => Tambara (objc :: k2 -> Constraint) (c :: k2 -> k2 -> Type) (objd :: k1 -> Constraint) (d :: k1 -> k1 -> Type) (objm :: k3 -> Constraint) (m :: k3 -> k3 -> Type) (o :: k3 -> k3 -> k3) (i :: k3) (f :: k3 -> k2 -> k2) (g :: k3 -> k1 -> k1) (Optic objc c objd d objm m o i f g a b :: k2 -> k1 -> Type)

Defined in Tambara

Methods

tambara :: (objc x, objd y, objm w) => Optic objc c objd d objm m o i f g a b x y -> Optic objc c objd d objm m o i f g a b (f w x) (g w y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Algebra []) ((->) :: Type -> Type -> Type) (,) () (,) (,) (Aggregating a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Algebra [] w) => Aggregating a b x y -> Aggregating a b (w, x) (w, y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) Either Void Either Either (Replacing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Any w) => Replacing a b x y -> Replacing a b (Either w x) (Either w y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) Either Void Either Either (Setting a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Any w) => Setting a b x y -> Setting a b (Either w x) (Either w y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (,) () (,) (,) (Replacing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Any w) => Replacing a b x y -> Replacing a b (w, x) (w, y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (,) () (,) (,) (Setting a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Any w) => Setting a b x y -> Setting a b (w, x) (w, y)

Monad m => Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Algebra m :: Type -> Constraint) ((->) :: Type -> Type -> Type) (,) () (,) (,) (Classifying m a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Algebra m w) => Classifying m a b x y -> Classifying m a b (w, x) (w, y)

Monad m => Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Algebra m :: Type -> Constraint) ((->) :: Type -> Type -> Type) (,) () (,) (,) (Viewing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Algebra m w) => Viewing a b x y -> Viewing a b (w, x) (w, y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) Either Void Either Either (Previewing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Any w) => Previewing a b x y -> Previewing a b (Either w x) (Either w y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (,) () (,) (,) (Previewing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Any w) => Previewing a b x y -> Previewing a b (w, x) (w, y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (,) () (,) (,) (Viewing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Any w) => Viewing a b x y -> Viewing a b (w, x) (w, y)

Monad m => Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) (Kleisli m :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (,) () (,) (,) (Updating m a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Any w) => Updating m a b x y -> Updating m a b (w, x) (w, y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) Functor (Nat :: (Type -> Type) -> (Type -> Type) -> Type) (Compose :: (Type -> Type) -> (Type -> Type) -> Type -> Type) Identity (App :: (Type -> Type) -> Type -> Type) (App :: (Type -> Type) -> Type -> Type) (Replacing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Functor w) => Replacing a b x y -> Replacing a b (App w x) (App w y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) Applicative (Nat :: (Type -> Type) -> (Type -> Type) -> Type) (Compose :: (Type -> Type) -> (Type -> Type) -> Type -> Type) Identity (App :: (Type -> Type) -> Type -> Type) (App :: (Type -> Type) -> Type -> Type) (Replacing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Applicative w) => Replacing a b x y -> Replacing a b (App w x) (App w y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) Applicative (Nat :: (Type -> Type) -> (Type -> Type) -> Type) (Compose :: (Type -> Type) -> (Type -> Type) -> Type -> Type) Identity (App :: (Type -> Type) -> Type -> Type) (App :: (Type -> Type) -> Type -> Type) (Aggregating a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Applicative w) => Aggregating a b x y -> Aggregating a b (App w x) (App w y)

Tambara (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) (Any :: Type -> Constraint) ((->) :: Type -> Type -> Type) Traversable (Nat :: (Type -> Type) -> (Type -> Type) -> Type) (Compose :: (Type -> Type) -> (Type -> Type) -> Type -> Type) Identity (App :: (Type -> Type) -> Type -> Type) (App :: (Type -> Type) -> Type -> Type) (Replacing a b :: Type -> Type -> Type)

Defined in Combinators

Methods

tambara :: (Any x, Any y, Traversable w) => Replacing a b x y -> Replacing a b (App w x) (App w y)

type ProfOptic objc c objd d objm m o i f g a b s t = forall p. (Tambara objc c objd d objm m o i f g p, MonoidalAction objm m o i objc c f, MonoidalAction objm m o i objd d g, objc a, objd b, objc s, objd t) => p a b -> p s t

Unified definition of Profunctor optic in terms of Tambara modules. This is the Yoneda representation of the category of optics, with Tambara modules as copresheaves.

ex2prof :: forall objc c objd d objm m o i f g a b s t. Optic objc c objd d objm m o i f g a b s t -> ProfOptic objc c objd d objm m o i f g a b s t

Transforms an existential optic into its profunctor representation. This is one side of a Yoneda embedding.

prof2ex :: forall objc c objd d objm m o i f g a b s t. (MonoidalAction objm m o i objc c f, MonoidalAction objm m o i objd d g, objc a, objc s, objd b, objd t) => ProfOptic objc c objd d objm m o i f g a b s t -> Optic objc c objd d objm m o i f g a b s t

Transforms a profunctor optic into its existential representation. This is the other side of a Yoneda embedding.