Data.Square

Double category

There is a double category of Haskell functors and profunctors.

The squares in this double category are natural transformations.

emptySquare :: Square '[] '[] '[] '[]

+-----+
|     |
|     |
|     |
+-----+

forall a b. (a -> b) -> (a -> b)

The empty square is the identity transformation.

proId :: Profunctor p => Square '[p] '[p] '[] '[]

+-----+
|     |
p-----p
|     |
+-----+

forall a b. p a b -> p a b

Profunctors are drawn as horizontal lines.

Note that emptySquare is proId for the profunctor (->). We don't draw a line for (->) because it is the identity for profunctor composition.

funId :: Functor f => Square '[] '[] '[f] '[f]

+--f--+
|  |  |
|  v  |
|  |  |
+--f--+

forall a b. (a -> b) -> (f a -> f b)

Functors are drawn with vertical lines with arrow heads. You will recognize the above type as fmap!

We don't draw lines for the identity functor, because it is the identity for functor composition.

funNat :: (Functor f, Functor g) => (f ~> g) -> Square '[] '[] '[f] '[g]

+--f--+
|  |  |
|  @  |
|  |  |
+--g--+

forall a b. (a -> b) -> (f a -> g b)

Non-identity transformations are drawn with an @ in the middle. Natural transformations between haskell functors are usualy given the type forall a. f a -> g a. The type above you get when fmapping before or after. (It doesn't matter which, because of naturality!)

proNat :: (Profunctor p, Profunctor q) => (p :-> q) -> Square '[p] '[q] '[] '[]

+-----+
|     |
p--@--q
|     |
+-----+

forall a b. p a b -> q a b

Natural transformations between profunctors.

newtype SquareNT p q f g

+--f--+
|  v  |
p--@--q
|  v  |
+--g--+

forall a b. p a b -> q (f a) (g b)

The complete definition of a square is a combination of natural transformations between functors and natural transformations between profunctors.

To make type inferencing easier the above type is wrapped by a newtype.

Constructors

Square

Fields

• unSquare :: forall a b. p a b -> q (f a) (g b)

type Square ps qs fs gs = SquareNT (PList ps) (PList qs) (FList fs) (FList gs)

To make composing squares associative, this library uses squares with lists of functors and profunctors, which are composed together.

FList '[] a ~ a
FList '[f, g, h] a ~ h (g (f a))
PList '[] a b ~ a -> b
PList '[p, q, r] a b ~ (p a x, q x y, r y b)

mkSquare :: Profunctor q => (forall a b. p a b -> q (f a) (g b)) -> Square '[p] '[q] '[f] '[g]

A helper function to add the wrappers needed for PList and FList, if the square has exactly one (pro)functor on each side (which is common).

(|||) infixl 6

Arguments

:: (Profunctor (PList rs), FAppend fs, FAppend gs, Functor (FList hs), Functor (FList is))

=> Square ps qs fs gs

-> Square qs rs hs is

-> Square ps rs (fs ++ hs) (gs ++ is)

+--f--+     +--h--+       +--f--h--+
|  v  |     |  v  |       |  v  v  |
p--@--q ||| q--@--r  ==>  p--@--@--r
|  v  |     |  v  |       |  v  v  |
+--g--+     +--i--+       +--g--i--+

Horizontal composition of squares. proId is the identity of `(|||)`. This is regular function composition of the underlying functions.

(===) infixl 5

Arguments

:: (PAppend ps, PAppend qs, Profunctor (PList ss))

=> Square ps qs fs gs

-> Square rs ss gs hs

-> Square (ps ++ rs) (qs ++ ss) fs hs

+--f--+
|  v  |
p--@--q              +--f--+
|  v  |              |  v  |
+--g--+              p--@--q
  ===        ==>     |  v  |
+--g--+              r--@--s
|  v  |              |  v  |
r--@--s              +--h--+
|  v  |
+--h--+

Vertical composition of squares. funId is the identity of `(===)`.

Proarrow equipment

The double category of haskell functors and profunctors is a proarrow equipment. Which means that we can "bend" functors to become profunctors.

toRight :: Functor f => Square '[] '[Star f] '[f] '[]

+--f--+
|  v  |
|  \->f
|     |
+-----+

A functor f can be bent to the right to become the profunctor Star f.

toLeft :: Square '[Costar f] '[] '[f] '[]

+--f--+
|  v  |
f<-/  |
|     |
+-----+

A functor f can be bent to the left to become the profunctor Costar f.

fromRight :: Functor f => Square '[] '[Costar f] '[] '[f]

+-----+
|     |
|  /-<f
|  v  |
+--f--+

The profunctor Costar f can be bent down to become the functor f again.

fromLeft :: Square '[Star f] '[] '[] '[f]

+-----+
|     |
f>-\  |
|  v  |
+--f--+

The profunctor Star f can be bent down to become the functor f again.

uLeft :: Functor f => Square '[Star f, Costar f] '[] '[] '[]

+-----+
f>-\  |         fromLeft
|  v  |         ===
f<-/  |         toLeft
+-----+

fromLeft and toLeft can be composed vertically to bend Star f back to Costar f.

uRight :: Functor f => Square '[] '[Costar f, Star f] '[] '[]

+-----+
|  /-<f         fromRight
|  v  |         ===
|  \->f         toRight
+-----+

fromRight and toRight can be composed vertically to bend Costar f to Star f.

spiderLemma

Arguments

:: (Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3, Functor g1, Functor g2, Functor g3)

=> Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]

-> Square '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]

+f-f-f+     +--f--+     spiderLemma n =
|v v v|     f> v <f       fromLeft ||| funId ||| fromRight
| \|/ |     | \|/ |       ===
p--@--q ==> p--@--q       n
| /|\ |     | /|\ |       ===
|v v v|     g< v >g       toLeft ||| funId ||| toRight
+g-g-g+     +--g--+

The spider lemma is an example how bending wires can also be seen as sliding functors around corners.

spiderLemma'

Arguments

:: (Profunctor p, Profunctor q, Functor f1, Functor f2, Functor f3, Functor g1, Functor g2, Functor g3)

=> Square '[Star f1, p, Costar g1] '[Costar f3, q, Star g3] '[f2] '[g2]

-> Square '[p] '[q] '[f1, f2, f3] '[g1, g2, g3]

spiderLemma' n = (toRight === proId === fromRight) ||| n ||| (toLeft === proId === fromLeft)

The spider lemma in the other direction.

In other categories than Hask

A--f--C
|  v  |
p--@--q
|  v  |
B--g--D

Squares can be generalized further by choosing a different category for each quadrant. To use this, SquareNT has been made kind polymorphic:

type SquareNT :: (a -> b -> Type) -> (c -> d -> Type) -> (a -> c) -> (b -> d) -> Type

This library is mostly about staying in Hask, but it is interesting to use f.e. the product category Hask × Hask or the unit category.

type Square21 ps1 ps2 qs f g = SquareNT (PList ps1 :**: PList ps2) (PList qs) (UncurryF f) (UncurryF g)

H²-f--H
|  v  |
p--@--q     H = Hask, H² = Hask x Hask
|  v  |
H²-g--H

data (p1 :**: p2) a b where

Combine two profunctors from Hask to a profunctor from Hask x Hask

Constructors

(:**:) :: p1 a1 b1 -> p2 a2 b2 -> (p1 :**: p2) '(a1, a2) '(b1, b2)

data UncurryF f a where

Uncurry the kind of a bifunctor.

type UncurryF :: (a -> b -> Type) -> (a, b) -> Type

Constructors

UncurryF

Fields

• :: { curryF :: f a b
•    } -> UncurryF f '(a, b)

type Square01 q a b = SquareNT Unit (PList q) (ValueF a) (ValueF b)

1--a--H
|  v  |
U--@--q     1 = Hask^0 = (), H = Hask
|  v  |
1--b--H

data Unit a b where

The boring profunctor from and to the unit category.

Constructors

Unit :: Unit () ()

data ValueF x u where

Values as a functor from the unit category.

Constructors

ValueF :: a -> ValueF a ()