# Pass it to the right...

Skew-monoidal category normalization

## Introduction

While trying to normalize arrow expression produced by a custom quasiquoter I asked around (thanks edwardk) and was pointed toward Coherence for Skew-Monoidal Categories. I do not have a rigorous background in category theory and notation, so I took this as the chance to implement and learn. You can follow along with the paper as I tried to keep as close as possible to its order of presenetation.

## Skew

Standard monoidal categories include many functions that are *balanced* in that when there is a bifunctor (a type like (a,b) or Either a b) there is no preference for one or the other component of it. This lack of preference leads to some ambiguity and inability to define a clear path to a normal form. There are multiple ways to create to any form and multiple ways to get to them. So to resolve this Tarmo Uustalu, the author, picks a preferred direction.

## Setup

At first I started with trying to defined a `class SkewMonoidal`

, but it turns out to be not needed yet. Though I believe it would be helpful to make this a usable normalization procedure. Instead let's start on pg. 3 section 3.
First the author defines a free symetric monoidal category with Objects from a set Var.

`data Tm = X' Var | I | Tm :-: Tm`

There is also a map between two objects by a set of rule expressions. This tells us that we will build this datatype from primitive rules and some combinators:

```
data Rule = IdRule | Dot Rule Rule | Cross Rule Rule | La | Rh | Asc deriving Show
-- | Interpretation of rules and their composition.
evalRule :: Rule -> Tm -> Tm
evalRule IdRule = id
evalRule (Dot a b) = evalRule a . evalRule b
evalRule (Cross a b) = \(c :-: d) -> evalRule a c :-: evalRule b d
evalRule La = \(I :-: a) -> a
evalRule Rh = \a -> a :-: I
evalRule Asc = \case
((a :-: b) :-: c) -> (a :-: (b :-: c))
a -> error $ show a
-- These lambdas are NOT total! Bad parens later on caused some errors.
```

## Normal forms.

Next we define a normal form to be isomorphic to a list of Terms:

`data Nf = J | Var :.: Nf deriving Show`

Next we write a function to move from a the normal form back to the original Terms:

```
emb :: Nf -> Tm
emb J = I
emb (a :.: n) = X' a :-: emb n
```

We will need a helper function which walks along a structure of terms and folds it into a `Nf`

. I could not figure out a way to get outfix operators in Haskell, so I callted it splay.

```
splay :: Tm -> Nf -> Nf
splay (X' x) n = x :.: n
splay I n = n
splay (a :-: b) n = splay a (splay b n)
-- | Every object expression is assigned a normal form using the helper.
nf :: Tm -> Nf
nf a = splay a J
```

## Home Stretch

By starting with Identity in `Nf`

, the `nf`

function creates the normal form for the expression via manually unpacking the structure of the expression. Next we define a new operator. Don't ask me how to create this from scratch, I merely translated:

```
splat :: Tm -> Nf -> Rule
splat (X' _) _ = IdRule
splat I _ = La
splat (a :-: b) n = splat a (splay b n)
`Dot` (IdRule `Cross` splat b n `Dot` Asc)
```

That is the helper function which creates the rule expression. It is used in the normalizing map expression function defined next; `nm`

. The `J`

and `Rh`

are to allow `splat`

to do its job, but then to remove it.

```
nm :: Tm -> Rule
nm a = splat a J `Dot` Rh
```

The idea is that `nm`

and `nf`

should produce the same normal form. This is proved by the author elsewhere. 5 laws are required to be satisfied by the skew-monoidal category, so I should write those down in a nice Haskell format soon. With this, we are done! The `nm`

function will produce a rule expression which can be evaluated with `evalRule`

along with a Term to produce a new Term.

## Testing

Let's give it a shot

```
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
import Prelude hiding (id,(.))
import Control.Category
-- show
s,t,u,v,w :: Tm
s = X' A
t = X' A :-: I :-: X' B
u = I :-: I :-: (X' A :-: I) :-: X' B
v = I :-: u
w = t :-: t
main :: IO ()
main = do
printTest s
printTest t
printTest u
printTest v
printTest w
-- /show
printTest :: Tm -> IO ()
printTest a = do
let b = nf a
c = nm a
d = evalRule c a
putStrLn $ "Original Object: " ++ show a
putStrLn $ "Normal Form : " ++ show b
putStrLn $ "Rewrite Rules : " ++ if length (show c) > 70 then take 65 (show c) ++ " ..." else show c
putStrLn $ "Rewriten Object: " ++ show d
putStrLn ""
-- A Skew-monoidal category is a category `k` together with a
-- distinguished object `Id`, a functor `bimap`, and three
-- natural transformations, `lambda`, rho, and disassociate.
-- It is half of an Associative, Monoidal, Cartesian
-- | Objects of free symetric monoidal category with Objects from Var
data Var = A | B | C deriving Show
data Tm = I | X' Var | Tm :-: Tm deriving Show
-- | Maps between two objects.
data Rule = IdRule | Dot Rule Rule | Cross Rule Rule | La | Rh | Asc deriving Show
-- | Interpretation of rules and their composition.
evalRule :: Rule -> Tm -> Tm
evalRule IdRule = id
evalRule (Dot a b) = evalRule a . evalRule b
evalRule (Cross a b) = \(c :-: d) -> evalRule a c :-: evalRule b d
evalRule La = \(I :-: a) -> a
evalRule Rh = \a -> a :-: I
evalRule Asc = \case
((a :-: b) :-: c) -> (a :-: (b :-: c))
a -> error $ show a
-- Do we need to encode all the rules on page 4? Or are those just expected laws?
-- | We define "normal forms" of object expression as Nf
data Nf = J | Var :.: Nf deriving Show
-- | Normal forms embed into object expressions.
emb :: Nf -> Tm
emb J = I
emb (a :.: n) = X' a :-: emb n
-- | Let ||-|| be a function ... i'm calling it splay
splay :: Tm -> Nf -> Nf
splay (X' x) n = x :.: n
splay I n = n
splay (a :-: b) n = splay a (splay b n)
-- | Every object expression is assigned a normal form.
nf :: Tm -> Nf
nf a = splay a J
-- | In Lemma 3, Let now `<<->>` ... i'm calling it splat
splat :: Tm -> Nf -> Rule
splat (X' _) _ = IdRule
splat I _ = La
splat (a :-: b) n = splat a (splay b n)
`Dot` (IdRule `Cross` splat b n `Dot` Asc)
-- | "Normalizing" map expression.
nm :: Tm -> Rule
nm a = splat a J `Dot` Rh
```

We can see that the normal form and rewritten form match. We got this result by applying our rewrite rules, the skewed portions of the monoidal category.

## Ending note

This was a bit of pleasant translation. Is this construct useful, should I include it in Hackage? Any corrections comments or improvements are very welcome.

Entire code:

```
{-# START_FILE Skew.hs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{- |
Module : Control.Category.Monoidal.Skew
Description : skew-monoidal
Copyright : (c) 2015 Thomas Bereknyei
License : BSD3
Maintainer : Thomas Bereknyei <tomberek@gmail.com>
Stability : unstable
Portability : GADTs,LambdaCase
Implements normalization from: <http://arxiv.org/pdf/1406.2064v1.pdf>
The following is almost directly pulled out from the paper.
This served as a good exercise in translating category theory
notation into Haskell code. I welcome any corrections or
suggestions for improvement.
-}
module Skew where
import Prelude hiding (id,(.))
import Control.Category
-- A Skew-monoidal category is a category `k` together with a
-- distinguished object `Id`, a functor `bimap`, and three
-- natural transformations, `lambda`, rho, and disassociate.
-- It is half of an Associative, Monoidal, Cartesian
-- | Objects of free symetric monoidal category with Objects from Var
data Var = A | B | C deriving Show
data Tm = I | X' Var | Tm :-: Tm deriving Show
-- | Maps between two objects.
data Rule = IdRule | Dot Rule Rule | Cross Rule Rule | La | Rh | Asc deriving Show
-- | Interpretation of rules and their composition.
evalRule :: Rule -> Tm -> Tm
evalRule IdRule = id
evalRule (Dot a b) = evalRule a . evalRule b
evalRule (Cross a b) = \(c :-: d) -> evalRule a c :-: evalRule b d
evalRule La = \(I :-: a) -> a
evalRule Rh = \a -> a :-: I
evalRule Asc = \case
((a :-: b) :-: c) -> (a :-: (b :-: c))
a -> error $ show a
-- Do we need to encode all the rules on page 4? Or are those just expected laws?
-- | We define "normal forms" of object expression as Nf
data Nf = J | Var :.: Nf deriving Show
-- | Normal forms embed into object expressions.
emb :: Nf -> Tm
emb J = I
emb (a :.: n) = X' a :-: emb n
-- | Let ||-|| be a function ... i'm calling it splay
splay :: Tm -> Nf -> Nf
splay (X' x) n = x :.: n
splay I n = n
splay (a :-: b) n = splay a (splay b n)
-- | Every object expression is assigned a normal form.
nf :: Tm -> Nf
nf a = splay a J
-- | In Lemma 3, Let now `<<->>` ... i'm calling it splat
splat :: Tm -> Nf -> Rule
splat (X' _) _ = IdRule
splat I _ = La
splat (a :-: b) n = splat a (splay b n)
`Dot` (IdRule `Cross` splat b n `Dot` Asc)
-- | "Normalizing" map expression.
nm :: Tm -> Rule
nm a = splat a J `Dot` Rh
{- Would this be useful? Can translate into our Tm as an intermediate, normalize, translate back?
import Control.Categorical.Bifunctor
class Bifunctor p k k k => SkewMonoidal (k :: * -> * -> *) (p :: * -> * -> *) where
type Id (k :: * -> * -> *) (p :: * -> * -> *) :: *
lam :: (Id k p `p` a) `k` a
rho :: a `k` (a `p` Id k p)
dis :: ((a `p` b) `p` c) `k` (a `p` (b `p` c))
-- Free Skew-monoidal Category includes embedding for
-- normalization.
data SkewF f where
Id :: SkewF f
XXX :: f -> f -> SkewF f
Lam :: f -> SkewF f
Rho :: f -> SkewF f
Dis :: f -> SkewF f
Lift :: Var -> SkewF f
deriving Show
newtype Fix f = Fix (f (Fix f))
type Skew = Fix SkewF
-- Smart Constructors
i :: Skew
i = Fix Id
x :: (f -> SkewF Skew) -> f -> Skew
x a b = Fix $ a b
a *.* b = Fix (a `XXX` b)
l,r,d :: Skew -> Skew
l = x Lam
r = x Rho
d = x Dis
lift :: Var -> Skew
lift = Fix . Lift
instance (Show (f (Fix f))) => Show (Fix f) where
showsPrec p (Fix x) = showParen (p >= 11) (showString "Fix " . showsPrec 11 x)
---}
```