From 5a35b099c1c85670b50727d87a76d7bbcb70ea0b Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Tue, 7 Mar 2023 22:15:08 -0500 Subject: [PATCH] Document everything --- Data/Profunctor/Cayley.idr | 1 + Data/Profunctor/Closed.idr | 34 +++++++++- Data/Profunctor/Costrong.idr | 104 +++++++++++++++++++++++------- Data/Profunctor/Functor.idr | 35 ++++++++-- Data/Profunctor/Mapping.idr | 32 ++++++++- Data/Profunctor/Representable.idr | 44 +++++++++---- Data/Profunctor/Sieve.idr | 24 ++++++- Data/Profunctor/Strong.idr | 80 ++++++++++++++++++++++- Data/Profunctor/Traversing.idr | 27 +++++++- Data/Profunctor/Types.idr | 49 +++++++++++++- Data/Profunctor/Yoneda.idr | 14 ++++ Data/Tensor.idr | 34 +++++++++- 12 files changed, 425 insertions(+), 53 deletions(-) diff --git a/Data/Profunctor/Cayley.idr b/Data/Profunctor/Cayley.idr index 48697bd..714baea 100644 --- a/Data/Profunctor/Cayley.idr +++ b/Data/Profunctor/Cayley.idr @@ -11,6 +11,7 @@ import Data.Profunctor.Sieve -- NOTE: This may be better as a type synonym instead of a new type? +||| A profunctor lifted into a functor. public export record Cayley {0 k1,k2,k3 : Type} f (p : k1 -> k2 -> k3) a b where constructor MkCayley diff --git a/Data/Profunctor/Closed.idr b/Data/Profunctor/Closed.idr index f7dbd6f..5f6780d 100644 --- a/Data/Profunctor/Closed.idr +++ b/Data/Profunctor/Closed.idr @@ -8,15 +8,34 @@ import Data.Profunctor.Strong %default total +------------------------------------------------------------------------------ +-- Closed interface +------------------------------------------------------------------------------ + + +||| Closed profunctors preserve the closed structure of a category. +||| +||| Laws: +||| * `lmap (. f) . closed = rmap (. f) . closed` +||| * `closed . closed = dimap uncurry curry . closed` +||| * `dimap const ($ ()) . closed = id` public export interface Profunctor p => Closed p where + ||| The action of a closed profunctor. closed : p a b -> p (x -> a) (x -> b) +------------------------------------------------------------------------------ +-- Implementations for existing types +------------------------------------------------------------------------------ + + export Closed Morphism where closed (Mor f) = Mor (f .) +||| A named implementation of `Closed` for function types. +||| Use this to avoid having to use a type wrapper like `Morphism`. export [Function] Closed (\a,b => a -> b) using Profunctor.Function where closed = (.) @@ -30,6 +49,12 @@ export curry' : Closed p => p (a, b) c -> p a (b -> c) curry' = lmap (,) . closed + +------------------------------------------------------------------------------ +-- Closure +------------------------------------------------------------------------------ + + -- Helper functions for working with function types hither : (s -> (a, b)) -> (s -> a, s -> b) hither h = (fst . h, snd . h) @@ -38,8 +63,8 @@ yon : (s -> a, s -> b) -> s -> (a,b) yon h s = (fst h s, snd h s) --- Closure - +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `Closed`. public export record Closure p a b where constructor MkClosure @@ -84,8 +109,13 @@ unclose : Profunctor q => p :-> Closure q -> p :-> q unclose f p = dimap const ($ ()) $ runClosure $ f p +------------------------------------------------------------------------------ -- Environment +------------------------------------------------------------------------------ + +||| The monad generated by the reflective subcategory of profunctors that +||| implement `Closed`. public export data Environment : (p : Type -> Type -> Type) -> Type -> Type -> Type where MkEnv : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b diff --git a/Data/Profunctor/Costrong.idr b/Data/Profunctor/Costrong.idr index 58d7a98..ca5d3b0 100644 --- a/Data/Profunctor/Costrong.idr +++ b/Data/Profunctor/Costrong.idr @@ -1,3 +1,14 @@ +||| This module defines profunctor costrength with respect to a particular +||| monoidal structure. +||| +||| Since the homset profunctor (`Morphism`) is not costrong, very few +||| profunctors implement this interface. +||| +||| Unlike Haskell's profunctors library, `Costrong` and `Cochoice` are here +||| special cases of the interface `GenCostrong`, which defines costrength with +||| respect to an arbitrary tensor product. When writing implementations for +||| a profunctor, `GenCostrong Pair` and `GenCostrong Either` should be used instead +||| of `Costrong` and `Cochoice` respectively. module Data.Profunctor.Costrong import Data.Morphisms @@ -7,37 +18,71 @@ import Data.Profunctor.Types %default total + +------------------------------------------------------------------------------ +-- Costrength interface +------------------------------------------------------------------------------ + + +||| Profunctor costrength with respect to a tensor product. +||| +||| These constraints are not required by the interface, but the tensor product +||| `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`. +||| +||| Laws: +||| * `costrongl = costrongr . dimap swap swap` +||| * `costrongl . dimap unitr.rightToLeft unitr.leftToRight = id` +||| * `costrongl . lmap (mapSnd f) = costrongl . rmap (mapSnd f)` +||| * `costrongr . costrongr = costrongr . dimap assoc.leftToRight assoc.rightToLeft` +||| +||| @ ten The tensor product of the monoidal structure public export interface Profunctor p => GenCostrong (0 ten : Type -> Type -> Type) p where + ||| The left action of a costrong profunctor. costrongl : p (a `ten` c) (b `ten` c) -> p a b + ||| The right action of a costrong profunctor. costrongr : p (c `ten` a) (c `ten` b) -> p a b +||| Profunctor costrength with respect to the product (`Pair`). public export Costrong : (p : Type -> Type -> Type) -> Type Costrong = GenCostrong Pair +||| A special case of `costrongl` with constraint `Costrong`. +||| This is useful if the typechecker has trouble inferring the tensor product. public export unfirst : Costrong p => p (a, c) (b, c) -> p a b unfirst = costrongl {ten=Pair} +||| A special case of `costrongr` with constraint `Costrong`. +||| This is useful if the typechecker has trouble inferring the tensor product. public export unsecond : Costrong p => p (c, a) (c, b) -> p a b unsecond = costrongr {ten=Pair} +||| Profunctor costrength with respect to the coproduct (`Either`). public export Cochoice : (p : Type -> Type -> Type) -> Type Cochoice = GenCostrong Either +||| A special case of `costrongl` with constraint `Cochoice`. +||| This is useful if the typechecker has trouble inferring the tensor product. public export unleft : Cochoice p => p (Either a c) (Either b c) -> p a b unleft = costrongl {ten=Either} +||| A special case of `costrongr` with constraint `Cochoice`. +||| This is useful if the typechecker has trouble inferring the tensor product. public export unright : Cochoice p => p (Either c a) (Either c b) -> p a b unright = costrongr {ten=Either} --- Implementations + +------------------------------------------------------------------------------ +-- Implementations for existing types +------------------------------------------------------------------------------ + export GenCostrong Pair Tagged where @@ -45,8 +90,13 @@ GenCostrong Pair Tagged where costrongr (Tag (_,x)) = Tag x --- Tambara +------------------------------------------------------------------------------ +-- Cotambara +------------------------------------------------------------------------------ + +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `GenCostrong ten`. public export data GenCotambara : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b @@ -76,43 +126,39 @@ Functor (GenCotambara ten p a) where map = rmap -export -gencotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q -gencotambara f = MkCotambara f - -export -ungencotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q -ungencotambara f p = proextract (f p) - - +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `Costrong`. +||| +||| This is a special case of `GenCotambara`. public export Cotambara : (p : Type -> Type -> Type) -> Type -> Type -> Type Cotambara = GenCotambara Pair -export -cotambara : Costrong p => p :-> q -> p :-> Cotambara q -cotambara = gencotambara - -export -uncotambara : Profunctor q => p :-> Cotambara q -> p :-> q -uncotambara = ungencotambara - - +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `Cochoice`. +||| +||| This is a special case of `GenCotambara`. public export CotambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type CotambaraSum = GenCotambara Either -export -cotambaraSum : Cochoice p => p :-> q -> p :-> CotambaraSum q -cotambaraSum = gencotambara export -uncotambaraSum : Profunctor q => p :-> CotambaraSum q -> p :-> q -uncotambaraSum = ungencotambara +cotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q +cotambara f = MkCotambara f + +export +uncotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q +uncotambara f p = proextract (f p) +------------------------------------------------------------------------------ -- Copastro +------------------------------------------------------------------------------ + +||| The monad generated by the reflective subcategory of profunctors that +||| implement `GenCostrong ten`. public export record GenCopastro (ten, p : Type -> Type -> Type) a b where constructor MkCopastro @@ -144,10 +190,18 @@ ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where procounit (MkCopastro h) = proextract (h id) +||| The monad generated by the reflective subcategory of profunctors that +||| implement `Costrong`. +||| +||| This is a special case of `GenCopastro`. public export Copastro : (p : Type -> Type -> Type) -> Type -> Type -> Type Copastro = GenCopastro Pair +||| The monad generated by the reflective subcategory of profunctors that +||| implement `Cochoice`. +||| +||| This is a special case of `GenCopastro`. public export CopastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type CopastroSum = GenCopastro Either diff --git a/Data/Profunctor/Functor.idr b/Data/Profunctor/Functor.idr index b6c8e76..e163294 100644 --- a/Data/Profunctor/Functor.idr +++ b/Data/Profunctor/Functor.idr @@ -1,3 +1,6 @@ +||| This module defines endofunctors in the category of profunctors `[Idrᵒᵖ * Idr, Idr]`, +||| along with adjunctions of those functors. +||| Examples of these functors include `Yoneda`, `Pastro`, `Closure`, etc. module Data.Profunctor.Functor import Data.Profunctor.Types @@ -5,24 +8,48 @@ import Data.Profunctor.Types %default total +||| An endofunctor in the category of profunctors. +||| +||| Laws: +||| * `promap id = id` +||| * `promap g . promap f = promap (g . f)` public export interface ProfunctorFunctor (0 t : (Type -> Type -> Type) -> k -> k' -> Type) where + ||| Lift a transformation between profunctors into the functor `t`. promap : Profunctor p => p :-> q -> t p :-> t q + +||| A monad in the category of profunctors. +||| +||| Laws: +||| * `projoin . proreturn ≡ id` +||| * `projoin . promap proreturn ≡ id` +||| * `projoin . projoin ≡ projoin . promap projoin` public export interface ProfunctorFunctor t => ProfunctorMonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where propure : Profunctor p => p :-> t p projoin : Profunctor p => t (t p) :-> t p +||| A comonad in the category of profunctors. +||| +||| Laws: +||| * `proextract . produplicate ≡ id` +||| * `promap proextract . produplicate ≡ id` +||| * `produplicate . produplicate ≡ promap produplicate . produplicate` public export interface ProfunctorFunctor t => ProfunctorComonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where proextract : Profunctor p => t p :-> p produplicate : Profunctor p => t p :-> t (t p) +||| An adjunction between endofunctors in the category of profunctors. +||| +||| Laws: +||| * `counit . promap unit ≡ id` +||| * `promap counit . unit ≡ id` public export -interface (ProfunctorFunctor f, ProfunctorFunctor u) => - ProfunctorAdjunction (0 f, u : (Type -> Type -> Type) -> Type -> Type -> Type) | f, u where - prounit : Profunctor p => p :-> u (f p) - procounit : Profunctor p => f (u p) :-> p +interface (ProfunctorFunctor l, ProfunctorFunctor r) => + ProfunctorAdjunction (0 l, r : (Type -> Type -> Type) -> Type -> Type -> Type) | l, r where + prounit : Profunctor p => p :-> r (l p) + procounit : Profunctor p => l (r p) :-> p diff --git a/Data/Profunctor/Mapping.idr b/Data/Profunctor/Mapping.idr index fae756f..90f8335 100644 --- a/Data/Profunctor/Mapping.idr +++ b/Data/Profunctor/Mapping.idr @@ -9,6 +9,18 @@ import Data.Profunctor.Traversing %default total +------------------------------------------------------------------------------ +-- Mapping interface +------------------------------------------------------------------------------ + + +||| The interface of profunctors that implement `roam`. +||| +||| Laws: +||| * `map' . lmap f = lmap (map f) . map'` +||| * `map' . rmap f = rmap (map f) . map'` +||| * `map' . map' = map' @{Compose}` +||| * `dimap Identity runIdentity . map' = id` public export interface (Traversing p, Closed p) => Mapping p where map' : Functor f => p a b -> p (f a) (f b) @@ -21,11 +33,18 @@ interface (Traversing p, Closed p) => Mapping p where functor = MkFunctor (\f => (. (. f))) +------------------------------------------------------------------------------ +-- Implementations for existing types +------------------------------------------------------------------------------ + + export Mapping Morphism where map' (Mor f) = Mor (map f) roam f (Mor x) = Mor (f x) +||| A named implementation of `Mapping` for function types. +||| Use this to avoid having to use a type wrapper like `Morphism`. export [Function] Mapping (\a,b => a -> b) using Traversing.Function Closed.Function where @@ -33,6 +52,13 @@ export roam = id +------------------------------------------------------------------------------ +-- Implementations for existing types +------------------------------------------------------------------------------ + + +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `Mapping`. public export record CofreeMapping p a b where constructor MkCFM @@ -83,8 +109,12 @@ Profunctor p => Mapping (CofreeMapping p) where map' (MkCFM p) = MkCFM (p @{Compose}) roam = roamCofree +------------------------------------------------------------------------------ +-- FreeMapping +------------------------------------------------------------------------------ - +||| The monad generated by the reflective subcategory of profunctors that +||| implement `Mapping`. public export data FreeMapping : (p : Type -> Type -> Type) -> Type -> Type -> Type where MkFM : Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b diff --git a/Data/Profunctor/Representable.idr b/Data/Profunctor/Representable.idr index 58a435d..d51366e 100644 --- a/Data/Profunctor/Representable.idr +++ b/Data/Profunctor/Representable.idr @@ -9,15 +9,45 @@ import Data.Profunctor.Sieve %default total +------------------------------------------------------------------------------ +-- Interfaces +------------------------------------------------------------------------------ + + +||| A profunctor `p` is representable if it is isomorphic to `Star f` for some `f`. public export interface (Sieve p f, Strong p) => Representable p f | p where tabulate : (a -> f b) -> p a b +||| A profunctor `p` is representable if it is isomorphic to `Costar f` for some `f`. +public export +interface Cosieve p f => Corepresentable p f | p where + cotabulate : (f a -> b) -> p a b + + +export +tabulated : (Representable q f, Representable r g) => forall p. Profunctor p => + p (q a b) (r a' b') -> p (a -> f b) (a' -> g b') +tabulated = dimap tabulate sieve + +export +cotabulated : (Corepresentable q f, Corepresentable r g) => forall p. Profunctor p => + p (q a b) (r a' b') -> p (f a -> b) (g a' -> b') +cotabulated = dimap cotabulate cosieve + + +------------------------------------------------------------------------------ +-- Implementations +------------------------------------------------------------------------------ + + export Representable Morphism Identity where tabulate f = Mor (runIdentity . f) +||| A named implementation of `Representable` for function types. +||| Use this to avoid having to use a type wrapper like `Morphism`. export [Function] Representable (\a,b => a -> b) Identity using Sieve.Function Strong.Function where @@ -33,17 +63,7 @@ Functor f => Representable (Star f) f where export -tabulated : (Representable q f, Representable r g) => forall p. Profunctor p => - p (q a b) (r a' b') -> p (a -> f b) (a' -> g b') -tabulated = dimap tabulate sieve +Functor f => Corepresentable (Costar f) f where + cotabulate = MkCostar -public export -interface (Cosieve p f, Costrong p) => Corepresentable p f | p where - cotabulate : (f a -> b) -> p a b - - -export -cotabulated : (Corepresentable q f, Corepresentable r g) => forall p. Profunctor p => - p (q a b) (r a' b') -> p (f a -> b) (g a' -> b') -cotabulated = dimap cotabulate cosieve diff --git a/Data/Profunctor/Sieve.idr b/Data/Profunctor/Sieve.idr index 65a8935..7308062 100644 --- a/Data/Profunctor/Sieve.idr +++ b/Data/Profunctor/Sieve.idr @@ -7,15 +7,34 @@ import Data.Profunctor %default total +------------------------------------------------------------------------------ +-- Interfaces +------------------------------------------------------------------------------ + + +||| A profunctor `p` is a sieve on `f` if it is a subprofunctor of `Star f`. public export interface (Profunctor p, Functor f) => Sieve p f | p where sieve : p a b -> a -> f b +||| A profunctor `p` is a cosieve on `f` if it is a subprofunctor of `Costar f`. +public export +interface (Profunctor p, Functor f) => Cosieve p f | p where + cosieve : p a b -> f a -> b + + +------------------------------------------------------------------------------ +-- Implementations +------------------------------------------------------------------------------ + + export Sieve Morphism Identity where sieve (Mor f) = Id . f +||| A named implementation of `Sieve` for function types. +||| Use this to avoid having to use a type wrapper like `Morphism`. export [Function] Sieve (\a,b => a -> b) Identity using Profunctor.Function where sieve = (Id .) @@ -29,15 +48,14 @@ Functor f => Sieve (Star f) f where sieve = applyStar -public export -interface (Profunctor p, Functor f) => Cosieve p f | p where - cosieve : p a b -> f a -> b export Cosieve Morphism Identity where cosieve (Mor f) = f . runIdentity namespace Cosieve + ||| A named implementation of `Cosieve` for function types. + ||| Use this to avoid having to use a type wrapper like `Morphism`. export [Function] Cosieve (\a,b => a -> b) Identity using Profunctor.Function where cosieve = (. runIdentity) diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr index f481a5f..fe72699 100644 --- a/Data/Profunctor/Strong.idr +++ b/Data/Profunctor/Strong.idr @@ -1,3 +1,11 @@ +||| This module defines profunctor strength with respect to a particular +||| monoidal structure. +||| +||| Unlike Haskell's profunctors library, `Strong` and `Choice` are here +||| special cases of the interface `GenStrong`, which defines strength with +||| respect to an arbitrary tensor product. When writing implementations for +||| a profunctor, `GenStrong Pair` and `GenStrong Either` should be used instead +||| of `Strong` and `Choice` respectively. module Data.Profunctor.Strong import Data.Morphisms @@ -7,50 +15,92 @@ import Data.Profunctor.Types %default total + +------------------------------------------------------------------------------ +-- Strength interface +------------------------------------------------------------------------------ + +||| Profunctor strength with respect to a tensor product. +||| A strong profunctor preserves the monoidal structure of a category. +||| +||| These constraints are not required by the interface, but the tensor product +||| `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`. +||| +||| Laws: +||| * `strongl = dimap swap swap . strongr` +||| * `dimap unitr.rightToLeft unitr.leftToRight . strongl = id` +||| * `lmap (mapSnd f) . strongl = rmap (mapSnd f) . strongl` +||| * `strongr . strongr = dimap assoc.rightToLeft assoc.leftToRight . strongr` +||| +||| @ ten The tensor product of the monoidal structure public export interface Profunctor p => GenStrong (0 ten : Type -> Type -> Type) p where + ||| The left action of a strong profunctor. strongl : p a b -> p (a `ten` c) (b `ten` c) + ||| The right action of a strong profunctor. strongr : p a b -> p (c `ten` a) (c `ten` b) +||| Profunctor strength with respect to the product (`Pair`). public export Strong : (p : Type -> Type -> Type) -> Type Strong = GenStrong Pair +||| A special case of `strongl` with constraint `Strong`. +||| This is useful if the typechecker has trouble inferring the tensor product. +%inline public export first : Strong p => p a b -> p (a, c) (b, c) first = strongl {ten=Pair} +||| A special case of `strongr` with constraint `Strong`. +||| This is useful if the typechecker has trouble inferring the tensor product. +%inline public export second : Strong p => p a b -> p (c, a) (c, b) second = strongr {ten=Pair} +||| Profunctor strength with respect to the coproduct (`Either`). public export Choice : (p : Type -> Type -> Type) -> Type Choice = GenStrong Either +||| A special case of `strongl` with constraint `Choice`. +||| This is useful if the typechecker has trouble inferring the tensor product to use. +%inline public export left : Choice p => p a b -> p (Either a c) (Either b c) left = strongl {ten=Either} +||| A special case of `strongr` with constraint `Choice`. +||| This is useful if the typechecker has trouble inferring the tensor product to use. +%inline public export right : Choice p => p a b -> p (Either c a) (Either c b) right = strongr {ten=Either} - export uncurry' : Strong p => p a (b -> c) -> p (a, b) c uncurry' = rmap (uncurry id) . first +export +strong : Strong p => (a -> b -> c) -> p a b -> p a c +strong f = dimap dup (uncurry $ flip f) . first + + +------------------------------------------------------------------------------ +-- Implementations for existing types +------------------------------------------------------------------------------ --- Implementations export Bifunctor ten => GenStrong ten Morphism where strongl (Mor f) = Mor (mapFst f) strongr (Mor f) = Mor (mapSnd f) +||| A named implementation of `GenStrong` for function types. +||| Use this to avoid having to use a type wrapper like `Morphism`. export [Function] Bifunctor ten => GenStrong ten (\a,b => a -> b) using Profunctor.Function where @@ -83,8 +133,13 @@ GenStrong Either Tagged where strongr (Tag x) = Tag (Right x) +------------------------------------------------------------------------------ -- Tambara +------------------------------------------------------------------------------ + +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `GenStrong ten`. public export record GenTambara (ten, p : Type -> Type -> Type) a b where constructor MkTambara @@ -114,10 +169,18 @@ Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where map = rmap +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `Strong`. +||| +||| This is a special case of `GenTambara`. public export Tambara : (p : Type -> Type -> Type) -> Type -> Type -> Type Tambara = GenTambara Pair +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `Choice`. +||| +||| This is a special case of `GenTambara`. public export TambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type TambaraSum = GenTambara Either @@ -132,8 +195,13 @@ untambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q untambara f x = dimap unitr.rightToLeft unitr.leftToRight $ runTambara $ f x +------------------------------------------------------------------------------ -- Pastro +------------------------------------------------------------------------------ + +||| The monad generated by the reflective subcategory of profunctors that +||| implement `GenStrong ten`. public export data GenPastro : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where MkPastro : (y `ten` z -> b) -> p x y -> (a -> x `ten` z) -> GenPastro ten p a b @@ -181,10 +249,18 @@ export r' = mapSnd swap . assoc.rightToLeft . mapFst r . swap +||| The monad generated by the reflective subcategory of profunctors that +||| implement `Strong`. +||| +||| This is a special case of `GenPastro`. public export Pastro : (p : Type -> Type -> Type) -> Type -> Type -> Type Pastro = GenPastro Pair +||| The monad generated by the reflective subcategory of profunctors that +||| implement `Choice`. +||| +||| This is a special case of `GenPastro`. public export PastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type PastroSum = GenPastro Either diff --git a/Data/Profunctor/Traversing.idr b/Data/Profunctor/Traversing.idr index ff2eac1..d123747 100644 --- a/Data/Profunctor/Traversing.idr +++ b/Data/Profunctor/Traversing.idr @@ -61,6 +61,20 @@ Traversable (Baz t b) where traverse f bz = map (\m => MkBaz (runBazaar m)) $ runBaz bz @{Compose} $ \x => sell <$> f x +------------------------------------------------------------------------------ +-- Traversing interface +------------------------------------------------------------------------------ + + +||| The interface of profunctors that implement `wander`. +||| NOTE: Definitions in terms of `wander` are much more efficient! +||| +||| Laws: +||| * `traverse' = wander traverse` +||| * `traverse' . lmap f = lmap (map f) . traverse'` +||| * `traverse' . rmap f = rmap (map f) . traverse'` +||| * `traverse' . traverse' = traverse' @{Compose}` +||| * `dimap Id runIdentity . traverse' = id` public export interface (Strong p, Choice p) => Traversing p where traverse' : Traversable f => p a b -> p (f a) (f b) @@ -75,6 +89,8 @@ Traversing Morphism where traverse' (Mor f) = Mor (map f) wander f (Mor p) = Mor (runIdentity . (f $ Id . p)) +||| A named implementation of `Traversing` for function types. +||| Use this to avoid having to use a type wrapper like `Morphism`. export [Function] Traversing (\a,b => a -> b) using Strong.Function where traverse' = map @@ -91,9 +107,13 @@ Applicative f => Traversing (Star f) where wander f (MkStar p) = MkStar (f p) - +------------------------------------------------------------------------------ -- CofreeTraversing +------------------------------------------------------------------------------ + +||| The comonad generated by the reflective subcategory of profunctors that +||| implement `Traversing`. public export record CofreeTraversing p a b where constructor MkCFT @@ -142,8 +162,13 @@ uncofreeTraversing : Profunctor q => p :-> CofreeTraversing q -> p :-> q uncofreeTraversing f p = proextract $ f p +------------------------------------------------------------------------------ -- FreeTraversing +------------------------------------------------------------------------------ + +||| The monad generated by the reflective subcategory of profunctors that +||| implement `Traversing`. public export data FreeTraversing : (p : Type -> Type -> Type) -> Type -> Type -> Type where MkFT : Traversable f => (f y -> b) -> p x y -> (a -> f x) -> FreeTraversing p a b diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr index c5b3310..3211308 100644 --- a/Data/Profunctor/Types.idr +++ b/Data/Profunctor/Types.idr @@ -1,3 +1,5 @@ +||| This module contains the Profunctor interface itself, along with a few +||| examples of profunctors. module Data.Profunctor.Types import Data.Contravariant @@ -6,26 +8,56 @@ import Data.Morphisms %default total +------------------------------------------------------------------------------ +-- Profunctor interface +------------------------------------------------------------------------------ + + +||| An interface for (self-enriched) profunctors `Idr -/-> Idr`. +||| +||| Formally, a profunctor is a binary functor that is contravariant in its +||| first argument and covariant in its second. A common example of a profunctor +||| is the (non-dependent) function type. +||| +||| Implementations can be defined by specifying either `dimap` or both `lmap` +||| and `rmap`. +||| +||| Laws: +||| * `dimap id id = id` +||| * `dimap (f . g) (h . i) = dimap g h . dimap f i` public export interface Profunctor p where + ||| Map over both parameters of a profunctor at the same time, with the + ||| left function argument mapping contravariantly. dimap : (a -> b) -> (c -> d) -> p b c -> p a d dimap f g = lmap f . rmap g + ||| Map contravariantly over the first parameter of a profunctor. lmap : (a -> b) -> p b c -> p a c lmap f = dimap f id + ||| Map covariantly over the second parameter of a profunctor. rmap : (b -> c) -> p a b -> p a c rmap = dimap id infix 0 :-> +||| A transformation between profunctors that preserves their type parameters. +||| +||| Formally, this is a natural transformation of functors `Idrᵒᵖ * Idr => Idr`. +||| +||| If the transformation is `tr`, then we have the following law: +||| * `tr . dimap f g = dimap f g . tr` public export 0 (:->) : (p, q : k -> k' -> Type) -> Type p :-> q = forall a, b. p a b -> q a b --- Instances for existing types +------------------------------------------------------------------------------ +-- Implementations for existing types +------------------------------------------------------------------------------ + export Profunctor Morphism where @@ -34,6 +66,8 @@ Profunctor Morphism where rmap = map namespace Profunctor + ||| A named implementation of `Profunctor` for function types. + ||| Use this to avoid having to use a type wrapper like `Morphism`. export [Function] Profunctor (\a,b => a -> b) where dimap f g h = g . h . f @@ -47,8 +81,15 @@ Functor f => Profunctor (Kleislimorphism f) where rmap = map --- Examples of profunctors +------------------------------------------------------------------------------ +-- Implementations for existing types +------------------------------------------------------------------------------ + +||| Lift a functor into a profunctor in the return type. +||| +||| This type is equivalent to `Kleislimorphism` except for the polymorphic type +||| of `b`. public export record Star {0 k : Type} (f : k -> Type) a (b : k) where constructor MkStar @@ -81,6 +122,7 @@ Functor f => Profunctor (Star f) where rmap f (MkStar g) = MkStar (map f . g) +||| Lift a functor into a profunctor in the argument type. public export record Costar {0 k : Type} (f : k -> Type) (a : k) b where constructor MkCostar @@ -106,11 +148,14 @@ Functor f => Profunctor (Costar f) where rmap f (MkCostar g) = MkCostar (f . g) +||| The profunctor that ignores its argument type. +||| Equivalent to `const id` up to isomorphism. public export record Tagged {0 k : Type} (a : k) b where constructor Tag runTagged : b +||| Retag the value with a different type-level parameter. public export retag : Tagged a c -> Tagged b c retag (Tag x) = Tag x diff --git a/Data/Profunctor/Yoneda.idr b/Data/Profunctor/Yoneda.idr index 08edd93..badb280 100644 --- a/Data/Profunctor/Yoneda.idr +++ b/Data/Profunctor/Yoneda.idr @@ -9,6 +9,12 @@ import Data.Profunctor.Sieve %default total +------------------------------------------------------------------------------ +-- Yoneda +------------------------------------------------------------------------------ + + +||| The cofree profunctor given a data constructor with two type parameters. public export record Yoneda p a b where constructor MkYoneda @@ -34,6 +40,7 @@ ProfunctorComonad Yoneda where proextract (MkYoneda p) = p id id produplicate p = MkYoneda $ \l,r => dimap l r p +||| A witness that `Yoneda p` and `p` are equivalent when `p` is a profunctor. export yonedaEqv : Profunctor p => p a b <=> Yoneda p a b yonedaEqv = MkEquivalence propure proextract @@ -75,6 +82,12 @@ Cosieve p f => Cosieve (Yoneda p) f where cosieve = cosieve . proextract +------------------------------------------------------------------------------ +-- Coyoneda +------------------------------------------------------------------------------ + + +||| The free profunctor given a data constructor with two type parameters. public export data Coyoneda : (p : Type -> Type -> Type) -> Type -> Type -> Type where MkCoyoneda : (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b @@ -100,6 +113,7 @@ ProfunctorComonad Coyoneda where proextract (MkCoyoneda l r p) = dimap l r p produplicate = MkCoyoneda id id +||| A witness that `Coyoneda p` and `p` are equivalent when `p` is a profunctor. export coyonedaEqv : Profunctor p => p a b <=> Coyoneda p a b coyonedaEqv = MkEquivalence propure proextract diff --git a/Data/Tensor.idr b/Data/Tensor.idr index 4d12017..7e8ee20 100644 --- a/Data/Tensor.idr +++ b/Data/Tensor.idr @@ -1,12 +1,29 @@ +||| This module defines tensor products, which are later used to define +||| the concept of profunctor strength. The two primary tensor products +||| in `Idr` are the product (`Pair`) and the coproduct (`Either`). module Data.Tensor %default total +------------------------------------------------------------------------------ +-- Tensor products +------------------------------------------------------------------------------ + + +||| A bifunctor that admits an *associator*, i.e. a bifunctor that is +||| associative up to isomorphism. +||| +||| Laws: +||| * `mapFst assoc.rightToLeft . assoc.leftToRight . assoc.leftToRight = assoc.leftToRight . mapSnd assoc.leftToRight` public export interface Bifunctor ten => Associative ten where assoc : a `ten` (b `ten` c) <=> (a `ten` b) `ten` c +||| A bifunctor that admits a swap map, i.e. a bifunctor that is +||| symmetric up to isomorphism. +||| +||| The bifunctor `ten` is generally also associative. public export interface Bifunctor ten => Symmetric ten where swap : a `ten` b -> b `ten` a @@ -16,13 +33,23 @@ interface Bifunctor ten => Symmetric ten where symmetric = MkEquivalence swap swap - +||| A tensor product is an associative bifunctor that has an identity element +||| up to isomorphism. Tensor products constitute the monoidal structure of a +||| monoidal category. +||| +||| Laws: +||| * `mapSnd unitl.leftToRight = mapFst unitr.leftToRight . assoc.leftToRight` public export interface Associative ten => Tensor ten i | ten where unitl : i `ten` a <=> a unitr : a `ten` i <=> a +------------------------------------------------------------------------------ +-- Cartesian monoidal structure +------------------------------------------------------------------------------ + + export Associative Pair where assoc = MkEquivalence (\(x,(y,z)) => ((x,y),z)) (\((x,y),z) => (x,(y,z))) @@ -37,6 +64,11 @@ Tensor Pair () where unitr = MkEquivalence fst (,()) +------------------------------------------------------------------------------ +-- Cocartesian monoidal structure +------------------------------------------------------------------------------ + + export Associative Either where assoc = MkEquivalence f b