Represent polymorphic function between two functors F
, G
trait ~>[F[_], G[_]] {
def apply[X](fa: F[X]): G[X]
}
that satisfy naturality square:
def naturalitySquare[A,B](fa: F[A], ff: ~>[F,G], g: A => B)(implicit FF: Functor[F], FG: Functor[G]): Boolean = {
val v1: G[A] = ff(fa)
val v2: G[B] = FG.map(v1)(g)
val w1: F[B] = FF.map(fa)(g)
val w2: G[B] = ff(w1)
v2 == w2
}
for example:
val headOption: List ~> Option = new ~>[List,Option] {
def apply[A](fa: List[A]): Option[A] = fa.headOption
}
Every polymorphic function (that do the same thing - do not change behavior for a specific type of X) have some nice properties. More in paper by Philip Wadler - Theorems for free.
-
Encoding close to mathematics: vpatryshev/Categories
-
Formalization in proof assistants: statebox/idris-ct, agda-categories UniMath, CubicalTT
-
Definition in Category Theory: nLab
-
Resources
- Cats docs
- tpolecat/doobie KleisliInterpreter uses natural transformations
- Parametricity: Money for Nothing and Theorems for Free - Bartosz Milewski (blog post)
- Natural transformations - TheCatsters (video playlist)
- Implementation: Haskell
Functor that works on natural transformations rather than on regular types
trait FFunctor[FF[_]] {
def ffmap[F[_],G[_]](nat: NaturalTransf[F,G]): FF[F] => FF[G]
}
-
Laws:
- identity:
ffmap id == id
- composition:
ffmap (eta . phi) = ffmap eta . ffmap phi
- identity:
-
Resources
- (Haskell) Functor Functors - Benjamin (blog post)
- Resources
- (Haskell) monad morphisms
- (Haskell) MFunctor used to be in pipes
- (Haskell) Q: What is not an MFunctor? reddit
- (Haskell) MMonad
- (Haskell) Github issue with code with MCoyoneda
- (Haskell) Tutorial - Gabriella Gonzalez
- (Haskell) mmorph-1.0.0: Monad morphisms - Gabriella Gonzalez blog post
In Category Theory a Monoidal Category is a Category with a Bifuctor and morphisms
trait MonoidalCategory[M[_, _], I] {
val tensor: Bifunctor[M]
val mcId: I
def rho[A] (mai: M[A,I]): A
def rho_inv[A](a: A): M[A, I]
def lambda[A] (mia: M[I,A]): A
def lambda_inv[A,B](a: A): M[I, A]
def alpha[A,B,C]( mabc: M[M[A,B], C]): M[A, M[B,C]]
def alpha_inv[A,B,C](mabc: M[A, M[B,C]]): M[M[A,B], C]
}
that satisfy triangular equations:
and pentagon equations:
trait MonoidalCategoryLaws[M[_, _], I] extends MonoidalCategory[M,I] {
def triangleEquations[A, B](fa: M[M[A, I], B]): Boolean = {
// ro[A] * id[B]
// (A * I) * C ----------------> A * B
val v1: M[A, B] = mcBif.bimap(rho[A], identity[B])(fa)
// alpha[A,I,B] id[A] * lambda[B]
// (A * I) * C --------------> A * (I * C) --------------------> A * B
val w1: M[A, M[I, B]] = alpha[A,I,B](fa)
val w2: M[A, B] = mcBif.bimap[A,A, M[I,B],B](identity[A],lambda[B])(w1)
v1 == w2
}
def pentagonEquations[A,B,C,D](fa: M[M[M[A,B],C],D]): Boolean = {
// alpha[A,B,C] * 1D alpha[A,B*C,D]
// ((A * B) * C) * D -------------------> (A * (B * C)) * D ------------------> A * ((B * C) * D)
// 1A * alpha[B,C,D]
// A * ((B * C) * D) ------------------> A * (B * (C * D))
val v1: M[M[A, M[B, C]], D] = mcBif.bimap(alpha[A,B,C],identity[D])(fa)
val v2: M[A, M[M[B,C], D]] = alpha[A,M[B,C],D](v1)
val v3: M[A, M[B, M[C,D]]] = mcBif.bimap(identity[A],alpha[B,C,D])(v2)
// alpha[A*B,C,D] alpha[A,B,C*D]
// ((A * B) * C) * D -----------------> (A * B) * (C * D) -----------------> A * (B * (C * D))
val w1: M[M[A,B], M[C,D]] = alpha[M[A,B],C,D](fa)
val w2: M[A,M[B,M[C,D]]] = alpha[A,B,M[C,D]](w1)
v3 == w2
}
}
We can create monoidal category where product (Tuple) is a bifunctor or an coproduct (Either).
Monoidal Categories are useful if we consider category of endofunctors. If we develop concept of Monoid Object then it is possible to define
- Monads as Monoid Object in Monoidal Category of Endofunctors with Product as Bifunctor
- Applicative as Monoid Object in Monoidal Category of Endofunctors with Day convolution as Bifunctor
In category of Profunctors with Profunctor Product as Bifunctor the Monoid Object is Arrow.
- Resources
- lemastero/MonoidalCategories.scala (Gist)
- (Haskell, Category Theory) Discrimination is Wrong: Improving Productivity - Edward Kmett (video)
- (Haskell, Category Theory) Notions of Computation as Monoids (extended version) - Exequiel Rivas, Mauro Jaskelioff (paper)
- (Haskell) Monoidal Category data-category/Data.Category.Monoidal, categories/Control.Category.Monoidal
- (Haskell) categories Cartesian Monoidal Category
- (Haskell) categories CoCartesian Monoidal Category
-
Resources
- TomasMikula/LambdaCart (CCC is used to define EDSL in Scala)
- Compiling to categories - Conal Elliott (Encoding of many CT abstractions, applications for automatic derivation of functions, describing hardware, Fast Fourier Transformation)
- (Haskell) Cartesian Closed Category in data-category
Monads are monoids in a monoidal category of endofunctors. Applicative functors are also monoids in a monoidal category of endofunctors but as a tensor is used Day convolution.
There is nice intuition for Day convolution as generalization of one of Applicative Functor methods.
- Haskell
data Day f g a where
Day :: forall x y. (x -> y -> a) -> f x -> g y -> Day f g a
- Scala
trait DayConvolution[F[_], G[_], A] {
type X
type Y
val fx: F[X]
val gy: G[Y]
def xya: (X, Y) => A
}
-
Implementation: Scalaz 7, Haskell, Purescritp
-
There is various ways to create Day Convolution:
def day[F[_], G[_], A, B](fab: F[A => B], ga: G[A]): Day[F, G, B]
def intro1[F[_], A](fa: F[A]): Day[Id, F, A]
def intro2[F[_], A](fa: F[A]): Day[F, Id, A]
- Day convolution can be transformed by mapping over last argument, applying natural transformation to one of type constructors, or swapping them
def map[B](f: A => B): Day[F, G, B]
def trans1[H[_]](nat: NaturalTransf[F, H]): Day[H, G, A]
def trans2[H[_]](nat: NaturalTransf[G, H]): Day[F, H, A]
def swapped: Day[G, F, A] = new Day[G, F, A]
- There is various ways to collapse Day convolution into value in type constructor:
def elim1[F[_], A](d: Day[Id, F, A])(implicit FunF: Functor[F]): F[A]
def elim2[F[_], A](d: Day[F, Id, A])(implicit FunF: Functor[F]): F[A]
def dap[F[_], A](d: Day[F, F, A])(implicit AF: Applicative[F]): F[A]
- We can define Functor instance without any conditions on type constructors (so it forms Functor for free like Coyoneda):
def functorDay[F[_], G[_]]: Functor[DayConvolution[F, G, ?]] = new Functor[DayConvolution[F, G, ?]] {
def map[C, D](d: DayConvolution[F, G, C])(f: C => D): DayConvolution[F, G, D] =
new DayConvolution[F, G, D] {
type X = d.X
type Y = d.Y
val fx: F[X] = d.fx
val gy: G[Y] = d.gy
def xya: X => Y => D = x => y => f(d.xya(x)(y))
}
}
-
If both type constructor are Applicative then whoe Day Convolution is applicative. Similarly it is Comonad if both type constructors are Comonads.
-
Resources
- (Haskell) Notions of Computation as Monoids by Exequiel Rivas, Mauro Jaskelioff (paper)
- (Haskell) Reddit comment by echatav (comment)
- (Haskell) Comonads and Day Convolution - Phil Freeman (blog post)
- (Purescript) extensible coeffect system built out of comonads and Day convolution paf31/purescript-smash
- (Purescript) paf31/purescript-react-explore
- (Haskell) usage examples with Free CoFree jwiegley/notes Day
- (Theory) The convolution of comonads is a comonad