-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | The double category of Hask functors and profunctors
--
-- The double category of Hask functors and profunctors
@package squares
@version 0
-- | Utilities for type level lists.
module Data.Type.List
-- | Type level list append
type family (as :: [k]) ++ (bs :: [k]) :: [k]
module Data.Profunctor.Composition.List
-- | N-ary composition of profunctors.
data PList (ps :: [* -> * -> *]) (a :: *) (b :: *)
[Hom] :: {unHom :: a -> b} -> PList '[] a b
[P] :: {unP :: p a b} -> PList '[p] a b
[PComp] :: p a x -> PList (q : qs) x b -> PList (p : (q : qs)) a b
-- | Combining and splitting nested PLists.
class PAppend p
pappend :: (PAppend p, Profunctor (PList q)) => Procompose (PList q) (PList p) a b -> PList (p ++ q) a b
punappend :: PAppend p => PList (p ++ q) a b -> Procompose (PList q) (PList p) a b
instance Data.Profunctor.Composition.List.PAppend '[]
instance Data.Profunctor.Unsafe.Profunctor p => Data.Profunctor.Composition.List.PAppend '[p]
instance (Data.Profunctor.Unsafe.Profunctor p, Data.Profunctor.Composition.List.PAppend (q : qs)) => Data.Profunctor.Composition.List.PAppend (p : q : qs)
instance Data.Profunctor.Unsafe.Profunctor (Data.Profunctor.Composition.List.PList '[])
instance Data.Profunctor.Unsafe.Profunctor p => Data.Profunctor.Unsafe.Profunctor (Data.Profunctor.Composition.List.PList '[p])
instance (Data.Profunctor.Unsafe.Profunctor p, Data.Profunctor.Unsafe.Profunctor (Data.Profunctor.Composition.List.PList (q : qs))) => Data.Profunctor.Unsafe.Profunctor (Data.Profunctor.Composition.List.PList (p : q : qs))
module Data.Functor.Compose.List
-- | N-ary composition of functors.
--
--
-- FList '[] a ~ a
-- FList '[f, g, h] a ~ h (g (f a))
--
data FList (fs :: [* -> *]) (a :: *)
[Id] :: {unId :: a} -> FList '[] a
[F] :: {unF :: f a} -> FList '[f] a
[FComp] :: {unFComp :: FList (g : gs) (f a)} -> FList (f : (g : gs)) a
-- | Combining and splitting nested FLists.
class FAppend f
fappend :: (FAppend f, Functor (FList g)) => FList g (FList f a) -> FList (f ++ g) a
funappend :: (FAppend f, Functor (FList g)) => FList (f ++ g) a -> FList g (FList f a)
-- | Natural transformations between two functors. (Why is this still not
-- in base??)
type f ~> g = forall a. f a -> g a
instance Data.Functor.Compose.List.FAppend '[]
instance Data.Functor.Compose.List.FAppend '[f]
instance (GHC.Base.Functor f, Data.Functor.Compose.List.FAppend (g : gs)) => Data.Functor.Compose.List.FAppend (f : g : gs)
instance GHC.Base.Functor (Data.Functor.Compose.List.FList '[])
instance GHC.Base.Functor f => GHC.Base.Functor (Data.Functor.Compose.List.FList '[f])
instance (GHC.Base.Functor f, GHC.Base.Functor (Data.Functor.Compose.List.FList (g : gs))) => GHC.Base.Functor (Data.Functor.Compose.List.FList (f : g : gs))
module Data.Square
-- |
-- +-----+
-- | |
-- | |
-- | |
-- +-----+
--
--
--
-- forall a b. (a -> b) -> (a -> b)
--
--
-- The empty square is the identity transformation.
emptySquare :: Square '[] '[] '[] '[]
-- |
-- +-----+
-- | |
-- 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.
proId :: Profunctor p => Square '[p] '[p] '[] '[]
-- |
-- +--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.
funId :: Functor f => Square '[] '[] '[f] '[f]
-- |
-- +--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!)
funNat :: (Functor f, Functor g) => (f ~> g) -> Square '[] '[] '[f] '[g]
-- |
-- +-----+
-- | |
-- p--@--q
-- | |
-- +-----+
--
--
--
-- forall a b. p a b -> q a b
--
--
-- Natural transformations between profunctors.
proNat :: (Profunctor p, Profunctor q) => (p :-> q) -> Square '[p] '[q] '[] '[]
-- |
-- +--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.
newtype SquareNT p q f g
Square :: (forall a b. p a b -> q (f a) (g b)) -> SquareNT p q f g
[unSquare] :: SquareNT p q f g -> forall a b. p a b -> q (f a) (g b)
-- | 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)
--
type Square ps qs fs gs = SquareNT (PList ps) (PList qs) (FList fs) (FList gs)
-- | 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).
mkSquare :: Profunctor q => (forall a b. p a b -> q (f a) (g b)) -> Square '[p] '[q] '[f] '[g]
-- |
-- +--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
-- `(|||)`.
(|||) :: (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)
infixl 6 |||
-- |
-- +--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
-- `(===)`.
(===) :: (PAppend ps, PAppend qs, Profunctor (PList ss)) => Square ps qs fs gs -> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs
infixl 5 ===
-- |
-- +--f--+
-- | v |
-- | \->f
-- | |
-- +-----+
--
--
-- A functor f can be bent to the right to become the profunctor
-- Star f.
toRight :: Functor f => Square '[] '[Star f] '[f] '[]
-- |
-- +--f--+
-- | v |
-- f<-/ |
-- | |
-- +-----+
--
--
-- A functor f can be bent to the left to become the profunctor
-- Costar f.
toLeft :: Square '[Costar f] '[] '[f] '[]
-- |
-- +-----+
-- | |
-- | /-<f
-- | v |
-- +--f--+
--
--
-- The profunctor Costar f can be bent down to become the
-- functor f again.
fromRight :: Functor f => Square '[] '[Costar f] '[] '[f]
-- |
-- +-----+
-- | |
-- f>-\ |
-- | v |
-- +--f--+
--
--
-- The profunctor Star f can be bent down to become the
-- functor f again.
fromLeft :: Square '[Star f] '[] '[] '[f]
-- |
-- +-----+
-- f>-\ | fromLeft
-- | v | ===
-- f<-/ | toLeft
-- +-----+
--
--
-- fromLeft and toLeft can be composed vertically to bend
-- Star f back to Costar f.
uLeft :: Functor f => Square '[Star f, Costar f] '[] '[] '[]
-- |
-- +-----+
-- | /-<f fromRight
-- | v | ===
-- | \->f toRight
-- +-----+
--
--
-- fromRight and toRight can be composed vertically to bend
-- Costar f to Star f.
uRight :: Functor f => Square '[] '[Costar f, Star f] '[] '[]
-- |
-- +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 :: (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]
-- |
-- spiderLemma' n = (toRight === proId === fromRight) ||| n ||| (toLeft === proId === fromLeft)
--
--
-- The spider lemma in the other direction.
spiderLemma' :: (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]
-- |
-- H²-f--H
-- | v |
-- p--@--q H = Hask, H² = Hask x Hask
-- | v |
-- H²-g--H
--
type Square21 ps1 ps2 qs f g = SquareNT (PList ps1 :**: PList ps2) (PList qs) (UncurryF f) (UncurryF g)
-- | Combine two profunctors from Hask to a profunctor from Hask x Hask
data ( p1 :**: p2 ) a b
[:**:] :: p1 a1 b1 -> p2 a2 b2 -> (p1 :**: p2) '(a1, a2) '(b1, b2)
-- | Uncurry the kind of a bifunctor.
--
--
-- type UncurryF :: (a -> b -> Type) -> (a, b) -> Type
--
data UncurryF f a
[UncurryF] :: {curryF :: f a b} -> UncurryF f '(a, b)
-- |
-- 1--a--H
-- | v |
-- U--@--q 1 = Hask^0 = (), H = Hask
-- | v |
-- 1--b--H
--
type Square01 q a b = SquareNT Unit (PList q) (ValueF a) (ValueF b)
-- | The boring profunctor from and to the unit category.
data Unit a b
[Unit] :: Unit '() '()
-- | Values as a functor from the unit category.
data ValueF x u
[ValueF] :: a -> ValueF a '()
module Data.Traversable.Square
-- |
-- +--t--+
-- | v |
-- f>-T->f
-- | v |
-- +--t--+
--
--
-- traverse as a square.
--
-- Naturality law:
--
--
-- +-----t--+ +--t-----+
-- | v | | v |
-- f>-@->T->g === f>-T->@->g
-- | v | | v |
-- +-----t--+ +--t-----+
--
--
-- Identity law:
--
--
-- +--t--+ +--t--+
-- | v | | | |
-- | T | === | v |
-- | v | | | |
-- +--t--+ +--t--+
--
--
-- Composition law:
--
--
-- +--t--+ +--t--+
-- | v | | v |
-- f>-T->f f>\|/>f
-- | v | === | T |
-- g>-T->g g>/|\>g
-- | v | | v |
-- +--t--+ +--t--+
--
traverse :: (Traversable t, Applicative f) => Square '[Star f] '[Star f] '[t] '[t]
-- |
-- +-f-t---+
-- | v v |
-- | \-@-\ |
-- | v v |
-- +---t-f-+
--
--
--
-- sequence = toRight ||| traverse ||| fromLeft
--
sequence :: (Traversable t, Applicative f) => Square '[] '[] '[f, t] '[t, f]
module Data.Profunctor.Square
-- |
-- +-a⊗_-+
-- | v |
-- p--@--p
-- | v |
-- +-a⊗_-+
--
second :: Strong p => Square '[p] '[p] '[(,) a] '[(,) a]
-- |
-- +-a⊕_-+
-- | v |
-- p--@--p
-- | v |
-- +-a⊕_-+
--
right :: Choice p => Square '[p] '[p] '[Either a] '[Either a]
-- |
-- +-a→_-+
-- | v |
-- p--@--p
-- | v |
-- +-a→_-+
--
closed :: Closed p => Square '[p] '[p] '[(->) a] '[(->) a]
-- |
-- +--f--+
-- | v |
-- p--@--p
-- | v |
-- +--f--+
--
map :: (Mapping p, Functor f) => Square '[p] '[p] '[f] '[f]
-- |
-- +-----+
-- | |
-- (→)-@ |
-- | |
-- +-----+
--
fromHom :: Square '[(->)] '[] '[] '[]
-- |
-- +-----+
-- | |
-- | @-(→)
-- | |
-- +-----+
--
toHom :: Square '[] '[(->)] '[] '[]
-- |
-- +-----+
-- | /-p
-- q.p-@ |
-- | \-q
-- +-----+
--
fromProcompose :: (Profunctor p, Profunctor q) => Square '[Procompose q p] '[p, q] '[] '[]
-- |
-- +-----+
-- p-\ |
-- | @-q.p
-- q-/ |
-- +-----+
--
toProcompose :: (Profunctor p, Profunctor q) => Square '[p, q] '[Procompose q p] '[] '[]
module Control.Monad.Square
-- |
-- +-----+
-- | |
-- | R->m
-- | |
-- +-----+
--
return :: Monad m => Square '[] '[Star m] '[] '[]
-- |
-- +--m--+
-- | v |
-- m>-B |
-- | v |
-- +--m--+
--
--
-- `(>>=)`
--
-- Left identity law:
--
--
-- +-------+
-- | R>-\ + +-----+
-- | v | | |
-- m>---B | === m>-\ |
-- | v | | v |
-- +----m--+ +--m--+
--
--
-- Right identity law:
--
--
-- +----m--+ +--m--+
-- | v | | | |
-- | R>-B | === | v |
-- | v | | | |
-- +----m--+ +--m--+
--
--
-- Associativity law:
--
--
-- +--m--+ +-----m--+
-- | v | m>-\ v |
-- m>-B | | v | |
-- | v | === m>-B | |
-- m>-B | | \->B |
-- | v | | v |
-- +--m--+ +-----m--+
--
bind :: Monad m => Square '[Star m] '[] '[m] '[m]
-- |
-- +-m-m-+
-- | v v |
-- | \-@ |
-- | v |
-- +---m-+
--
--
--
-- join = toRight ||| bind
--
join :: Monad m => Square '[] '[] '[m, m] '[m]
-- |
-- +-----+
-- m>-\ |
-- m>-@ |
-- | \->m
-- +-----+
--
--
-- Kleisli composition `(M.>=>)`
kleisli :: Monad m => Square '[Star m, Star m] '[Star m] '[] '[]