Last active
September 23, 2024 18:27
-
-
Save echatav/25815ea86a4f3f0c7861e289703b9043 to your computer and use it in GitHub Desktop.
alternative, filterable, distributive and partial functors and profunctors
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Given distributive categories | |
* -C>, >C<, 1C, +C+, 0C | |
* -D>, >D<, 1D, +D+, 0D | |
An alternative functor consists of | |
* A functor | |
- F : C -> D | |
* morphisms | |
- eps : 1D -D> F(1C) | |
- mu : F(a) >D< F(b) -D> F(a >C< b) | |
- eta : 1D -D> F(0C) | |
- nu : F(a) >D< F(b) -D> F(a +C+ b) | |
* laws | |
- (F, eps, mu) is a lax monoidal functor | |
- (F, eta, nu) is a lax monoidal functor | |
A lax distributive functor consists of | |
* A functor | |
- F : C -> D | |
* morphisms | |
- eps : 1D -D> F(1C) | |
- mu : F(a) >D< F(b) -D> F(a >C< b) | |
- iota' : F(0C) -D> 0D | |
- kappa' : F(a +C+ b) -D> F(a) +D+ F(b) | |
* laws | |
- (F, eps, mu) is a lax monoidal functor | |
- (F, iota', kappa') is an oplax monoidal functor | |
A filterable functor consists of | |
* A functor | |
- F : C -> D | |
* morphisms | |
- iota : 0D -D> F(0C) | |
- kappa : F(a) +D+ F(b) -D> F(a +C+ b) | |
- eta' : F(0C) -D> 1D | |
- nu' : F(a +C+ b) -D> F(a) >D< F(b) | |
* laws | |
- (F, iota, kappa) is a lax monoidal functor | |
- (F, eta', nu') is an oplax monoidal functor | |
A partial distributive functor consists of | |
* A functor | |
- F : C -> D | |
* morphisms | |
- eps : 1D -D> F(1C) | |
- mu : F(a) >D< F(b) -D> F(a >C< b) | |
- iota : 0D -D> F(0C) | |
- kappa : F(a) +D+ F(b) -D> F(a +C+ b) | |
- eta : F(0C) -D> 0D | |
- nu : F(a +C+ b) -D> F(a) +D+ F(b) | |
- eta' : F(0C) -D> 1D | |
- nu' : F(a +C+ b) -D> F(a) >D< F(b) | |
* laws | |
- (F, eps, mu, eta, nu) is an alternative functor | |
- (F, iota, kappa, eta', nu') is a filterable functor | |
- (F, eta, eta', nu, nu') is a strong monoidal functor | |
Construct distributive categories with | |
* C^op x D | |
- (a >C< c, b >D< d) | |
- (1C, 1D) | |
- (a +C+ c, b +D+ d) | |
- (0C, 0D) | |
* Set | |
- Functions -> | |
- Cartesian product >< | |
- One point set 1 | |
- Disjoint union | | |
- Empty set 0 | |
A lax distributive profunctor consists of | |
* A profunctor | |
- P : C^op x D -> Set | |
* functions | |
- eps : 1 -> P(1C, 1D) | |
- mu : P(a,b) >< P(c,d) -> P(a >C< c, b >D< d) | |
- eta : 1 -> P(0C, 0D) | |
- nu : P(a,b) >< P(c,d) -> P(a +C+ c, b +D+ d) | |
* law | |
- (P, eps, mu, eta, nu) is a lax alternative functor | |
A partial profunctor consists of | |
* A profunctor | |
- P : C^op x D -> Set | |
* functions | |
- iota : 0 -> P(0C, 0D) | |
- kappa : P(a,b) | P(c,d) -> P(a +C+ c, b +D+ d) | |
- eta' : P(0C, 0D) -> 1 | |
- nu' : P(a +C+ c, b +D+ d) -> P(a,b) >< P(c,d) | |
* law | |
- (P, iota, kappa, eta', nu') is a filterable functor | |
A partial distributive profunctor consists of | |
* A profunctor | |
- P : C^op x D -> Set | |
* functions | |
- eps : 1 -> P(1C, 1D) | |
- mu : P(a,b) >< P(c,d) -> P(a >C< c, b >D< d) | |
- iota : 0 -> P(0C, 0D) | |
- kappa : P(a,b) | P(c,d) -> P(a +C+ c, b +D+ d) | |
- eta : 1 -> P(0C, 0D) | |
- nu : P(a,b) >< P(c,d) -> P(a +C+ c, b +D+ d) | |
- eta' : P(0C, 0D) -> 1 | |
- nu' : P(a +C+ c, b +D+ d) -> P(a,b) >< P(c,d) | |
* law | |
- (P, eps, mu, iota, kappa, eta, nu, eta', nu') is a syntax functor | |
Proposition: | |
Given a lax distributive functor F, | |
both F^* and F_* are lax distributive profunctors. | |
Example: | |
In Haskell, the `Alternative` typeclass is equivalent to | |
an alternative functor from ((->), (,), (), Either, Void) to ((->), (,), ()). | |
``` | |
eps :: Applicative f => () -> f () | |
eps _ = pure () | |
mu :: Applicative f => (f a, f b) -> f (a,b) | |
mu (fa, fb) = (,) <$> fa <*> fb | |
eta :: Alternative f => () -> f Void | |
eta _ = empty | |
nu :: Alternative f => (f a, f b) -> f (Either a b) | |
nu (fa, fb) = Left <$> fa <|> Right <$> fb | |
``` | |
Examples of lax distributive functors can be found too, | |
using the `Adjunction` typeclass in Haskell. | |
``` | |
eta :: Adjunction f u => f Void -> Void | |
eta = unabsurdL | |
nu :: Adjunction f u => f (Either a b) -> Either (f a) (f b) | |
nu = cozipL | |
``` |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment