June 1st, 2019

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.