# Skew-Monoidal Normalization

27 Aug 2015

As of March 2020, School of Haskell has been switched to read-only mode.

# 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 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: