categorical-algebra (empty) → 0.0.0.1

raw patch · 4 files changed

+711/−0 lines, 4 filesdep +basedep +newtypedep +pointless-haskellsetup-changed

Dependencies added: base, newtype, pointless-haskell, void

Files

LICENSE +30/−0
Setup.hs +2/−0
categorical-algebra.cabal +62/−0
src/Data/Semiring.lhs +617/−0

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c)2012, Jonathan Fischoff++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 Jonathan Fischoff 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

+ categorical-algebra.cabal view

@@ -0,0 +1,62 @@+-- categorical-algebra.cabal auto-generated by cabal init. For+-- additional options, see+-- http://www.haskell.org/cabal/release/cabal-latest/doc/users-guide/authors.html#pkg-descr.+-- The name of the package.+Name:                categorical-algebra++-- The package version. See the Haskell package versioning policy+-- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for+-- standards guiding when and how versions should be incremented.+Version:             0.0.0.1++-- A short (one-line) description of the package.+Synopsis:            Categorical Monoids and Semirings++-- A longer description of the package.+Description: This my attempt at synthesizing a few ideas about invertible programming with Arrow like type classes. Here is a link to pdf produced from the source <https://takeittothelimit.files.wordpress.com/2012/03/semiring.pdf> And here is a blog post that says basically the same thing. <http://takeittothelimit.wordpress.com/2012/03/26/categorical-semirings-2/>++-- The license under which the package is released.+License:             BSD3++-- The file containing the license text.+License-file:        LICENSE++-- The package author(s).+Author:              Jonathan Fischoff++-- An email address to which users can send suggestions, bug reports,+-- and patches.+Maintainer:          jonathangfischoff@gmail.com++-- A copyright notice.+-- Copyright:           ++Category:            Data++Build-type:          Simple++-- Extra files to be distributed with the package, such as examples or+-- a README.+-- Extra-source-files:  ++-- Constraint on the version of Cabal needed to build this package.+Cabal-version:       >=1.2+++Library+  Hs-Source-Dirs: src+  -- Modules exported by the library.+  Exposed-modules:     Data.Semiring+  +  -- Packages needed in order to build this package.+  Build-depends:  base > 4.0.0 && <= 5.0,    +                  newtype >= 0.2,+                  pointless-haskell >= 0.0.8,+                  void >= 0.5.5++  GHC-options:       -Wall+  +  -- Modules not exported by this package.+  -- Other-modules:       +  +

+ src/Data/Semiring.lhs view

@@ -0,0 +1,617 @@+\documentclass{article}+\usepackage{fge}+\usepackage{mathabx}+\usepackage{hyperref}+\usepackage{marvosym}+%include polycode.fmt+\begin{document}++\title{Fly Like an Arrow}+\author{Jonathan Fischoff \hskip 2pt \Letter \hskip 4pt \<jonathangfischoff\MVAt gmail.com\>}+\maketitle   +The great thing about {\tt Arrows} is you can write code that works for morphisms in different categories. For example, you can write code for functions and later use monad actions, or Kleisli arrows, instead. This is useful for error handling, and of course, adding {\tt IO}.++If the underlying category uses isomorphisms (things with inverses) exclusively then it is called a {\sl groupoid}. Groupoids cause cracks to show in the {\tt Arrow} abstraction. {\tt Arrow} assumes that you can lift any function into the category you are writing code for, by requiring a definition for @arr :: (b -> c) -> a b c@ function. This is out for groupoids, because not all functions are isomorphisms.+ +To remedy this, among other issues, Adam Megacz came up with. \href{http://arxiv.org/pdf/1007.2885v2.pdf}{Generalized Arrows.}. ++In \href{https://www.cs.indiana.edu/~rpjames/papers/rc.pdf}{\sl Dagger Traced Symmetric Monoidal Categories and Reversible Programming} the authors show how to construct an reversible language out of the sum and product types along with related combinators to form a commutative semiring, at the type level. Both approaches are similar.++Error handling and \href{http://www.informatik.uni-marburg.de/~rendel/rendel10invertible.pdf}{\sl partial isomorphisms} are possible with Generalized Arrows. However, I find the algebraic approach of {\sl DTSMCRP} more elegant. So I am going to try to get the same combinators as {\sl DTSMCRP} but for an arbitrary category, as I would with Generalized Arrows.+ +This is a Literate Haskell file, which means it can be executed as Haskell code. First, I need to start with a simple Haskell preamble.+\begin{code}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeSynonymInstances   #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FlexibleContexts       #-}    +-- |Categorical semirings (my term, but maybe the correct one) are an alternative to Arrows, but play nicely with groupoids. | +--  See the source or the latex source for more background.+module Data.Semiring (+        -- * Endofunctors for construction+          Ctor(..)+        -- ** first/right like functions+        , promote+        , swap_promote+        -- * Laws (Axioms) for building algebraic structures+        , Absorbs(..)+        , Assocative(..)+        , Commutative(..)+        , Annihilates(..)+        , Distributes(..)+        -- * Categorical Algebraic Structures+        , Monoidial+        , CommutativeMonoidial+        , Semiring+        -- * Arrow like functions for semiring categories+        , first+        , second+        , left+        , right+        -- * A groupoid class that is a category. Maybe this is a bad idea?+        , Groupoid(..)+        , Iso(..)+        -- * Alegraic laws as isomorphism for groupoid instances+        , biject_sum_absorb+        , biject_sum_assoc+        , biject_product_absorb+        , biject_product_assoc+        , biject_distributes+        , kbiject_sum_absorb+        , kbiject_sum_assoc+        , kbiject_product_absorb+        , kbiject_product_assoc+        , kbiject_distributes+    ) where  +import Prelude hiding ((.), id)+import Control.Category ((.), id, Category(..))+import Data.Void(Void) +import Control.Arrow (Kleisli(..))   +import Generics.Pointless.MonadCombinators (mfuse)+import Control.Monad (liftM)+import Control.Newtype+\end{code}+\newpage+++\noindent I start with an abstraction for both sum and product constructors.++\begin{code}+-- |An endofunctor for combining two morphisms|+class Category k => Ctor k constr | constr -> k where+    selfmap :: k a b -> k c d -> k (constr a c) (constr b d)  +\end{code}++\noindent With Ctor I can write a generic {\tt first} or {\tt left}++\begin{code}+-- |construct a new morphism with identity|+promote :: Ctor k op => k a b -> k (op a c) (op b c)+promote = flip selfmap id++-- |construct a new morphism with identity with the arguments reversed|+swap_promote :: Ctor k op => k a b -> k (op c a) (op c b)+swap_promote = selfmap id+\end{code}++It is probably not clear at this point but depending on the type of {\sl op} we can get either the {\tt Arrow} $\ast\ast\ast$ or the {\tt ArrowChoice} $\interleave$ function. If we make a semiring we can get them both. That's what we are going to do.++I use type classes to encode the algebraic laws of semirings, with a class per law.+%format \<-\> = "\leftrightarrow "+\vskip 5pt+\begin{code}+-- |The absorbtion law => x+0 \<-\> x |+class Ctor k op => Absorbs k op id | op -> k, op -> id where+    absorb   :: k (op id a) a+    unabsorb :: k a (op id a)+\end{code}+\begin{code}+-- |The commutative law => x + y \<-\> y + x|+class Ctor k op => Commutative k op | op -> k where    +    commute  :: k (op a b) (op b a)    +\end{code}  +\begin{code}+-- |The assocative law => (x + y) + z \<-\> x + (y + z)|+class Ctor k op => Assocative k op | op -> k where+    assoc    :: k (op (op a b) c) (op a (op b c)) +    unassoc  :: k (op a (op b c)) (op (op a b) c)+\end{code}    +\begin{code}    +-- |The annihilation law => 0 * x \<-\> 0|+class Ctor k op => Annihilates k op zero | op zero -> k where+    annihilates   :: k (op zero a) zero    +\end{code}    +\begin{code}  +-- |The distribution law => (a + b) * c \<-\> (a * c) + (b * c)|+class (Ctor k add, Ctor k multi) => Distributes k add multi | add multi -> k where+    distribute   :: k (multi (add a b) c) (add (multi a c) (multi b c))    +    undistribute :: k (add (multi a c) (multi b c)) (multi (add a b) c)+\end{code}++I collect these into groups of laws to make different algebraic structures.++\begin{code}+-- |Monoidial Category class|+class (Assocative k dot, Absorbs k dot id)  => +      Monoidial k dot id | dot id -> k where+\end{code}+\begin{code}+-- |Commutative Monoidial Category class|          +class (Monoidial k dot id, Commutative k dot) => +      CommutativeMonoidial k dot id | dot id -> k where +\end{code}+\begin{code}+-- |Semiring Category class|        +class (CommutativeMonoidial k add zero, +       CommutativeMonoidial k multi one, +       Annihilates k multi zero, +       Distributes k add multi) => +       Semiring k add zero multi one | add zero multi one -> k where+\end{code}++From which I regain {\tt Arrow} and {\tt ArrowChoice} functionality. Although, because of {\tt promote}, I already had this capability.++\begin{code}+-- |Apply the multi monoid operator to the morphism and identity|+first :: Semiring a add zero multi one => a b c -> a (multi b d) (multi c d)+first = promote+-- |Apply the multi monoid operator to identity and the morphism|+second :: Semiring a add zero multi one => a b c -> a (multi d b) (multi d c)+second = swap_promote+-- |Apply the add monoid operator to the morphism and identity|+left :: Semiring a add zero multi one => a b c -> a (add b d) (add c d)+left = promote+-- |Apply the add monoid operator to identity and the morphism|+right :: Semiring a add zero multi one => a b c -> a (add d b) (add d c)+right = swap_promote+\end{code}++Many of the Generic Arrow functions can be included through absorption ({\tt cancel}, {\tt uncancel}) and commutativity ({\tt swap}). I'm not interested in adding looping at this point.++This also makes clear the relationship between {\tt Arrow} and {\tt ArrowChoice} as has been noted else where. Basically the same thing with a different endofunctor or constructor ({\tt Arrow} uses product types, {\tt ArrowChoice} uses sum types) as the monoid operator of a type level commutative monoid. ++Making instances is a little onerous because of the use of multiparameter classes and the functional dependencies I have chosen. When I begin actually using these classes, it could result in massive changes. I am open to any suggestions on better designs.++\newpage++The rest of the code is basically boilerplate. I used Djinn to write some of the functions (hopefully they work :)).++\section{Small Category Instances}+\subsection{Function Instances}+\subsubsection{Sum Commutative Monoid Instances}++%format Sum = "\bigplus "+%format Zero = "\MVZero "+\begin{code}+--Sugar+type Sum = Either+type Zero  = Void+--Instances    +instance Ctor (->) Sum where+    selfmap f g = either (Left . f) (Right . g)+    +instance Absorbs (->) Sum Zero where+    absorb  (Right x) = x+    absorb  _ = error "Absorbs,->,Sum,Zero Semiring.lhs absorb:impossible!" +    unabsorb = Right+    +instance Assocative (->) Sum where+    assoc   = either (either Left (Right . Left)) (Right . Right)+    unassoc = either (Left . Left) (either (Left . Right) Right)+    +instance Monoidial (->) Sum Zero where++instance Commutative (->) Sum where+    commute = either Right Left+ +instance CommutativeMonoidial (->) Sum Zero where    +\end{code}++\subsubsection{Product Commutative Monoid Instances}++%format Product = "\ast "+%format One = "\MVOne "+\begin{code}+type Product = (,)+type One  = ()+--Instances    +instance Ctor (->) Product where+    selfmap f g (x, y) = (f x, g y)+    +instance Absorbs (->) Product One where+    absorb  ((), x) = x +    unabsorb x = ((), x)+    +instance Assocative (->) Product where+    assoc   ((x, y), z) = (x, (y, z)) +    unassoc (x, (y, z)) = ((x, y), z)+    +instance Monoidial (->) Product One where++instance Commutative (->) Product where+    commute (x, y) = (y, x)+ +instance CommutativeMonoidial (->) Product One where+\end{code}++\subsubsection{Function Semiring Instance}++\begin{code}+instance Annihilates (->) Product Zero where+    annihilates   (_, _) = undefined++instance Distributes (->) Sum Product where+    distribute (Left x, z)  = Left (x, z)+    distribute (Right y, z) = Right (y, z) +    +    undistribute (Left (x, z))  = (Left x, z)+    undistribute (Right (y, z)) = (Right y, z)+    +instance Semiring (->) Sum Zero Product One where+\end{code}++\subsection{Kleisli Instances}++The functional dependencies of the classes require alternate versions of the sum and product types used for \to instances. ++%format KSum = "\bigplus "+%format KZero = "\MVZero "++\subsection{Sum Commutative Monoid Instances}+\begin{code}+data KSum a b = KLeft a | KRight b+newtype KZero = KZ Void+--Instances    +instance Monad m => Ctor (Kleisli m) KSum where+    selfmap (Kleisli f) (Kleisli g) = Kleisli $ +        \e -> case e of+            KLeft  x -> KLeft `liftM`  f x+            KRight x -> KRight `liftM` g x+    +instance Monad m => Absorbs (Kleisli m) KSum KZero where+    absorb   = Kleisli $ \e -> case e of+        KRight x -> return x +        _ -> error "Absorbs,Kleisli,KSum,KZero Semiring.lhs absorb:impossible!" +    unabsorb = Kleisli $ \x -> return $ KRight x+    +instance Monad m => Assocative (Kleisli m) KSum where+    assoc   = Kleisli $ \e -> case e of+                KLeft x  -> case x of+                              KLeft  y -> return $ KLeft y+                              KRight y -> return $ KRight $ KLeft y+                KRight x -> return $ KRight $ KRight x++    unassoc = Kleisli $ \e -> case e of+                KLeft  x -> return $ KLeft $ KLeft x+                KRight x -> case x of+                              KLeft y  -> return $ KLeft $ KRight y+                              KRight y -> return $ KRight y    +    +instance Monad m => Monoidial (Kleisli m) KSum KZero where++instance Monad m => Commutative (Kleisli m) KSum where+    commute = Kleisli $ \e -> case e of+                        KLeft x  -> return $ KRight x+                        KRight x -> return $ KLeft x+ +instance Monad m => CommutativeMonoidial (Kleisli m) KSum KZero where    +\end{code}++%format KProduct = "\ast "+%format KOne = "\MVOne "+\subsubsection{Product Commutative Monoid Instances}+\begin{code}+data KProduct a b = KP a b+newtype KOne  = KO ()+--Instances    +instance Monad m => Ctor (Kleisli m) KProduct where+    selfmap (Kleisli f) (Kleisli g) = Kleisli $ +                        \(KP x y) -> uncurry KP `liftM` mfuse (f x, g y)+    +instance Monad m => Absorbs (Kleisli m) KProduct KOne where+    absorb   = Kleisli $ \(KP (KO ()) x) -> return x +    unabsorb = Kleisli $ \x -> return $ KP (KO ()) x+    +instance Monad m => Assocative (Kleisli m) KProduct where+    assoc   = Kleisli $ \(KP (KP x y) z) -> return $ KP x (KP y z) +    unassoc = Kleisli $ \(KP x (KP y z)) -> return $ KP (KP x y) z+    +instance Monad m => Monoidial (Kleisli m) KProduct KOne where++instance Monad m => Commutative (Kleisli m) KProduct where+    commute = Kleisli $ \(KP x y) -> return $ KP y x+ +instance Monad m => CommutativeMonoidial (Kleisli m) KProduct KOne where+\end{code}++\subsubsection{Function Semiring Instance}++\begin{code}+instance Monad m => Annihilates (Kleisli m) KProduct KZero where+    annihilates  = Kleisli $ \(KP _ _) -> return undefined++instance Monad m => Distributes (Kleisli m) KSum KProduct where+    distribute = Kleisli $ \e -> case e of+               KP (KLeft x) z ->  return $ KLeft $  KP x z+               KP (KRight y) z -> return $ KRight $ KP y z +    +    undistribute = Kleisli $ \e -> case e of+        KLeft  (KP x z) -> return $ KP (KLeft x)   z+        KRight (KP x z) -> return $ KP (KRight x)  z+    +instance Monad m => Semiring (Kleisli m) KSum KZero KProduct KOne where+\end{code}+++\section{Groupoid Class}+\begin{code}+class (Category g) => Groupoid g where  +    inv :: g a b -> g b a+\end{code}+\section{Groupoid Instances}+\begin{code}+data Iso k a b = Iso {+        embed   :: k a b,+        project :: k b a+    }++instance (Category k) => Category (Iso k) where+    id  = Iso id id+    (Iso f g) . (Iso h i) = Iso (f . h) (i . g)+    +instance Newtype (Iso k a b) (k a b, k b a) where+    pack (f, g)        = Iso f g+    unpack (Iso f g)   = (f, g)+    +instance (Category k) => Groupoid (Iso k) where+    inv (Iso f g) = Iso g f+\end{code} +\subsection{Helper Code}+\begin{code}+type Biject    = Iso (->)+type KBiject m = Iso (Kleisli m) ++(<->) :: k a b -> k b a -> Iso k a b+(<->) = Iso+\end{code}+\subsection{Groupoid Semirings Instances}+\subsection{Groupoid with a Function as the base category}+\subsubsection{Sum Commutative Monoid Instances}+%format BSum = "\bigplus "+%format BZero = "\MVZero "+\begin{code}+data  BSum a b = BLeft a | BRight b+newtype BZero = BZ Void+    +instance Ctor Biject BSum where+    selfmap f g = fw <-> bk where+        fw (BLeft x)  = BLeft  $ embed f x+        fw (BRight x) = BRight $ embed g x+        +        bk (BLeft x)  = BLeft  $ project f x+        bk (BRight x) = BRight $ project g x+        +    +instance Absorbs Biject BSum BZero where+    absorb   = biject_sum_absorb+    unabsorb = inv biject_sum_absorb+    +biject_sum_absorb :: Biject (BSum BZero a) a+biject_sum_absorb = fw <-> bk where+    fw (BRight x) = x+    fw _ = error "biject_sum_absorb fw: impossible" +    bk = BRight++instance Assocative Biject BSum where+    assoc   = biject_sum_assoc+    unassoc = inv biject_sum_assoc++biject_sum_assoc :: Biject (BSum (BSum a b) c) (BSum a (BSum b c))+biject_sum_assoc = fw <-> bk where+    fw (BLeft (BLeft x))  = BLeft x+    fw (BLeft (BRight x)) = BRight $ BLeft x+    fw (BRight x)         = BRight $ BRight x +    +    bk (BLeft x)            = BLeft (BLeft x)+    bk (BRight (BLeft x)) = BLeft (BRight x) +    bk (BRight (BRight x))  = BRight x++instance Monoidial Biject BSum BZero where++instance Commutative Biject BSum where+    commute = fw <-> bk where+        fw (BRight x) = BLeft x+        fw (BLeft x)  = BRight x +        +        bk (BRight x) = BLeft x+        bk (BLeft x)  = BRight x ++instance CommutativeMonoidial Biject BSum BZero where+\end{code}++\subsubsection{Product Commutative Monoid Instances}+%format BProduct = "\ast "+%format BOne = "\MVOne "+\begin{code}+data BProduct a b = BP a b+newtype BOne  = BO ()+--Instances    +instance Ctor Biject BProduct where+    selfmap (Iso f_fw f_bk ) (Iso g_fw g_bk) = +        Iso (\(BP x y) -> BP (f_fw x) (g_fw y)) (\(BP x y) -> BP (f_bk x) (g_bk y)) +    +instance Absorbs Biject BProduct BOne where+    absorb   = biject_product_absorb+    unabsorb = inv biject_product_absorb+    +biject_product_absorb :: Biject (BProduct BOne a) a+biject_product_absorb = fw <-> bk where+    fw (BP (BO ()) x) = x +    bk x = BP (BO ()) x+    +instance Assocative Biject BProduct where+    assoc   = biject_product_assoc+    unassoc = inv biject_product_assoc+    +biject_product_assoc :: Biject (BProduct (BProduct a b) c) (BProduct a (BProduct b c))+biject_product_assoc = fw <-> bk where+    fw (BP (BP x y) z) = BP x (BP y z)+    bk (BP x (BP y z)) = BP (BP x y) z+    +instance Monoidial Biject BProduct BOne where++instance Commutative Biject BProduct where+    commute = (\(BP x y) -> BP y x) <-> (\(BP x y) -> BP y x) +    +instance CommutativeMonoidial Biject BProduct BOne where+\end{code}++\subsubsection{Semiring Instance}+\begin{code}+instance Annihilates Biject BProduct BZero where+    annihilates = (\(BP _ _) -> undefined) <-> (`BP` undefined)++instance Distributes Biject BSum BProduct where+    distribute   = biject_distributes+    undistribute = inv biject_distributes+    +biject_distributes :: Biject (BProduct (BSum a b) c) (BSum (BProduct a c) (BProduct b c))+biject_distributes = fw <-> bk where+    fw (BP (BLeft x) z)  = BLeft (BP x z) +    fw (BP (BRight y) z) = BRight (BP y z)+    +    bk (BLeft (BP x z))  = BP (BLeft x) z+    bk (BRight (BP y z)) = BP (BRight y) z+    +instance Semiring Biject BSum BZero BProduct BOne where+\end{code}++\subsection{Groupoid with a Klesli arrow as the base category}+\subsubsection{Sum Commutative Monoid Instances}+%format KBSum = "\bigplus "+%format KBZero = "\MVZero "+\begin{code}+data KBSum a b = KBLeft a | KBRight b+newtype KBZero = KBZ Void+--Instances    +instance Monad m => Ctor (KBiject m) KBSum where+    selfmap f g = fw <-> bk where+        fw = Kleisli $ run_pair (embed f) (embed g)+        bk = Kleisli $ run_pair (project f) (project g)++        run_pair t _ (KBLeft  x) = KBLeft  `liftM` runKleisli t x+        run_pair _ u (KBRight x) = KBRight `liftM` runKleisli u x+    +instance Monad m => Absorbs (KBiject m) KBSum KBZero where+    absorb   = kbiject_sum_absorb+    unabsorb = inv kbiject_sum_absorb+    +kbiject_sum_absorb :: Monad m => (KBiject m) (KBSum KBZero a) a+kbiject_sum_absorb = fw <-> bk where+    fw = Kleisli $ \e -> case e of+                    KBRight x -> return x+                    _ -> error "kbiject_sum_absorb fw: impossible"   +    bk = Kleisli $ \x -> return $ KBRight x+    +instance Monad m => Assocative (KBiject m) KBSum where+    assoc   = kbiject_sum_assoc+    unassoc = inv kbiject_sum_assoc+                              +kbiject_sum_assoc :: Monad m => (KBiject m) (KBSum (KBSum a b) c) (KBSum a (KBSum b c))+kbiject_sum_assoc = fw <-> bk where  +    fw = Kleisli $ \e -> case e of+                KBLeft x  -> case x of+                              KBLeft  y -> return $ KBLeft y+                              KBRight y -> return $ KBRight $ KBLeft y+                KBRight x -> return $ KBRight $ KBRight x+    bk = Kleisli $ \e -> case e of+                KBLeft  x -> return $ KBLeft $ KBLeft x+                KBRight x -> case x of+                              KBLeft y  -> return $ KBLeft $ KBRight y+                              KBRight y -> return $ KBRight y+    +instance Monad m => Monoidial (KBiject m) KBSum KBZero where++instance Monad m => Commutative (KBiject m) KBSum where+    commute = fw <-> fw where+        fw = Kleisli $ \e -> case e of+                        KBLeft x  -> return $ KBRight x+                        KBRight x -> return $ KBLeft x+ +instance (Monad m) => CommutativeMonoidial (KBiject m) KBSum KBZero where+\end{code}++\subsubsection{Product Commutative Monoid Instances}+%format KBProduct = "\ast "+%format KBOne = "\MVOne "+\begin{code}+data KBProduct a b = KBP a b+newtype KBOne  = KBO ()+--Instances    +instance Monad m => Ctor (KBiject m) KBProduct where+    selfmap f g = fw <-> bk where+        fw = Kleisli $ run_pair (embed   f) (embed   g)+        bk = Kleisli $ run_pair (project f) (project g) +                +        run_pair t u (KBP x y) = +            uncurry KBP `liftM` mfuse (runKleisli t x, runKleisli u y)                   ++    +instance Monad m => Absorbs (KBiject m) KBProduct KBOne where+    absorb   = kbiject_product_absorb+    unabsorb = inv kbiject_product_absorb+   +kbiject_product_absorb :: Monad m => (KBiject m) (KBProduct KBOne a) a+kbiject_product_absorb = fw <-> bk where+    fw = Kleisli $ \(KBP (KBO ()) x) -> return x   +    bk = Kleisli $ \x -> return $ KBP (KBO ()) x+   +    +instance Monad m => Assocative (KBiject m) KBProduct where+    assoc   = kbiject_product_assoc+    unassoc = inv kbiject_product_assoc++kbiject_product_assoc :: Monad m+                      => (KBiject m) (KBProduct (KBProduct a b) c) (KBProduct a (KBProduct b c))+kbiject_product_assoc = fw <-> bk where  +    fw = Kleisli $ \(KBP (KBP f g) h) -> return $ KBP f (KBP g h)+    bk = Kleisli $ \(KBP f (KBP g h)) -> return $ KBP (KBP f g) h+    +instance Monad m => Monoidial (KBiject m) KBProduct KBOne where++instance Monad m => Commutative (KBiject m) KBProduct where+    commute = fw <-> fw where+        fw = Kleisli $ \(KBP x y) -> return $ KBP y x+                          +instance (Monad m) => CommutativeMonoidial (KBiject m) KBProduct KBOne where+\end{code}+\subsubsection{Semiring Instance}+\begin{code}+instance (Monad m) => Annihilates (KBiject m) KBProduct KBZero where+    annihilates = fw <-> bk where +        fw = Kleisli $ \(KBP _ _) -> return undefined+        bk = Kleisli $ \x -> return $ KBP x undefined++instance (Monad m) => Distributes (KBiject m) KBSum KBProduct where+    distribute   = kbiject_distributes+    undistribute = inv kbiject_distributes+    +kbiject_distributes :: Monad m+                    => (KBiject m) (KBProduct (KBSum a b) c) (KBSum (KBProduct a c) (KBProduct b c))+kbiject_distributes = fw <-> bk where+    fw = Kleisli $ \e -> case e of+        KBP (KBLeft x) z  -> return $ KBLeft (KBP x z) +        KBP (KBRight y) z -> return $ KBRight (KBP y z)+    +    bk = Kleisli $ \e -> case e of+                    KBLeft (KBP x z)  -> return $ KBP (KBLeft x) z+                    KBRight (KBP y z) -> return $ KBP (KBRight y) z+    +instance Monad m => Semiring (KBiject m)  KBSum KBZero KBProduct KBOne where+\end{code}++++\end{document}