Skew-Monoidal Normalization

27 Aug 2015 tomberek View Markdown source

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

Sections

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.

Untitled.png

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:

Untitled.png

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:

Untitled.png

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

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

Untitled.png

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.

Untitled.png

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:

Untitled.png

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.

Untitled.png

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:

comments powered by Disqus