# Simplicity is the Initial Distributive Category

Simplicity is a combinator-based typed language with the unit type, sum types and product types.

Types: `𝟙`; `A + B`; `A × B`

Every Simplicity expression, `t`, has some input type, `A`, and some output type, `B`. We write this as `t : A ⊢ B`.

The combinators for the core Simplicity language are as follows:

```------------
iden : A ⊢ A

s : A ⊢ B
t : B ⊢ C
----------------
comp s t : A ⊢ C

------------
unit : A ⊢ 𝟙

s : A ⊢ B
t : A ⊢ C
--------------------
pair s t : A ⊢ B × C

t : A ⊢ C
------------------
take t : A × B ⊢ C

t : B ⊢ C
------------------
drop t : A × B ⊢ C

t : A ⊢ B
------------------
injl t : A ⊢ B + C

t : A ⊢ C
------------------
injr t : A ⊢ B + C

s : A × C ⊢ D
t : B × C ⊢ D
--------------------------
case s t : (A + B) × C ⊢ D
```

These look like the typical typing rules for the a sequent-calculus based type theory with the exception of the unusual typing rule found in the case expression.

In this post I want to show that this core Simplicity language is essentially the internal language for distributive categories. In particular, it means that in the category of distributive categories, the core Simplicity language is an initial object.

However, in order to do this we need to fix up the core Simplicity language a little. The first problem we need to address is that the core Simplicity language is missing the `𝟘` type. We have to add that type, along with its associated combinator.

```----------------
expl : 𝟘 × A ⊢ B
```

This combinator could easily be added to the Simplicity language. The combintor has no semantics because there is no input that satisfies the type `𝟘 × A`. In particular this means the combinator is never executed and must be pruned if used in Simplicity's blockchain application. Because all uses of `expl` must be pruned, the `𝟘` type wouldn't have any influence on type inference. Thus adding this combinator wouldn't necessarily affect the consensus critical interpretation of Simplicity. (That said, it maybe possible to leverage the `𝟘` type to reduce memory usage a little bit if the consensus critical interpreter would embrace the `𝟘` type.)

Next we need to impose a a relation onto the Simplicity terms in order to generate a congruence relation in order to satisfy the laws of a distributive category. Before doing that, let us add some useful definitions and notations.

```s ; t := comp s t

s ▵ t := pair s t

π₁ := take iden

π₂ := drop iden

σᴸ := injl iden

σᴿ := injr iden

s ▿ t := iden ▵ unit ; case (take s) (take t)

! := iden ▵ unit ; expl
```

Now we define the generating equations of that we want our equivalence relation on terms to satisfy:

```t : A ⊢ B
--------------------
t ; iden ≍ t : A ⊢ B

t : A ⊢ B
--------------------
iden ; t ≍ t : A ⊢ B

r : A ⊢ B
s : B ⊢ C
t : C ⊢ D
---------------------------------
r ; (s ; t) ≍ (r ; s) ; t : A ⊢ D

t : A ⊢ 𝟙
----------------
t ≍ unit : A ⊢ 𝟙

s : A ⊢ C
t : C ⊢ D
---------------------------------------
take (s ; t) ≍ (take s) ; t : A × B ⊢ D

s : B ⊢ C
t : C ⊢ D
---------------------------------------
drop (s ; t) ≍ (drop s) ; t : A × B ⊢ D

s : A ⊢ B
t : A ⊢ C
------------------------
(s ▵ t) ; π₁ ≍ s : A ⊢ B

s : A ⊢ B
t : A ⊢ C
------------------------
(s ▵ t) ; π₂ ≍ s : A ⊢ C

t : A ⊢ B × C
-----------------------------------
(t ; π₁) ▵ (t ; π₂) ≍ t : A ⊢ B × C

s : A ⊢ B
t : B ⊢ C
-------------------------------------
injl (s ; t) ≍ s ; injl t : A ⊢ C + D

s : A ⊢ B
t : B ⊢ D
-------------------------------------
injr (s ; t) ≍ s ; injr t : A ⊢ C + D

t : A ⊢ C
---------------------------------------------
injl (take t) ≍ take (injl t) : A × B ⊢ C + D

t : B ⊢ C
---------------------------------------------
injl (drop t) ≍ drop (injl t) : A × B ⊢ C + D

t : A ⊢ D
---------------------------------------------
injr (take t) ≍ take (injr t) : A × B ⊢ C + D

t : B ⊢ D
---------------------------------------------
injr (drop t) ≍ drop (injr t) : A × B ⊢ C + D

s : A × C ⊢ D
t : B × C ⊢ D
-------------------------------------------
(injl π₁ ▵ π₂) ; (case s t) ≍ s : A × C ⊢ D

s : A × C ⊢ D
t : B × C ⊢ D
-------------------------------------------
(injr π₁ ▵ π₂) ; (case s t) ≍ t : B × C ⊢ D

t : (A + B) × C ⊢ D
--------------------------------------------------------------------
case ((injl π₁ ▵ π₂) ; t) ((injr π₁ ▵ π₂) ; t) ≍ t : (A + B) × C ⊢ D

s : 𝟘 × A ⊢ B
--------------------
s ≍ expl : 𝟘 × A ⊢ B
```

plus reflexivity, symmetry and transitivity of `≍` and all the rules needed for `≍` to form a congruence relation, which I will omit.

We are going to show that the core Simplicity terms (extended with `expl`) under this equivalence relation form an initial distributive category. Before we do that though, let's observe the consequences of this theorem. Firstly, every bicartesian closed category is a distributive category. This means the functional semantics of core Simplicity, is uniquely defined by the only functor from core into the lambda-calculus that preserves, products and coproducts.

We also can see why the typing rules for the `case` expression look so unusual. If we had built terms using the standard rules for products and sums, we would get something that is the initial bicartesian category, but we wouldn't be able to derive the distributive law between sums and products. In bicartesian closed category we can use exponential objects (aka function types) to derive the distributive law, but Simplicity is first order so we are unable to do that. To get around the issue we "bake" the distributive law directly into the `case` combinator (and `expl` combinator).

That said, baking the distributive law into the case combinator comes at a price. This term calculus doesn't support cut-elimination, so a logician would hate it, and so perhaps it isn't great for term-rewriting. However for programming purposes, we were always going to use cuts anyways, because it makes terms exponentially smaller and doubly so when you have terms with sharing of sub-expressions.

It's also notable that the Kliesli category that we interpret the full Simplicity language into is not a distributive category because Kliesli categories do not have products. In particular, the equivalence `(s ▵ t) ; π₁ ≍ s,` is violated because the function denoted by `(s ▵ t) ; π₁` has the effects of both `s` and `t`, while obviously the term `s` only has the effects of `s`. This is the kind of semantic failure that is typical of strict functional languages with side-effects.

To show that the core Simplicity terms (extended with `expl`) under this equivalence relation forms an initial distributive category, we first prove that it forms a distributive category.

The `iden` and `comp` combinators with the laws gives us that it forms a category.

The `unit` expression provides the arrow to the terminal object, and the equation `t ≍ unit : A ⊢ 𝟙` proves that this arrow is unique.

The `π₁` and `π₂` expressions are the projection arrows needed for products and the `▵` combinator provides the existence of the arrow needed for the product's universal property. The equivalence relation rules involving the `▵`, `π₁` and `π₂` combinators show that the diagram for the universal property commutes and that the universal property's arrow is unique.

The `σᴸ` and `σᴿ` expressions are the injection arrows needed for the coproduct and the `▿` combinator provides the existence of the arrow needed for the coproduct's universal property. Let us prove that the diagram for the universal property commutes by showing `σᴸ ; (s ▿ t) ≍ s` and `σᴿ ; (s ▿ t) ≍ t`

```σᴸ ; (s ▿ t) ≍
σᴸ ; (iden ▵ unit) ; case (take s) (take t) ≍
((σᴸ ; (iden ▵ unit) ; π₁) ▵ (σᴸ ; (iden ▵ unit) ; π₂)) ; case (take s) (take t) ≍
((σᴸ ; iden) ▵ (σᴸ ; unit)) ; case (take s) (take t) ≍
(σᴸ ▵ unit) ; case (take s) (take t) ≍
((iden ; σᴸ) ▵ unit) ; case (take s) (take t) ≍
((iden ▵ unit) ; π₁ ; σᴸ) ▵ unit) ; case (take s) (take t) ≍
((iden ▵ unit) ; injl π₁) ▵ ((iden ▵ unit) ; π₂) ; case (take s) (take t) ≍
((iden ▵ unit) ; (injl π₁ ▵ π₂) ; π₁) ▵ ((iden ▵ unit) ; (injl π₁ ▵ π₂) ; π₂) ; case (take s) (take t) ≍
(iden ▵ unit) ; (injl π₁ ▵ π₂) ; case (take s) (take t) ≍
(iden ▵ unit) ; take s ≍
(iden ▵ unit) ; π₁ ; s ≍
iden ; s ≍
s
```

The proof that `σᴿ ; (s ▿ t) ≍ t` is similar.

We also need to prove that the coproducts universal property's arrow is unique by showing that `(σᴸ ; t) ▿ (σᴿ ; t) ≍ t`.

```(σᴸ ; t) ▿ (σᴿ ; t) ≍
(iden ▵ unit) ; case (take (σᴸ ; t)) (take (σᴿ ; t)) ≍
(iden ▵ unit) ; case (take σᴸ ; t) (take σᴿ ; t) ≍
(iden ▵ unit) ; case (injl π₁ ; t) (injr π₁ ; t) ≍
(iden ▵ unit) ; case ((injl π₁ ▵ π₂) ; π₁ ; t) ((injr π₁ ▵ π₂) ; π₁ ; t) ≍
(iden ▵ unit) ; π₁ ; t) ≍
iden ; t ≍
t
```

The `! : 𝟘 ⊢ A` expression defines the arrow from the initial object. We need to prove it is unique by showing that for any `t : 𝟘 ⊢ A` that `t ≍ !`.

```t  ≍
iden ; t ≍
iden ▵ unit ; π₁ ; t ≍
iden ▵ unit ; take t ≍
iden ▵ unit ; expl ≍
!
```

Lastly we need to prove the distributive properties. First we need to show that `! : 𝟘 ⊢ 𝟘 × A` is an isomorphism. The expression `expl` is the inverse. `! ; expl ≍ ! ≍ iden` proves one direction, by the uniqueness of `!`. For the order direction `expl ; ! ≍ expl ≍ iden` by the uniqueness of `expl`.

We also need to show that `((π₁ ; σᴸ) ▵ π₂) ▿ ((π₁ ; σᴿ) ▵ π₂) : A × C + B × C ⊢ (A + B) × C` is an isomorphism. The inverse is `case σᴸ σᴿ`.

```case σᴸ σᴿ ; ((π₁ ; σᴸ) ▵ π₂) ▿ ((π₁ ; σᴿ) ▵ π₂) ≍
case (σᴸ ; ((π₁ ; σᴸ) ▵ π₂) ▿ ((π₁ ; σᴿ) ▵ π₂)) (σᴿ ; ((π₁ ; σᴸ) ▵ π₂) ▿ ((π₁ ; σᴿ) ▵ π₂)) ≍
case ((π₁ ; σᴸ) ▵ π₂) ((π₁ ; σᴿ) ▵ π₂) ≍
case ((π₁ ; σᴸ) ▵ π₂ ; iden) ((π₁ ; σᴿ) ▵ π₂ ; iden) ≍
case (injl π₁ ▵ π₂ ; iden) (injr π₁ ▵ π₂ ; iden) ≍
iden
```
```((π₁ ; σᴸ) ▵ π₂) ▿ ((π₁ ; σᴿ) ▵ π₂) ; (case σᴸ σᴿ) ≍
((π₁ ; σᴸ) ▵ π₂ ; case σᴸ σᴿ) ▿ ((π₁ ; σᴿ) ▵ π₂ ; case σᴸ σᴿ) ≍
((injl π₁) ▵ π₂ ; case σᴸ σᴿ) ▿ (injr π₁ ▵ π₂ ; case σᴸ σᴿ) ≍
(σᴸ ▿ σᴿ) ≍
((σᴸ ; iden) ▿ (σᴿ ; iden)) ≍
iden
```

In order to show that our distributive category of core Simplicity terms (extended with expl) is initial, we must prove there is a functor into any distributive category. We will use the notation ⟦⋅⟧ to denote this functor. Our functor must map `𝟙` to the category's terminal object, map `𝟘` to the category's initial object, and must preserve products and coproducts.

• `iden : A ⊢ A`⟧ is id[⟦`A`⟧].
• `comp s t : A ⊢ C`⟧ is the composition ⟦`t`⟧∘⟦`s`⟧.
• `unit : A ⊢ 𝟙`⟧ is unique arrow from ⟦`A`⟧ to ⟦`𝟙`⟧.
• `take t : A × B ⊢ C`⟧ is the composition ⟦`t`⟧∘pi[1] where pi[1] is the first projection function of the target category.
• `drop t : A × B ⊢ C`⟧ is the composition ⟦`t`⟧∘pi[2] where pi[2] is the second projection function of the target category.
• `pair s t : A ⊢ B × C`⟧ is the arrow <⟦`s`⟧,⟦`t`⟧> is the unique arrow of the universal property of the target category's products.
• `injl t : A ⊢ B + C`⟧ is the composition sigma[1]∘⟦`t`⟧ where sigma[1] is the first injection function of the target category.
• `injr t : A ⊢ B + C`⟧ is the composition sigma[2]∘⟦`t`⟧ where sigma[2] is the second injection function of the target category.
• `case s t : (A + B) × C ⊢ D`⟧ is the composition [⟦`s`⟧,⟦`t`⟧]∘dist⁻¹ where [f,g] is the unique arrow of the universal property of the target category's coproduct generate from arrows f and g, and dist⁻¹ is the inverse of the distributive function, dist := [sigma[1]×id,sigma[2]×id].
• `expl : 𝟘 × A ⊢ B`⟧ is the composition ![⟦`B`⟧]∘![⟦`𝟘 × A`⟧]⁻¹ where ![⟦`B`⟧] is the unique arrow from the initial object to ⟦`B`⟧ and ![⟦`𝟘 × A`⟧]⁻¹ is the inverse of the unique arrow from the initial object to ⟦`𝟘 × A`⟧.

We need to show that the universal properties of our terms map are preserved by this functor.

```⟦π₁⟧ = id∘pi[1] = pi[1].
⟦π₂⟧ = id∘pi[2] = pi[2].
⟦s ▵ t⟧ = <⟦s⟧,⟦t⟧>.
⟦σᴸ⟧ = sigma[1]∘id = sigma[1]
⟦σᴿ⟧ = sigma[2]∘id = sigma[2]
⟦s ▿ t⟧ = ⟦iden ▵ unit ; case (take s) (take t)⟧
= [⟦s⟧∘pi[1],⟦t⟧∘pi[1]]∘dist⁻¹∘<id,⟦unit⟧>
= [⟦s⟧∘pi[1],⟦t⟧∘pi[1]]∘dist⁻¹∘[<id,⟦unit⟧>∘sigma[1],<id,⟦unit⟧>∘sigma[2]]
= [⟦s⟧∘pi[1],⟦t⟧∘pi[1]]∘dist⁻¹∘[<sigma[1],⟦unit⟧∘sigma[1]>,<sigma[2],⟦unit⟧∘sigma[2]>]
= [⟦s⟧∘pi[1],⟦t⟧∘pi[1]]∘dist⁻¹∘[<sigma[1],⟦unit⟧>,<sigma[2],⟦unit⟧>]
= [⟦s⟧∘pi[1],⟦t⟧∘pi[1]]∘dist⁻¹∘[sigma[1]×id∘<id,⟦unit⟧>,sigma[2]×id∘<id,⟦unit⟧>]
= [⟦s⟧∘pi[1],⟦t⟧∘pi[1]]∘dist⁻¹∘[sigma[1]×id,sigma[2]×id]∘(<id,⟦unit⟧>+<id,⟦unit⟧>)
= [⟦s⟧∘pi[1],⟦t⟧∘pi[1]]∘dist⁻¹∘dist∘(<id,⟦unit⟧>+<id,⟦unit⟧>)
= [⟦s⟧∘pi[1],⟦t⟧∘pi[1]]∘(<id,⟦unit⟧>+<id,⟦unit⟧>)
= [⟦s⟧∘pi[1]∘<id,⟦unit⟧>,⟦t⟧∘pi[1]∘<id,⟦unit⟧>]
= [⟦s⟧∘id,⟦t⟧∘id]
= [⟦s⟧,⟦t⟧]
```

and the unique arrows from the initial object and the unique arrows to final object are necessarily preserved.

For this functor to be well-defined we also have to show that it respect our congruence relation on terms.

```⟦t ; iden⟧ = ⟦iden⟧∘⟦t⟧ = id∘⟦t⟧ = ⟦t⟧
⟦iden ; t⟧ = ⟦t⟧∘⟦iden⟧ = ⟦t⟧∘id = ⟦t⟧
⟦r ; (s ; t)⟧ = ⟦t⟧∘⟦s⟧∘⟦r⟧ = ⟦(r ; s) ; t⟧
⟦t : A ⊢ 𝟙⟧ = ⟦unit : A ⊢ 𝟙⟧ due to the uniqueness of the arrow to the terminal object.
⟦take (s ; t)⟧ = ⟦t⟧∘⟦s⟧∘pi[1] = ⟦take s ; t⟧
⟦drop (s ; t)⟧ = ⟦s⟧∘⟦s⟧∘pi[2] = ⟦drop s ; t⟧
⟦(s ▵ t) ; π₁⟧ = pi[1]∘<⟦s⟧,⟦t⟧> = ⟦s⟧
⟦(s ▵ t) ; π₂⟧ = pi[2]∘<⟦s⟧,⟦t⟧> = ⟦t⟧
⟦(t ; π₁) ▵ (t ; π₂)⟧ = <pi[1]∘⟦t⟧,pi[2]∘⟦t⟧> = ⟦t⟧
⟦injl (s ; t)⟧ = sigma[1]∘⟦t⟧∘⟦s⟧ = ⟦s ; injl t⟧
⟦injr (s ; t)⟧ = sigma[2]∘⟦t⟧∘⟦s⟧ = ⟦s ; injr t⟧
⟦injl (take t)⟧ = sigma[1]∘⟦t⟧∘pi[1] = ⟦take (injl t)⟧
⟦injl (drop t)⟧ = sigma[1]∘⟦t⟧∘pi[2] = ⟦drop (injl t)⟧
⟦injr (take t)⟧ = sigma[2]∘⟦t⟧∘pi[1] = ⟦take (injr t)⟧
⟦injr (drop t)⟧ = sigma[2]∘⟦t⟧∘pi[2] = ⟦drop (injr t)⟧
⟦(injl π₁ ▵ π₂) ; (case s t)⟧ = [⟦s⟧,⟦t⟧]∘dist⁻¹∘<sigma[1]∘pi[1],pi[2]>
= [⟦s⟧,⟦t⟧]∘dist⁻¹∘(sigma[1]×id)
= [⟦s⟧,⟦t⟧]∘dist⁻¹∘[sigma[1]×id,sigma[2]×id]∘sigma[1]
= [⟦s⟧,⟦t⟧]∘dist⁻¹∘dist∘sigma[1]
= [⟦s⟧,⟦t⟧]∘sigma[1]
= ⟦s⟧
⟦(injr π₁ ▵ π₂) ; (case s t)⟧ = [⟦s⟧,⟦t⟧]∘dist⁻¹∘<sigma[2]∘pi[1],pi[2]>
= [⟦s⟧,⟦t⟧]∘dist⁻¹∘(sigma[2]×id)
= [⟦s⟧,⟦t⟧]∘dist⁻¹∘[sigma[1]×id,sigma[2]×id]∘sigma[2]
= [⟦s⟧,⟦t⟧]∘dist⁻¹∘dist∘sigma[2]
= [⟦s⟧,⟦t⟧]∘sigma[2]
= ⟦t⟧
⟦case ((injl π₁ ▵ π₂) ; t) ((injr π₁ ▵ π₂) ; t)⟧ = [⟦t⟧∘<sigma[1]∘pi[1],pi[2]>,⟦t⟧∘<sigma[2]∘pi[1],pi[2]>]∘dist⁻¹
= ⟦t⟧∘[sigma[1]×id,sigma[2]×id]∘dist⁻¹
= ⟦t⟧∘dist∘dist⁻¹
= ⟦t⟧
⟦s : 𝟘 × A ⊢ B⟧ = ⟦s⟧∘![𝟘 × A]∘![𝟘 × A]⁻¹ = ![B]∘![𝟘 × A]⁻¹ = ⟦expl⟧
```

Finally, we need to prove that this functor we have defined is the unique functor to this arbitrary category. Suppose that ⟦⋅⟧ is any functor from core Simplicity terms (extended with expl) to a distributive category that preserves the distributive structure and respect our equivalence relation on terms. Therefore this functor maps `𝟙` to the category's terminal object, maps `𝟘` to the category's initial object, and must preserve products and coproducts. It must map `unit : A ⊢ 𝟙` to the unique arrow from ⟦`A`⟧ to the terminal object, map `iden : A ⊢ A` to id[⟦`A`⟧] and map `comp s t : A ⊢ C` to the composition ⟦`t`⟧∘⟦`s`⟧. The rest of the terms must be mapped as follows.

```⟦take t : A × B ⊢ C⟧ = ⟦take (iden ; t)⟧ = ⟦π₁ ; t⟧ = ⟦t⟧∘pi[1]
⟦drop t : A × B ⊢ C⟧ = ⟦drop (iden ; t)⟧ = ⟦π₂ ; t⟧ = ⟦t⟧∘pi[2]
⟦pair s t : A ⊢ B × C⟧ = <⟦s⟧,⟦t⟧>
⟦injl t : A × B ⊢ C⟧ = ⟦injl (t ; iden)⟧ = ⟦t ; σᴸ⟧ = sigma[1]∘⟦t⟧
⟦injr t : A × B ⊢ C⟧ = ⟦injr (t ; iden)⟧ = ⟦t ; σᴿ⟧ = sigma[2]∘⟦t⟧
⟦case s t : (A + B) × C ⊢ D⟧ = ⟦case s t⟧∘dist∘dist⁻¹
= ⟦case s t⟧∘[sigma[1]×id,sigma[2]×id]∘dist⁻¹
= ⟦case s t⟧∘[<sigma[1]∘pi[1],pi[2]>,<sigma[2]∘pi[1],pi[2]>∘dist⁻¹
= ⟦case s t⟧∘⟦((π₁ ; σᴸ) ▵ π₂) ▿ ((π₁ ; σᴿ) ▵ π₂)⟧∘dist⁻¹
= ⟦(((π₁ ; σᴸ) ▵ π₂) ▿ ((π₁ ; σᴿ) ▵ π₂)) ; case s t⟧∘dist⁻¹
= ⟦(((injl π₁) ▵ π₂) ▿ ((injr π₁) ▵ π₂)) ; case s t⟧∘dist⁻¹
= ⟦((injl π₁) ▵ π₂ ; case s t) ▿ ((injr π₁) ▵ π₂ ; case s t)⟧∘dist⁻¹
= ⟦s ▿ t⟧∘dist⁻¹
= [⟦s⟧,⟦t⟧]∘dist⁻¹
⟦expl : 𝟘 × A ⊢ B⟧ = ⟦expl⟧∘![⟦𝟘 × A⟧]∘![⟦𝟘 × A⟧]⁻¹
= ⟦expl⟧∘⟦iden ▵ unit ; expl⟧∘![⟦𝟘 × A⟧]⁻¹
= ⟦iden ▵ unit ; expl ; expl⟧∘![⟦𝟘 × A⟧]⁻¹
= ⟦iden ▵ unit ; expl⟧∘![⟦𝟘 × A⟧]⁻¹
= ![⟦B⟧]∘![⟦𝟘 × A⟧]⁻¹
```

That completes the proof that core Simplicity terms (extended with `expl`) is an initial distributive category.

• #### From Van Laarhoven Isomorphisms in one shot.

The type ∀ f, g : Functor. (g a → f b) → g s → f t is isomorphic to the type (s → a)×(b → t). The Van…

• #### A new case for the pointed functor class

There has been some debate for some time as to whether there should be a superclass for Applicative with just the pure function should exist:…

• #### Grate: A new kind of Optic

James Deikun (known as xplat on freenode) and I discovered a new kind of Optic today. If not discovered, then at least characterized it. We know…

• Post a new comment

#### Error

default userpic
When you submit the form an invisible reCAPTCHA check will be performed.