squares (empty) → 0

raw patch · 11 files changed

+767/−0 lines, 11 filesdep +basedep +profunctorssetup-changed

Dependencies added: base, profunctors

Files

CHANGELOG.md +5/−0
LICENSE +30/−0
Setup.hs +2/−0
squares.cabal +30/−0
src/Control/Monad/Square.hs +84/−0
src/Data/Functor/Compose/List.hs +56/−0
src/Data/Profunctor/Composition/List.hs +48/−0
src/Data/Profunctor/Square.hs +94/−0
src/Data/Square.hs +337/−0
src/Data/Traversable/Square.hs +62/−0
src/Data/Type/List.hs +19/−0

+ CHANGELOG.md view

@@ -0,0 +1,5 @@+# Revision history for squares++## 0 -- 2020-05-22++* First version. Released on an unsuspecting world.

+ LICENSE view

@@ -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.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ squares.cabal view

@@ -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

+ src/Control/Monad/Square.hs view

@@ -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

+ src/Data/Functor/Compose/List.hs view

@@ -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

+ src/Data/Profunctor/Composition/List.hs view

@@ -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)

+ src/Data/Profunctor/Square.hs view

@@ -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)))

+ src/Data/Square.hs view

@@ -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 '()

+ src/Data/Traversable/Square.hs view

@@ -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

+ src/Data/Type/List.hs view

@@ -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)