summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSjoerdVisscher <>2020-05-22 17:53:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2020-05-22 17:53:00 (GMT)
commit4df454b9864583105233d22792c902423c7c7304 (patch)
treea7bf6b4c833c307551b58180b9e20c974f44c234
version 00
-rwxr-xr-xCHANGELOG.md5
-rw-r--r--LICENSE30
-rw-r--r--Setup.hs2
-rw-r--r--squares.cabal30
-rw-r--r--src/Control/Monad/Square.hs84
-rw-r--r--src/Data/Functor/Compose/List.hs56
-rw-r--r--src/Data/Profunctor/Composition/List.hs48
-rw-r--r--src/Data/Profunctor/Square.hs94
-rw-r--r--src/Data/Square.hs337
-rw-r--r--src/Data/Traversable/Square.hs62
-rw-r--r--src/Data/Type/List.hs19
11 files changed, 767 insertions, 0 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100755
index 0000000..2120715
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for squares
+
+## 0 -- 2020-05-22
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..12c0356
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2020, Sjoerd Visscher
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above
+ copyright notice, this list of conditions and the following
+ disclaimer in the documentation and/or other materials provided
+ with the distribution.
+
+ * Neither the name of Sjoerd Visscher nor the names of other
+ contributors may be used to endorse or promote products derived
+ from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/squares.cabal b/squares.cabal
new file mode 100644
index 0000000..67dfed0
--- /dev/null
+++ b/squares.cabal
@@ -0,0 +1,30 @@
+cabal-version: >=1.10
+
+name: squares
+version: 0
+synopsis: The double category of Hask functors and profunctors
+homepage: https://github.com/sjoerdvisscher/squares
+bug-reports: https://github.com/sjoerdvisscher/squares/issues
+license: BSD3
+license-file: LICENSE
+author: Sjoerd Visscher
+maintainer: sjoerd@w3future.com
+category: Math
+build-type: Simple
+extra-source-files: CHANGELOG.md
+
+library
+ exposed-modules: Data.Square
+ Data.Type.List
+ Data.Functor.Compose.List
+ Data.Profunctor.Composition.List
+ Data.Profunctor.Square
+ Data.Traversable.Square
+ Control.Monad.Square
+ build-depends: base == 4.*, profunctors == 5.*
+ hs-source-dirs: src
+ default-language: Haskell2010
+
+source-repository head
+ type: git
+ location: git://github.com/sjoerdvisscher/squares.git
diff --git a/src/Control/Monad/Square.hs b/src/Control/Monad/Square.hs
new file mode 100644
index 0000000..516e49b
--- /dev/null
+++ b/src/Control/Monad/Square.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE DataKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : Control.Monad.Square
+-- License : BSD-style (see the file LICENSE)
+-- Maintainer : sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Control.Monad.Square where
+
+import Prelude hiding (return)
+import Data.Square
+import Data.Profunctor
+import Data.Profunctor.Square
+import qualified Control.Monad as M
+
+-- |
+-- > +-----+
+-- > | |
+-- > | R->m
+-- > | |
+-- > +-----+
+return :: Monad m => Square '[] '[Star m] '[] '[]
+return = toHom ||| proNat (Star . (M.return .))
+
+-- |
+-- > +--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]
+bind = mkSquare (flip (>>=) . runStar) ||| fromHom
+
+-- |
+-- > +-m-m-+
+-- > | v v |
+-- > | \-@ |
+-- > | v |
+-- > +---m-+
+--
+-- @join = toRight ||| bind@
+join :: Monad m => Square '[] '[] '[m, m] '[m]
+join = toRight ||| bind
+
+-- |
+-- > +-----+
+-- > m>-\ |
+-- > m>-@ |
+-- > | \->m
+-- > +-----+
+--
+-- Kleisli composition `(M.>=>)`
+kleisli :: Monad m => Square '[Star m, Star m] '[Star m] '[] '[]
+kleisli = fromLeft === bind === toRight
diff --git a/src/Data/Functor/Compose/List.hs b/src/Data/Functor/Compose/List.hs
new file mode 100644
index 0000000..067ac99
--- /dev/null
+++ b/src/Data/Functor/Compose/List.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : Data.Functor.Compose.List
+-- License : BSD-style (see the file LICENSE)
+-- Maintainer : sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Data.Functor.Compose.List where
+
+import Data.Type.List
+
+-- | N-ary composition of functors.
+--
+-- > FList '[] a ~ a
+-- > FList '[f, g, h] a ~ h (g (f a))
+data FList (fs :: [* -> *]) (a :: *) where
+ Id :: { unId :: a } -> FList '[] a
+ F :: { unF :: f a } -> FList '[f] a
+ FComp :: { unFComp :: FList (g ': gs) (f a) } -> FList (f ': g ': gs) a
+
+instance Functor (FList '[]) where
+ fmap f = Id . f . unId
+instance Functor f => Functor (FList '[f]) where
+ fmap f = F . fmap f . unF
+instance (Functor f, Functor (FList (g ': gs))) => Functor (FList (f ': g ': gs)) where
+ fmap f = FComp . fmap (fmap f) . unFComp
+
+
+-- | Combining and splitting nested `FList`s.
+class FAppend f where
+ fappend :: Functor (FList g) => FList g (FList f a) -> FList (f ++ g) a
+ funappend :: Functor (FList g) => FList (f ++ g) a -> FList g (FList f a)
+instance FAppend '[] where
+ fappend = fmap unId
+ funappend = fmap Id
+instance FAppend '[f] where
+ fappend (Id fa) = F (unF fa)
+ fappend f@F{} = FComp $ fmap unF f
+ fappend f@FComp{} = FComp $ fmap unF f
+ funappend fa@F{} = Id fa
+ funappend (FComp fga@F{}) = fmap F fga
+ funappend (FComp fga@FComp{}) = fmap F fga
+instance (Functor f, FAppend (g ': gs)) => FAppend (f ': g ': gs) where
+ fappend = FComp . fappend . fmap unFComp
+ funappend = fmap FComp . funappend . unFComp
+
+
+-- | Natural transformations between two functors. (Why is this still not in base??)
+type f ~> g = forall a. f a -> g a
diff --git a/src/Data/Profunctor/Composition/List.hs b/src/Data/Profunctor/Composition/List.hs
new file mode 100644
index 0000000..d978eff
--- /dev/null
+++ b/src/Data/Profunctor/Composition/List.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : Data.Profunctor.Composition.List
+-- License : BSD-style (see the file LICENSE)
+-- Maintainer : sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Data.Profunctor.Composition.List where
+
+import Data.Profunctor
+import Data.Profunctor.Composition
+import Data.Type.List
+
+-- | N-ary composition of profunctors.
+data PList (ps :: [* -> * -> *]) (a :: *) (b :: *) where
+ 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
+
+instance Profunctor (PList '[]) where
+ dimap l r (Hom f) = Hom (r . f . l)
+instance Profunctor p => Profunctor (PList '[p]) where
+ dimap l r (P p) = P (dimap l r p)
+instance (Profunctor p, Profunctor (PList (q ': qs))) => Profunctor (PList (p ': q ': qs)) where
+ dimap l r (PComp p ps) = PComp (lmap l p) (rmap r ps)
+
+-- | Combining and splitting nested `PList`s.
+class PAppend p where
+ pappend :: Profunctor (PList q) => Procompose (PList q) (PList p) a b -> PList (p ++ q) a b
+ punappend :: PList (p ++ q) a b -> Procompose (PList q) (PList p) a b
+instance PAppend '[] where
+ pappend (Procompose q (Hom f)) = lmap f q
+ punappend q = Procompose q (Hom id)
+instance Profunctor p => PAppend '[p] where
+ pappend (Procompose (Hom f) (P p)) = P (rmap f p)
+ pappend (Procompose q@P{} (P p)) = PComp p q
+ pappend (Procompose q@PComp{} (P p)) = PComp p q
+ punappend p@P{} = Procompose (Hom id) p
+ punappend (PComp p qs) = Procompose qs (P p)
+instance (Profunctor p, PAppend (q ': qs)) => PAppend (p ': q ': qs) where
+ pappend (Procompose q (PComp p ps)) = PComp p (pappend (Procompose q ps))
+ punappend (PComp p pq) = case punappend pq of Procompose q ps -> Procompose q (PComp p ps)
diff --git a/src/Data/Profunctor/Square.hs b/src/Data/Profunctor/Square.hs
new file mode 100644
index 0000000..deae048
--- /dev/null
+++ b/src/Data/Profunctor/Square.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : Data.Profunctor.Square
+-- License : BSD-style (see the file LICENSE)
+-- Maintainer : sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Data.Profunctor.Square where
+
+import Data.Square
+import Data.Functor.Compose.List
+import Data.Profunctor.Composition.List
+import qualified Data.Profunctor as P
+import Data.Profunctor.Composition
+
+-- * Squares for profunctor subclasses
+
+-- |
+-- > +-a⊗_-+
+-- > | v |
+-- > p--@--p
+-- > | v |
+-- > +-a⊗_-+
+second :: P.Strong p => Square '[p] '[p] '[(,) a] '[(,) a]
+second = mkSquare P.second'
+
+-- |
+-- > +-a⊕_-+
+-- > | v |
+-- > p--@--p
+-- > | v |
+-- > +-a⊕_-+
+right :: P.Choice p => Square '[p] '[p] '[Either a] '[Either a]
+right = mkSquare P.right'
+
+-- |
+-- > +-a→_-+
+-- > | v |
+-- > p--@--p
+-- > | v |
+-- > +-a→_-+
+closed :: P.Closed p => Square '[p] '[p] '[(->) a] '[(->) a]
+closed = mkSquare P.closed
+
+-- |
+-- > +--f--+
+-- > | v |
+-- > p--@--p
+-- > | v |
+-- > +--f--+
+map :: (P.Mapping p, Functor f) => Square '[p] '[p] '[f] '[f]
+map = mkSquare P.map'
+
+-- * Squares for @(->)@
+
+-- |
+-- > +-----+
+-- > | |
+-- > (→)-@ |
+-- > | |
+-- > +-----+
+fromHom :: Square '[(->)] '[] '[] '[]
+fromHom = Square (Hom . P.dimap unId Id . unP)
+
+-- |
+-- > +-----+
+-- > | |
+-- > | @-(→)
+-- > | |
+-- > +-----+
+toHom :: Square '[] '[(->)] '[] '[]
+toHom = Square (P . P.dimap unId Id . unHom)
+
+-- * Squares for `Procompose`
+
+-- |
+-- > +-----+
+-- > | /-p
+-- > q.p-@ |
+-- > | \-q
+-- > +-----+
+fromProcompose :: (P.Profunctor p, P.Profunctor q) => Square '[Procompose q p] '[p, q] '[] '[]
+fromProcompose = Square ((\(Procompose q p) -> PComp (P.lmap unId p) (P (P.rmap Id q))) . unP)
+
+-- |
+-- > +-----+
+-- > p-\ |
+-- > | @-q.p
+-- > q-/ |
+-- > +-----+
+toProcompose :: (P.Profunctor p, P.Profunctor q) => Square '[p, q] '[Procompose q p] '[] '[]
+toProcompose = Square (P . (\(PComp p (P q)) -> Procompose (P.rmap Id q) (P.lmap unId p)))
diff --git a/src/Data/Square.hs b/src/Data/Square.hs
new file mode 100644
index 0000000..7aa6dea
--- /dev/null
+++ b/src/Data/Square.hs
@@ -0,0 +1,337 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE FlexibleContexts #-}
+#if __GLASGOW_HASKELL__ >= 810
+{-# LANGUAGE StandaloneKindSignatures #-}
+#endif
+-----------------------------------------------------------------------------
+-- |
+-- Module : Data.Square
+-- License : BSD-style (see the file LICENSE)
+-- Maintainer : sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+
+module Data.Square where
+
+import Data.Functor.Compose.List
+import Data.Profunctor
+import qualified Data.Profunctor.Composition as P
+import Data.Profunctor.Composition.List
+import Data.Type.List
+#if __GLASGOW_HASKELL__ >= 810
+import Data.Kind
+#endif
+
+-- * Double category
+
+-- $doubleCategory
+-- There is a double category of Haskell functors and profunctors.
+--
+-- The squares in this double category are natural transformations.
+
+-- |
+-- > +-----+
+-- > | |
+-- > | |
+-- > | |
+-- > +-----+
+--
+-- > forall a b. (a -> b) -> (a -> b)
+--
+-- The empty square is the identity transformation.
+emptySquare :: Square '[] '[] '[] '[]
+emptySquare = Square $ dimap unId Id
+
+-- |
+-- > +-----+
+-- > | |
+-- > 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] '[] '[]
+proId = Square $ dimap unId Id
+
+-- |
+-- > +--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]
+funId = Square \(Hom f) -> Hom (fmap 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 `fmap`ping before or after.
+-- (It doesn't matter which, because of naturality!)
+funNat :: (Functor f, Functor g) => (f ~> g) -> Square '[] '[] '[f] '[g]
+funNat n = Square $ Hom . dimap unF F . (.) n . fmap . unHom
+
+-- |
+-- > +-----+
+-- > | |
+-- > 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] '[] '[]
+proNat n = Square $ P . dimap unId Id . n . unP
+
+-- |
+-- > +--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.
+#if __GLASGOW_HASKELL__ >= 810
+type SquareNT :: (a -> b -> Type) -> (c -> d -> Type) -> (a -> c) -> (b -> d) -> Type
+#endif
+newtype SquareNT p q f g = Square { unSquare :: 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]
+mkSquare f = Square (P . dimap unF F . f . unP)
+
+-- |
+-- > +--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 `(|||)`.
+infixl 6 |||
+(|||) :: (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) -- ^
+Square pq ||| Square qr = Square $ dimap funappend fappend . qr . pq
+
+-- |
+-- > +--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 `(===)`.
+infixl 5 ===
+(===) :: (PAppend ps, PAppend qs, Profunctor (PList ss))
+ => Square ps qs fs gs -> Square rs ss gs hs -> Square (ps ++ rs) (qs ++ ss) fs hs -- ^
+Square pq === Square rs = Square \pr -> case punappend pr of P.Procompose r p -> pappend (P.Procompose (rs r) (pq p))
+
+
+-- * Proarrow equipment
+--
+-- $proarrowEquipment
+-- The double category of haskell functors and profunctors is a proarrow equipment.
+-- Which means that we can "bend" functors to become profunctors.
+
+-- |
+-- > +--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] '[]
+toRight = Square \(Hom f) -> P (Star (fmap (Id . f) . unF))
+
+-- |
+-- > +--f--+
+-- > | v |
+-- > f<-/ |
+-- > | |
+-- > +-----+
+--
+-- A functor @f@ can be bent to the left to become the profunctor @`Costar` f@.
+toLeft :: Square '[Costar f] '[] '[f] '[]
+toLeft = Square \(P (Costar f)) -> Hom (Id . f . unF)
+
+-- |
+-- > +-----+
+-- > | |
+-- > | /-<f
+-- > | v |
+-- > +--f--+
+--
+-- The profunctor @`Costar` f@ can be bent down to become the functor @f@ again.
+fromRight :: Functor f => Square '[] '[Costar f] '[] '[f]
+fromRight = Square \(Hom f) -> P (Costar (F . fmap (f . unId)))
+
+-- |
+-- > +-----+
+-- > | |
+-- > f>-\ |
+-- > | v |
+-- > +--f--+
+--
+-- The profunctor @`Star` f@ can be bent down to become the functor @f@ again.
+fromLeft :: Square '[Star f] '[] '[] '[f]
+fromLeft = Square \(P (Star f)) -> Hom (F . f . unId)
+
+-- |
+-- > +-----+
+-- > 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] '[] '[] '[]
+uLeft =
+ fromLeft
+ ===
+ toLeft
+
+-- |
+-- > +-----+
+-- > | /-<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] '[] '[]
+uRight =
+ fromRight
+ ===
+ toRight
+
+-- |
+-- > +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 =
+ fromLeft ||| funId ||| fromRight
+ ===
+ n
+ ===
+ toLeft ||| funId ||| toRight
+
+-- |> 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] -- ^
+spiderLemma' n = (toRight === proId === fromRight) ||| n ||| (toLeft === proId === fromLeft)
+
+-- * In other categories than Hask
+
+-- $otherCategories
+-- > 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.
+
+-- |
+-- > 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 where
+ (:**:) :: 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
+#if __GLASGOW_HASKELL__ >= 810
+type UncurryF :: (a -> b -> Type) -> (a, b) -> Type
+#endif
+data UncurryF f a where
+ 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 where
+ Unit :: Unit '() '()
+
+-- | Values as a functor from the unit category.
+data ValueF x u where
+ ValueF :: a -> ValueF a '()
diff --git a/src/Data/Traversable/Square.hs b/src/Data/Traversable/Square.hs
new file mode 100644
index 0000000..2171ac6
--- /dev/null
+++ b/src/Data/Traversable/Square.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE DataKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : Data.Traversable.Square
+-- License : BSD-style (see the file LICENSE)
+-- Maintainer : sjoerd@w3future.com
+--
+-----------------------------------------------------------------------------
+module Data.Traversable.Square where
+
+import Prelude hiding (traverse)
+import Data.Square
+import Data.Profunctor
+import qualified Data.Traversable as T
+
+-- |
+-- > +--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]
+traverse = mkSquare (Star . T.traverse . runStar)
+
+-- |
+-- > +-f-t---+
+-- > | v v |
+-- > | \-@-\ |
+-- > | v v |
+-- > +---t-f-+
+--
+-- @sequence = toRight ||| traverse ||| fromLeft@
+sequence :: (Traversable t, Applicative f) => Square '[] '[] '[f, t] '[t, f]
+sequence = toRight ||| traverse ||| fromLeft
diff --git a/src/Data/Type/List.hs b/src/Data/Type/List.hs
new file mode 100644
index 0000000..66c0a6b
--- /dev/null
+++ b/src/Data/Type/List.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : Data.Type.List
+-- License : BSD-style (see the file LICENSE)
+-- Maintainer : sjoerd@w3future.com
+--
+-- Utilities for type level lists.
+-----------------------------------------------------------------------------
+module Data.Type.List where
+
+-- | Type level list append
+type family (as :: [k]) ++ (bs :: [k]) :: [k] where
+ '[] ++ bs = bs
+ (a ': as) ++ bs = a ': (as ++ bs)