A considerable amount of time has been spent on both research (more amazing stuff about this will follow in the coming months) and on formalizing a formally verified version of our core in Idris, which in turn has been implemented by many people from our team (mainly Sjoerd, Alex and Andre, which I thank for the incredible work!).

What does it do?

Now that we have a version of the core released, I’d like to explain what it does. The idea is simple: You pass it a specification for a finite state machine/Petri net, an initial state and a sequence of actions, and the core will tell you if that sequence of actions is valid.

I know what you are thinking: “Wait what? You spent more than a year to get this?!” The short answer is “Yes, we have.” The long answer is “We decided to make an investment, and spent a lot of time developing our basic infrastructure so that building incrementally on it would be much easier later on”. An even better answer is: “Try it out yourself!”. In any case, with this post, I hope to convince you this choice is not as abysmally dumb as it sounds, but quite the opposite.

Typedefs and Typed Core

Several years ago we started two big projects at Statebox, namely Typedefs and Typed Core. Typedefs is a formally verified programming language for types and terms. Essentially, it allows to specify a universal format for types that can be recursively built out of type variables, products, coproducts and fixed point operators, and for their terms. Given Typedefs and their terms, one is able to automatically serialize and deserialize them to various formats, such as binary, S-expressions and JSON. This allows for a formally well-defined way of exchanging data between different programming languages.

On the other hand, typed core is a formally verified implementation of the main engine that tells us if a given sequence of transitions fired in a Petri net is valid or not. This is done in Idris, and relies on idris-ct, our formally verified category theory library.

Getting these two projects up to a point where they could be useful has been a lot of work, but it pays off! Now, we can just define our categories effortlessly using idris-ct, and import/export their signatures and morphisms using Typedefs.

This is exactly what we did in our first version of the core, which we completed roughly a month ago. In it, the user is able to feed the core with a specification for a finite state machine, an initial state and a sequence of actions, specified as a path in the underlying FSM graph. This specification is exchanged using JSON, as in the following example:

{
  "_0": {
    "_0": 5,
    "_1": [
      {
       "input": 1,
       "output": 1
      },
      {
       "input": 3,
       "output": 4
      },
      {
       "input": 2,
       "output": 1
      },
      {
       "input": 3,
       "output": 2
      }]
  },
  "_1": 3,
  "_2": [3, 2, 0]
}

Here, the first field specifies the “shape” of the FSM:

"_0": 5,
    "_1": [
      {
       "input": 1,
       "output": 1
      },
      {
       "input": 3,
       "output": 4
      },
      {
       "input": 2,
       "output": 1
      },
      {
       "input": 3,
       "output": 2
      }]

The first field tells us that the FSM has five vertexes, indexed 0, 1, 2, 3, 4 . The second field specifies the edges, indexed 0,1,2,3: The first edge goes from 1 to 1 , the second from 3 to 4 , the third from 2 to 1, the fourth from 3 to 2. All in all, the FSM looks like this:

Then we have:

  "_1": 3,
  "_2": [3, 2, 0]

Here the first field specifies the initial state (start from vertex 3), while the second one specifies a path, in this case (go through edge 3, then through edge 2, then through 0 ). The path is the one displayed below:

The point is that this JSON format is not arbitrary; it is the encoding of a Typedefs term. So if the term is malformed for whatever reason, Typedefs will throw an error automatically. We do not have to worry anymore about our parser being correct, because it is generated automatically from our definition!

Internally, a correct FSM specification is used as the signature to build the free category associated to it. Then, the path is evaluated: Either it forms a valid morphism or it doesn’t. If it doesn’t then we throw an error, if it does we check that the domain of such morphism is indeed the initial state specified. If this is the case we return a positive answer. In any case, the answer is again returned as a Typedefs term, and as such can be easily exchanged around.

All in all, our software works like an oracle. The cool thing is that we can be very flexible about the types we use to exchange computational objects around since TDefs will take care of serialization and parsing for us. Moreover, we are using categorical constructions as typecheckers, and not some ad-hoc thing.

The advantages of this approach are considerable. Less than two weeks ago we started working on the Petri net version of this, which amounts to taking symmetric strict monoidal categories as our typecheckers. We had already implemented those in idris-ct, and hence we were able to finish our work almost instantly. With an amount of minimal tweaking, we were able to recast our infrastructure completely to deal with Petri nets. Indeed, we are now in the process of documenting the new version of the core, which we will likely release in the coming months.

I hope that the advantages of employing categorical methods are now clear. It’s a lot of hassle in the beginning, but then things become way easier since in category theory everything is defined “canonically”, meaning that there is often just one way to do things, which is also the right one if you worked on the foundations of your project well enough.

Feel free to play with the oracle we released, and stay tuned for the new version that we’ll release soon!

FSM-Oracle Release was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

As our dear readers widely know, Statebox is a company that heavily relies on category theory for the development of its products. Attention towards category theory by academia is not at all surprising. Applied category theory has become a fertile research field, as reflected by the several conferences and events which emerged in the past few years, such as the yearly applied category theory conference (ACT) or our own yearly summit.

On the other hand, the enterprise sector seems to get increasingly aware of how categorical reasoning could impact their own future. In many niches of the tech space, there is a pervasive feeling that we finally possess the right formal tools to apply compositional techniques (that is, ACT) in a widespread fashion. Some companies are understanding this at a naïve level, and are reacting by, say, increasingly adopting functional programming languages for the development of their product stack. Other companies are instead fully aware of this, and are actively setting up research efforts in applied category theory.

How category theory can help your company

In An Invitation to Applied Category Theory, Fong and Spivak introduce their topic as follows:

It is unmatched in its ability to organize and layer abstractions, to find commonalities between structures of all sorts.

To give you an intuitive feeling of how category theory can impact company life, think about the following:

• at a high and abstract level, business is about connecting different ideas and crunching numbers to see how these ideas perform and become profitable;
• programming is about connecting different pieces of software in a manner that will minimise generative effects, or as we like to call it, emergent behavior;
• production and planning is about connecting different facts (e.g. travelling time and price from A to B) while keeping an eye on optimization.

In all these examples, the idea of “connecting things to other things” is preeminent. Category theory provides a universal language to reason about these relationships. Now business planning and programming become just two different incarnations of the same underlying idea. Moreover, the use of functors (which are ways to map things to other things while preserving their connections) makes the unthinkable possible, e.g. by mapping business workflows directly into code. This is precisely what we are working on at Statebox, and you can see a minimal application of this in our video series about designing smart contracts with Petri nets.

Do you need to be a mathematician to learn category theory?

This is the most popular myth surrounding category theory adoption and we are here to bust it. Unfortunately, as all things when seen from the outside world, the ideas behind category theory can feel obscure and complicated. In addition to this, people seem to believe that you have to already know a lot of mathematics to get category theory right. This is clearly false, but such prejudice is reinforced by the fact that nearly all of the free learning material on the internet is directed at mathematicians, physicists and computer scientists.

Too hard, won’t bother

But how hard is it to learn category theory? In my experience as a category theory teacher, I’ve noticed that people tend to naturally think in compositional terms, but somehow they forget about it when they are taught other things. For this reason, learning category theory requires a shift in point of view that, once started, feels more as a re-discovery than as something new. This is confirmed by my own experience as a category theory student. When I myself had to learn category theory, I found out that the cause of my struggle was trying to understand category theory with the tools I had already acquired, instead of just starting from scratch. When things started clicking, I realized that category theory is, by definition, the most natural way to reason about and model systems. From this point of view it is evident that category theory is not difficult to learn, since its working principles are, most often than not, already well understood by its learners, who simply are not yet aware of this.

Category Theory Course — March, Berlin

For the above reasons and more, we decided to launch a category theory course aimed at programmers, system architects and businesses in general. We already have experience in teaching category theory to non mathematicians and we believe the best way to teach it is through examples tailored on the knowledge of the learners. In our course, we carefully evaluate the needs of our clients and their skillset, and figure out the most frictionless way to initiate your journey into categorical thinking.

The aim of our course is to provide a base layer of understanding of the main topics in ACT and show how they can be used to model systems. Then, you will be able to either deepen your knowledge by yourself by accessing previously unmanageable learning material on the internet or to interact with expert category theorists in the ACT community. You will be able to understand the category theory jargon, and this will endow you with a universal language that facilitates the understanding of current research in the field as well as form abstractions and find similarities in seemingly unfamiliar spheres. We truly believe that this opens the door to offering unique solutions to problem solving, regardless of the domain you find yourself in.

Join our category theory course on 24–27 March in Berlin. The course will be taught by yours truly with the support of at least one other guest category theorist from the ACT community. Sign up here!

Abstraction is the New Gold was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

In this post we will revisit the ideas presented there in a more categorical fashion, but focusing on lenses in particular.

What we will present in this post is a series of results which were obtained at the third Statebox Summit with the collaboration of the participants, out of which I ought to mention Jules Hedges, David Spivak, Brendan Fong, Christina Vasilakopoulou, Eliana Lorch, Andre Knispel and Stefano Gogioso for taking active part in this discussion.

The Category of Lenses

Let’s start by defining the category of lenses. The objects of our category will be pairs of sets (S, T), morphisms between (S, T) and (A, B) will be lenses of type Lens S T A B, which are described by pairs of functions

g : S → A

p : S → B → T

The composition of two morphisms, i.e. two lenses, (g, p) : (S, T) → (A, B) and (h, q) : (A, B) → (C, D) is a new lens (g', p') : Lens S T C D defined by functions

g' : S → C
g' = g ; h

p' : S → D → T
p' s d = p s (q (g s) d)

where p' can be represented by the following diagram

where ∙ : S → S × S is the copy operation.

Given any object of our category, which is a pair (S, T), the identity morphism on it is the lens (gᵢ, pᵢ) : (S, T) → (S, T) defined by

gᵢ : S → S
gᵢ s = s

pᵢ : S → T → T
pᵢ s t = t

It can be checked that the above definitions satisfy the axioms for a category.

Associated Lenses

Given a generic lens L := (g, p) : (S, T) → (A, B), we saw in this post that we can define a set

M = { m ∈ B → T | ∃ s : S . m = p s }

which turns out to be really helpful in proving that lawful lenses are exactly the constant complement ones. In fact, this set allows us to define two new lenses associated to the lens L.

First off, we can define L* : (S, T) → (A × M, B × M) by

g*: S → A × M
g* s = (g s, p s)

p* : S → B × M → T
p* s (b, m) = m b

Moreover, we can also define L^ : (B × M, A × M) → (T, S) by

g^ : B × M → T
g^ (b, m) = m b

p^ : B × M → S → A × M
p^ (b, m) s = (g s, p s)

Notice how ^ (pronounced “hat”) produces a swap between A and B and between S and T. In their generic form, L* and L^ are not composable. However, if we restrict them to simple lenses, they are!

So, with these two new lenses at hand, some questions arise naturally

• In the simple lens case, when are L* and L^ inverse of one another?
• In the simple lens case, when are L* and L^ lawful?
• In the generic case, if we consider π : (A × M, B × M) → (A, B) to be the lens defined by

gπ : A × M → A
gπ (a, m) = a

pπ : A × M → B → B × M 
pπ (a, m) b = (b, m)

is it always true that L = L* ; π?

Are L* and L^ Inverses?

Let us first consider the composition L* ; L^. In this case we have

g*^ : S → S
g*^ s = p s (g s) = s -- by getput

p*^ : S → S → S
p*^ s₁ s₂ = p s₂ (g s₂) = s₂ -- by getput

Therefore L^ ; L^ = id on (S, S) if and only if getput holds for L.

On the other hand, consider L^ ; L*. We obtain

g^* : A × M → A × M
g^* (a, m) = (g (m a), p (m a))

p^* : A × M → A × M → A × M
p^* (a₁, m₁) (a₂, m₂) = (g (m₂ a₂), p (m₂ a₂))

Remember that by definition of M we have that any m ∈ M is of the form p s for some s ∈ S. Hence we get

g^* : A × M → A × M
g^* (a, p s) = (g (p s a), p (p s a))
             = (a, p s) -- by putget and putput

p^* : A × M → A × M → A × M
p^* (a₁, p s₁) (a₂, p s₂) = (g (p s₂ a₂), p (p s₂ a₂))
                          = (a₂, p s₂) -- by putget and putput

We then obtain that L^ ; L* = id on (M × A) whenever L satisfies putget and putput.

We conclude by saying that L* and L^ are each other’s inverses if and only if L is a lawful lens.

Are L* and L^ Lawful?

In this section we will check whether L* and L^ are lawful lenses in the simple case, and which conditions we do need to assume on L for them to satisfy the lens laws.

Let’s start with L*

getput

p* s (g* s) = p s (g s) = s -- by getput

putget

g* (p* s₁ (a, p s₂)) = g* (p s₂ a)
                     = (g (p s₂ a), p (p s₂ a))
                     = (a, p s₂) -- by putget and putput

putput

p* (p* s (a₁, m₁)) (a₂, m₂) = p* (m₁ a₁) (a₂, m₂)
                            = m₂ a₂
                            = p* s (a₂, m₂) -- always holds

Hence L* always satisfies putput, satisfies getput if L satisfies getput and satisfies putget if L satisfies putget and putput. Therefore L* is lawful if and only if L is.

Let’s now have a look at L^.

getput

p^ (a, p s) (g^ (a, p s)) = p^ (a, p s) (p s a)
                          = (g (p s a), p (p s a))
                          = (a, p s) -- by putget and putput

putget

g^ (p^ (a, m) s) = g^ (g s, p s)
                 = p s (g s)
                 = s -- by getput

putput

p^ (p^ (a, m) s₁) s₂ = p^ (g s₁, p s₁) s₂
                     = (g s₂, p s₂)
                     = p^ (a, m) s₂ -- always

Therefore also L^ always satisfies putput, and it satisfies getput if L satisfies putget and putput and satisfies putget if L satisfies getput. So also L^ is lawful if and only if L is.

Decomposing L

One question remains: whether L = L* ; π holds. It is not hard to check that it actually always does; in fact if we compute the components g° and p° for the composed lens, we get

g° : S → A
g° s = gπ (g* s) = gπ (g s, p s) = g s

p° : S → B → T
p° s b = p* (s, pπ (g* s, b))
       = p* (s, pπ ((g s, p s), b))
       = p* (s, (b, p s)) = p s b

In conclusion, we can always decompose L into L* ; π, where π is always lawful.

Conclusion

In this post we investigated the role of M more closely, as well as the lenses L* and L^ which are generated from it. We saw that L* and L^ are strictly related to L, and that they satisfy the lens laws only if L satisfies other lens laws.

Putting together the three results presented above, we can also recover a more formal proof that a simple lens is lawful if and only if it is isomorphic to a constant complement lens.

Some further questions we might consider

• What is M for L* and L^ ?
• How are L**, L*^, L^* and L^^ related to L, L* and L^?
• Is there a relation between M being a singleton set and isomorphisms in the category of lenses (it is easy to prove that M = {*} implies that L satisfies putput)?
• Are the properties stated for the simple case generalizable to the general case?

More (Categorical) Thoughts on Lawful Lenses was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

Lenses and optics in general seem to be popping up both in the functional programming and category theory community. This suggest they have an important role that is yet to be completely understood.

One thing that struck me while reading about lenses is the fact that functional programmers tend to consider only lawful lenses, while academics are interested more broadly in generic lenses. Moreover, optics laws, although very meaningful in practice, appear as something God-given and it is hard to understand where they come from. Additionally, laws are usually defined only for simple lenses, while it seems reasonable to expect that generic lenses also obey some coherence conditions.

This is why at the Statebox summit I was very curious to talk to other people more skilled than me about lawful generic lenses. It turned out this was a really interesting thing to do, since it seems we now have a good idea on how to solve the above issues. I really need to thank Jules Hedges, David Spivak, Brendan Fong, Christina Vasilakopoulou, Eliana Lorch, Andre Knispel, Stefano Gogioso and everyone else who was there for contributing to what follows.

Lens Recap

Let’s review briefly what a Lens is. It can be seen as a way to access and update a part of an immutable data structure S, through two functions

data Lens S T A B = Lens
  { g : S -> A
  , p : S -> B -> T
  }

For example, we could define a lens cc : Lens (A x M) (B x M) A B defined by

cc : Lens (A x M) (B x M) A B
cc = lens get put
  where
    get : A x M -> A
    get (a, m) = a

    put : (A x M) -> B -> (B x M)
    put (a, m) b = (b, m)

We will call every lens of this form a constant complement lens.

We will call a lens Simple if T = Sand B = A, that is if put does not have the ability to change types, but only to update the value of type A inside S.

Lens Laws

Traditionally the lens laws are stated for simple lenses as follows:

getput

Here • is the function S -> (S, S) that duplicates the input, and i : S -> S is the identity on S.

Alternatively, we could rewrite this as p s (g s) = s .

putget

Here, ◦ means that we are not using its argument S and i : a -> a is the identity on a.

This could be rewritten as g (p s a) = a .

putput

Here ◦ means that we are not using its argument a.

This could be rewritten as p (p s a) = p s .

We say that a simple lens is lawful or very well-behaved if it satisfies the three laws above.

On Lens Laws

I’ve always felt a bit bothered by the three lens laws because, though they make a lot of sense, they still feel a lot like God-given rules without a clear mathematical explanation.

Moreover, as presented above, we are able to state them only for simple lenses, and it feels pretty weird that general lenses do not need to satisfy any rule at all!

Also, lawful lenses seem to be of interest only for programmers, while in academic papers (with some exceptions such as this one) lawful lenses don’t seem to be considered to be very interesting, and generic lenses are usually investigated instead.

Before trying to understand something more about generic lawful lenses, let’s have a look at an easier example of optics, namely adapters.

Generic Lawful Adapters

An adapter is the simplest of all optics and it encodes the fact that we can adapt data between two different formats. It is defined as

data Adapter S T A B = Adapter
  { f : S -> A
  , t : B -> T
  }

An adapter is said to be simple if T = S and B = A. A simple adapter is lawful if f and t are each other’s inverses, i.e. f (t a) = a and t (f s) = s for any a : A and s : S .

From this point of view, it is clear that we cannot generalise this definition for generic adapters, because we have no way of composing f and t in the generic case.

On the other hand we can easily interpret a simple adapter as follows: it enables us to adapt functions A -> A to functions S -> S, and vice versa, using the isomorphism provided by f and t.

But now we can try to generalize this new point of view to generic adapters: we want a generic adapter to be lawful if it gives us a way to translate functions A -> B to functions S -> T in an isomorphic way, meaning that we can use it to adapt functions A -> B to functions S -> T and vice versa. Hence, we could give the following definition:

A generic adapter is lawful when both f and t are isomorphisms

It is now easy to observe that this definition is equivalent to the previous one when we restrict to the simple case, so this new definition is a generalization of the traditional one.

Generalizing to Lenses

Now that we were able to state a definition for a generic lawful adapter, let’s see if we can apply this insight to other optics.

If we look at the paper Categories of Optics by Mitchell Riley, we see that a generic optic is defined as

data Optic S T A B = exists M . Optic
  { g : S -> M ⊗ A
  , p : M ⊗ B -> T
  }

where ⊗ is a tensor in a symmetric monoidal category. If you don’t know what that is, don’t worry and interpret it as follows in our relevant examples.

• For lenses ⊗ is the product, so think to M ⊗ A as (M, A).
• For prisms ⊗ is the coproduct, or sum. In this case we think to M ⊗ A as Either M A.
• For adapters ⊗ is just the constant functor, so M ⊗ A is just A.

We can observe that for adapters this definition coincides exactly with the one we gave above. So, we restate our new interpretation of generic lawful adapters in this new more generic setting: an adapter is lawful if both g and p are isomorphisms.

However, with this new interpretation our definition can now be expressed for any possible Optic, not only for adapters! To state it again in its full generality, we say that

An optic o : Optic S T A B is lawful if g and p are isomorphisms

If we now interpret this definition for lenses, where ⊗ is the product, we see that we obtain that lawful lenses are all lenses Lens S T A B where S is isomorphic to M x A and T is isomorphic to M x B. But, up to isomorphism, this is exactly the definition of constant complement lenses we introduced above!

So, to check if our interpretation makes sense, we want to prove that a simple lens is lawful (in the traditional sense, i.e. it respects the three lens laws) if and only if it is constant complement.

Lawful Lenses are a Constant Complement

It is quite easy to check that a simple constant complement lens respects the three lens laws, so we are just going to prove that a lawful lens is constant complement.

The idea of this proof came to us thanks to this hint from Edward Kmett:

Edward Kmett on Twitter

@marcoshuttle @mstk @BartoszMilewski It is easiest to see (in tweet form) by looking at s -> (a -> s, a) as extracting the complement as an s with an a-sized hole, and the a. The fact that the former is injective (or s is uninhabited) is key to realizing this is actually just a proxy for the unnamed complement.

Let’s consider a Lens S S A A, defined by functions g : S -> A and p : S -> A -> S, which satisfies getput, putget and putput.

To prove our claim we need to define an M such that S is isomorphic to A x M.

First off, we observe that we can collapse our functions g and p into a single function

g&p : S -> (A, A -> S)
g&p s = (g s, p s)

This is really interesting because it is already sending S into the product of A with something else, where every element of this something else is of the form p s. Hence, we could try to define

M = { m : A -> S | ∃ s : S . m = p s }

At this point let’s try to see if we can prove that S is isomorphic to A x M. Let’s start by defining functions

f : S -> A x M
f s = (g s, p s)

and

h : A x M -> S
h (a, m) = m a

Next, we would like to prove that these two functions f and h are each other’s inverses.

Let’s check first that f ; h is the identity on S. We have

(f ; h) s = p s g(s)

which is equal to s by getput.

Finally, let’s check that h ; f is the identity on A x M.

(h ; f) (a, m) = (g(m a), p(m a))

By the definition of the set M, we know that m = p s for some s : S and hence

(g(m a), p(m a)) = (g(p s a), p(p s a))

which is actually equal to (a, p s) = (a, m) by putget and putput, respectively.

QED!

Conclusion

The fact that simple lawful lenses are constant complement lenses is folklore in the functional programming community (e.g. Lenses embody Products, Prisms embody Sums), but a proof of the fact was not easy to find, so I think that writing it down could be useful for future reference.

On the other hand, a definition for a generic lawful optic seems to not be present in the literature, and I think the approach proposed above works really nicely and can help us understand the origin of lens laws.

One interesting question to tackle now would be to understand how this generic notion of lawfulness translates to the profunctor optics encoding.

On Lawful Lenses was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

In this post, I’d like to take a closer look at the core bit of mathematics that makes a zkSNARK work: the elliptic curve pairing.

Introduction

Usually in cryptography we want our encryption functions to destroy as much information as possible. The inputs to these functions should appear to be completely unrelated to their outputs — unless, of course, you know the key.

However there are situations where we might want a little bit of information about the inputs to be recoverable, but not all of it.

For instance, suppose you had an online store and you wanted to check that your customer’s password was sufficiently complex without asking the user to actually reveal their password to you. First they would encrypt their password using some encryption function. Then you would need to be able to tell from only the encrypted output that the input to the function satisfied some condition.

This is possible. It requires a form of encryption that doesn’t destroy all information about its inputs. One mathematical object used to accomplish this is an elliptic curve pairing.

Elliptic Curve 101

A lot of this information can be found elsewhere, so I’ll just give the bare necessities. An elliptic curve is a polynomial that looks like:

The set of points (x,y) that are solutions to this equation plus a “point at infinity” form a group under a special addition rule.

Two points are added on elliptic curves by drawing a line through the two points. Because the curve is degree three this line will intercept the curve in a third place. That point of intersection is then reflected over the x-axis. Because of the y-squared term on the left side the curve is symmetric over the x-axis and this reflected point is also on the curve. The reflected point is the sum.

The geometric method of adding points is beautiful, but not so practical. There is a function that computes the sum of two points using on a curve by using their coordinates. Thankfully, this function is a rational function which is not too hard to compute. A point can also be doubled using a similar rational function. A double-and-add algorithm makes it practical to compute arbitrary multiples of an elliptic curve point, which I will write as n*g for integer n and some elliptic curve point g.

The point at infinity serves as the identity of the group. Two elliptic curve points that lie on the same vertical line are inverses.

Since addition and doubling are computed by rational functions on the coordinates, an elliptic curve group can be created using coordinates from any field. In a cryptographic setting we would use a finite field for the coordinates. Using a finite field destroys the nice geometric method of adding points by drawing lines between points, but the rational functions that compute adding and doubling are the same.

The Elliptic Curve Discrete Logarithm Problem

Something that is believed to be very hard to do with elliptic curve points is to compute the elliptic curve discrete logarithm (ECDLP). Given a point g on an elliptic curve and some multiple of that point n*g, what is n?

One of the most efficient algorithms for solving ECDLP, the baby-step giant-step method, runs in time exponential on the number of digits in the order of the elliptic curve group. For large groups this problem is highly impractical to solve.

Since this is problem is difficult, we can choose a secret n and be sure that it will remain secret even if we reveal g and n*g.

Why is it called discrete logarithm? Usually this problem is expressed in multiplicative notation, where the problem becomes computing n from g and g^n, essentially computing the base-g logarithm of g^n.

The Torsion Subgroup

An r-torsion subgroup is a subgroup formed of all elements g for which r*g = 0. The torsion subgroups of elliptic curve groups have a predictable structure. If we say E[r] is the the r-torsion subgroup of elliptic curve group E, then E[r] has this structure:

The caveats are that r must be relatively prime to the degree of the field E is defined on, and we may have to pass up to an extension of that field in order to get “all” of the points in E[r].

The Embedding Degree

The embedding degree k is the smallest degree field extension needed to get the entire torsion subgroup E[r].

The embedding degree k, as well as r, have an enormous effect on the security and efficiency of an elliptic curve and its pairing.

Elliptic Curve Pairings

An elliptic curve pairing is a function that takes a pair of points on an elliptic curve and returns an element of some other group, called the target group. Elliptic curve pairings have this nice essential property:

For some g1, g2, and g3 on the curve and integers a and b.

This is called bilinearity since the pairing is linear in both coordinates.

A pairing needs to have a further property, called non-degeneracy. For generators g1, g2:

The groups G1 and G2 are often different subgroups of a torsion group E[r], and the target group is either the rth roots of unity or a cyclic group isomorphic to it.

An Attack on Elliptic Curve Cryptography

Elliptic curve pairings were introduced by French mathematician André Weil in 1940 as a tool for solving an analogue of the Riemann Hypothesis for finite fields.

Pairings were later used as an attack on elliptic curve cryptography. A desirable property of a secure cryptosystem is that the Decisional Diffie-Hellman problem (DDH) is difficult in the underlying group. The DDH problem is this: given g, x*g, y*g, can you tell the difference between xy*g and a randomly chosen z*g? If that is difficult, the group has DDH. A group that where DDH holds can be used to hide the fact that the coefficients x, y and xy are related by multiplication.

The bilinearity property of pairings can be used to break DDH. (How? Compute e(x*g, y*g) and e(g, z*g). If they are equal, then xy = z with high probability.)

Since pairings can break DDH, a pairing can reveal that secret values are related by multiplication even though the values themselves remain secret.

Pairings are only able to show a relationship with one single multiplication. One would need a three-coordinate, trilinear function to reveal a relationship with two multiplications.

How are Pairings used in zk-SNARKs?

Pairings can reveal that secret values are related by addition and up to one multiplication.

If a statement can be transformed into a relationship with a single multiplication than it can easily be checked using a pairing. For example, suppose I want to convince you that I have an integer solution to a quadratic equation but I don’t want to reveal it. Here is an example equation:

I take my root a and a pair of elliptic curve points g1 and g2. I compute a*g1 and a*g2 give you the results, along with the points g1 and g2. Because of the ECDLP I can be sure you won’t be able to compute a and my root will remain a secret.

You use a pairing and compute:

By the bilinearity property, this is equal to:

If this is equal to 1, then a^2-2027a+16152 is equal to 0 with high probability. (The non-degeneracy condition, along with a large target group ensures this.) I have convinced you that my secret a really is a solution to the quadratic equation without ever revealing it.

In a zk-SNARK, elliptic curve pairings are used to check a system of quadratic constraints like the one above. The system of constraints is converted into a single large polynomial that has particular roots only if each of the quadratic constraints is satisfied.

Computing a Pairing

The best known algorithm for computing pairings is Miller’s algorithm. The algorithm is computationally expensive, as its complexity is polynomial on the order of the particular subgroup used in the pairing. For security, the order of this subgroup is very large, so the algorithm can take some time.

For this reason, efficient zero-knowledge protocols using elliptic curve pairings minimize the amount of pairing values that must be computed. The Pinocchio Protocol in PGHR13 needs 11 pairing values, while Groth16 needs only 3.

Want to know more about pairings?

The introductory sources on elliptic curve pairings on the internet are slim, but I found these helpful and illuminating:

Vitalik Buterin’s blog post:
https://medium.com/@VitalikButerin/exploring-elliptic-curve-pairings-c73c1864e627

Craig Costello’s Pairings for Beginners:
http://www.craigcostello.com.au/pairings/PairingsForBeginners.pdf

This talk by Dan Boneh:
https://www.youtube.com/watch?v=8WDOpzxpnTE

Want to know more about Statebox?

Check out our blog or watch some of our talks.

Elliptic Curve Pairings was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

A boolean circuit is a function that transforms a bitstring of m bits into a bitstring of n bits. It is called a circuit because it can be imagined as a diagram of wires and gates, where a 1 is a wire carrying a charge and a 0 is a wire with no charge. The gates can be logical operators like OR or NAND.

Boolean circuit satisfiability is NP-complete, so any problem in NP can be expressed as a boolean circuit. Due to the PCP Theorem, any decision problem in NP has probabilistically checkable proofs that can be verified in a reasonable amount of time.

Connecting everything together, we ought to be able to construct a non-interactive zero-knowledge proof that a morphism exists between two states of a system.

Libsnark is a library for creating zkSNARKs, and it has an efficient method for constructing SNARKs from two-input boolean circuits. (Two-input boolean circuits consist of gates where each gate has exactly two inputs.) Let’s look at how we can use libsnark to create a zkSNARK for a tiny example circuit.

An Example Circuit

Suppose we want a boolean circuit that can test whether a three-bit number is divisible by three. The input to our circuit is a bitstring of length three while the output is a single bit. Out of eight total three-bit numbers there are only two that are divisible by three: 011 and 110. Our circuit must be able to test any three-bit number and return 1 only on 011 or 110.

Designing the Circuit

Both correct bitstrings have a middle bit of 1 and each has exactly two set bits. These statements completely characterize the two bitstrings we are trying to select.

If the middle bit must be 1, then there is only one set bit left for the outer bits. So one of the outer bits must be 1 and the other must be 0. We can use an XOR gate to test that the outer bits are opposites. Then all we need to do is test that the middle bit is 1. Here is a diagram of a two-input boolean circuit with two gates and five wires that accomplishes the task.

How a Boolean Circuit becomes a SNARK

Most SNARKs are based on a Quadratic Arithmetic Program which is constructed from an arithmetic circuit. The arithmetic circuit is first written as a rank-1 constraint system (R1CS), then a special polynomial is constructed from the R1CS that has roots corresponding to each gate of the arithmetic circuit. Then it is possible to check that each gate of the arithmetic circuit is satisfied by checking that the polynomial has the expected roots.

While it is possible to convert boolean circuits into arithmetic circuits and use a quadratic arithmetic program, it is not very efficient to do so. Instead, we can use what is called a Square Span Program.

Square Span Programs

A Square Span Program is another system for building a SNARK that is designed to be efficient for boolean circuits. Each boolean gate is written as a linear combination of the input and output bits. For example, if a and b are bits, then 2a + 2b + 4c - 5 will be either 1 or -1 if NAND(a,b) = c. Each type of boolean gate gets one of these linear combinations that equal -1 or 1 if the gate is satisfied. Then all that needs to be checked is that(2a + 2b + 4c — 5)² = 1. This is called a Unitary Square Constraint System (USCS). It is similar to a R1CS but is much more simple for boolean circuits and produces smaller SNARKs. Libsnark can express a boolean circuit as a USCS.

Writing Our Circuit in Libsnark

Writing our boolean circuit in libsnark is quite simple. For each gate, we specify its left and right input wires, its output wire, its gate type, and whether or not the gate is an output of the entire circuit.

Gate Types

A two-input boolean gate can be represented as a truth table for its inputs and output. Here is the truth table for NAND:

| a | b | c |
|---|---|---|
| 0 | 0 | 1 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 0 |

The last column specifies exactly how NAND functions for each input. Since the last column is 1110, NAND is given an op code of 14. There are sixteen possible two-input boolean gates and libsnark recognizes each one.

Circuit Output Gates

The proof generated for a boolean circuit is a proof that each gate behaves according to its type and that the outwire of any circuit output gate is 0. This is the opposite of the usual intuition for circuits and will cause the circuit we designed earlier to fail verification in libsnark. We can easily fix this by changing the output gate of our circuit to its negation, so that AND becomes NAND.

Our corrected circuit:

Specifying our Circuit in Libsnark

Our circuit is specified in libsnark like this:

int main()
{   
    // Choose the field
    typedef libff::Fr<default_tbcs_ppzksnark_pp> FieldT;

    // Initialize public parameters
    default_tbcs_ppzksnark_pp::init_public_params();

    // Initialize the circuit
    tbcs_circuit div_by_3;

    // Set the circuit size
    div_by_3.primary_input_size = 0;     // number of PUBLIC inputs
    div_by_3.auxiliary_input_size = 3;   // number of PRIVATE inputs

    tbcs_gate g1;
    tbcs_gate g2;

    g1.left_wire = 1;
    g1.right_wire = 3;
    g1.type = tbcs_gate_type(6);      // XOR
    g1.output = 4;
    g1.is_circuit_output = false;

    g2.left_wire = 4;
    g2.right_wire = 2;
    g2.type = tbcs_gate_type(14);     // NAND
    g2.output = 5;
    g2.is_circuit_output = true;

    div_by_3.add_gate(g1);                   
    div_by_3.add_gate(g2);

Valid Circuits

For a circuit to be considered valid by libsnark, the output wire of each gate must be exactly one more than the number of previous wires already specified. Also, the left and right input wires must each be less than the output wire.

Libsnark provides a constant wire (wire 0), so the first input wire is wire 1.

Specifying an Assignment

An assignment to our circuit is a vector of bits, with one bit for each wire (including the internal wires). Here is a correct assignment showing 110 (six) is divisible by three:

vector<bool> assgn_six = {1,1,0,1,0};

Note that the last wire needs to be 0 because we marked the last gate as a circuit output.

Create the Proving and Verifying Keys (Trusted Setup)

const tbcs_ppzksnark_keypair<default_tbcs_ppzksnark_pp> keypair =
   tbcs_ppzksnark_generator<default_tbcs_ppzksnark_pp>(div_by_3);

Make an Assignment to the Circuit

// public input is empty                               tbcs_primary_input pi = {};

// private input
tbcs_auxiliary_input ai = assgn_six;

Generate a Proof

tbcs_ppzksnark_proof<default_tbcs_ppzksnark_pp> proof = tbcs_ppzksnark_prover<default_tbcs_ppzksnark_pp>(keypair.pk, pi, ai);

Verify the Proof

bool verified = tbcs_ppzksnark_verifier_strong_IC<default_tbcs_ppzksnark_pp>
(keypair.vk, pi, proof);

Thank you to Christian Lundkvist and Howard Wu for their helpful libsnark tutorials on which this code is based.

Boolean Circuits in Libsnark was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

Disclaimer: Before you roast me, this post is not meant to judge any person or organisation and what they did or did not do. In particular, I have nothing against ETH, ETC, the DAO team or the hacker. All of them did and are doing incredibly useful things.

There are ongoing online discussions regarding “blockchain governance”. I want to add a few cents to this, from the point of view of someone understanding a thing or two about foundations of mathematics and security engineering.

For some context regarding the governance discussion, check:

- The blogpost “Against Szabo’s law”
- A response “In Defense of Szabo’s Law”
- This recent twitter thread which made me write this

What is the point of Szabo’s law / ethos?

> Zamfir: “Do not implement changes to the blockchain protocol unless the changes are required for the purpose of technical maintenance.”

> Shapiro: Szabo’s ethos: a “social trust minimisation approach”

Code is Law

Before we dive into that, let’s talk about “code is law”. This notion refers to smart contracts and suggests that “the law” is not coming from what is written down in a natural language contract and the lawyers and court’s interpretation of it, but instead a “smart contract” blindly and mechanically executes its code and nobody can do anything about it. Because the code is public and because the execution is deterministic*, you know exactly what kind of contract you are interacting with. (*same input, same behaviour)

So the most important aspect of *code is law* is that -but hold on- it makes it unambiguous how the contract should be interpreted, unlike the natural language version of a contract.

At this stage, we need to understand the code that creates the ‘simulation’, namely the runtime, the smart contract host, (for example the Bitcoin or Ethereum daemons).

The runtime in principle does not distinguish between smart contracts, they are all on equal footing. So you could write a very simple, safe contract, or you could have a very complicated, buggy contract. The runtime does not care and just executes the code as is.

In order to understand unambiguously what a SC does, you need to understand exactly what the machine does AND what the smart contract tells the machine to do. The instructions in the smart contract are a form of “machine code” running on a virtualised process, called a virtual machine. (EVM, Ethereum virtual machine in ETH case).

Roughly, we call the machine code in smart contracts ‘syntax’ and the behaviour or meaning that we expect the “semantics”.

There are two ways to describe the semantics of this virtual machine precisely:

- operationally, or a step-by-step description. If you see instruction A and you are in state X, then go to state Y and change the memory at location…

The nice part of operational semantics is that it is very close to how the machine actually operates. For example, here you see this in action; it’s how a Turing machine works / is described:

The not so nice part is that it is very difficult to understand what it’s happening if you zoom out from the local view, to the effect of the entire calculation. For instance, in the video it is not exactly clear right away that all the erasing and writing ones and zeros is actually adding or counting, etc.

- the other way of describing semantics is denotational.

Here, instead of giving the step by step instructions, you show that your syntax is just another way of speaking about a specific mathematical structure. Without going into too much detail (could be a whole blog series), the point here is that you can use existing theories about this structure to reason about the “global” behaviour.

I am mentioning this to show you that even though it is exactly known for each input what the contract does, depending on the complexity of the virtual machine it may still be impossible for a human, or even a computer to reason about all possible things that can happen with the contract.

Mathematics may look complicated, but it is really mainly formed to be easy to reason about. You just look at the transition table of a Turing machine, and you see each step. Easy to understand what this does! But you cannot create a conjecture about all possible ways it can run, let alone proof that conjecture easily, except for some very special situations.

In fact, a famous theorem states that a universal Turning machine (a TM that can simulate any other Turing machine, having this property in a VM or programming language is called Turing completeness) is that there are programs for which there does not exist an algorithm that can decide if the program will terminate or not.

Very concretely, this means that you could construct a transaction for a blockchain and all the nodes in the network would never finish processing the transaction and there is no way to detect this before you start working.

This is one of the reasons Ethereum has Gas (which I am going to call fuel). If you are out of fuel, the computation stops. So trivially the EVM is not Turing complete.

But this still does not help with making reasoning about SC behaviour any easier. You can also read this as more generally: **if you have Turing completeness, it becomes impossible to exclude unwanted behaviour automatically in all cases.**

This is why I have always argued against Turing completeness in the EVM and why I argue for formal semantics. It is an easy way out to take a TM and restrict it with fuel. But I want to be able to reason in the large about the behaviour of smart contracts.

Back to Governance

There is another very (in)famous example of governance in action, “the DAO fork”, probably better called the “DAO bailout”.

Let’s quickly summarise what happened there.

A particular smart contract running on the Ethereum blockchain (the DAO contract) was implemented in a rather complicated way and it turned out that there was some ‘emergent behaviour’ that was not exactly clear from the code immediately. In fact, it was even pointed out to the smart contract developers that their code was very complicated and might have bugs, but they brushed it off with “we don’t see any bugs with it, so it’s probably fine”. But it was not and had a critical security flaw which was eventually exploited by someone.

This is where the friction starts.

If “code was law”, then the DAO contract (which anyone was free to “sign into”) said in a not-immediately-obvious way that anyone could take all the money if they followed a very specific protocol.

Anyone with some security training (either offensive or defensive) knows that large complicated codebases are a Bad Thing(tm).

Would you sign a huge contract written in legalspeak where all pages refer back and forth to conditions in other pages etc, and on top of that you barely understand the legalspeak in the first place (machine code/solidity), let alone the implications of the laws holding particular jurisdiction this ‘legal code’ applies to? (the EVM semantics) **You probably won’t, because you don’t want to get into deep trouble signing something you don’t understand.**

Furthermore, if you are the organisation that is handing out the contracts (DAO), and you decide to write the legalese yourself instead of hiring expensive/experienced lawyers (~ someone that formalizes your contract first using paper math and then on a computer, ie. us) and then it turns out your amateur contract has some very bad unintended side effects and the signing party uses those to their benefit, well, … who’s at fault here?

Now, clearly with a paper contract, you can say: “Hey wait, you are interpreting this text wrong, I didn’t mean that”. And this is what expensive lawyers and courts are for, to figure out who is wrong.

Even so, in the DAO case, are you really sure the SC behaviour used by the “attacker” was unintentional? Crazy suggestion, you say? Consider this:

- structural issues about the security process and code base were pointed out to the team before attack was engaged, the team brushed this off
- imagine you are the only person in a team trying to point out there is a security issue or the approach is wrong and they laugh you repeatedly; you could turn around and exploit it at some point, so you silence yourself and instead say: “yeah let’s keep hacking on this reentrant code, looks good to me”
- at that time not many people would have the background to understand reentrancy bugs in EVM, likely the attacker had some stash ETH (if he/she didn’t, you’d probably attack straight away)
- so maybe the DAO was the ETH biggest scam so far?

FWIW, I really don’t think this happened, but I just want to point out the possibility and how non-obvious the intended behaviour was.

You might also say that clearly everyone that was investing into the DAO wanted it not to get hacked, the terms & conditions of the investment contract clearly gave a different impression about the behaviour of the code.

But this is the point, you DO-NOT-WANT to have a piece of natural language text that says what the code _should_ do and if later it turns out there are discrepancies, you just resolve that in court instead (as a form of governance).

Firstly, this problem already exists in the non-decentralised software world.
It is very inefficient and expensive to go from imprecise specification to precise code. As the programmers have to turn the spec into code, usually they discover incomplete specifications, inconsistencies or plain impossibilities. So they need to give feedback to the spec author, which then updates specs, etc. very time consuming and waterfall vs agile is exactly about making this iteration loop as fast as possible.

So how was this DAO situation resolved?

Let’s call the runtime ‘the simulation’, because as far as a smart contract is concerned this is all it sees and all interactions come from this environment. Zooming out, we see it’s simulations (formalised “virtual” worlds) all the way down:

If we then look at the user-defined ones, we can distinguish different levels of ambiguity in those contracts.

The green box represents the simplest contracts that have very limited functionality and for which you can (and have) proof that there is no other behaviour *at all* possible than what is in the contract. I call this closed, because it assumes a “closed universe”, every possible thing that can happen in *The Simulation* is considered in the security proof, interaction with other contracts, but also all things in ‘The Real World’, etc.

You can also have (yellow) very simple contracts that are fully understood, but because they interact in a more complicated way with the rest of the simulation, we cannot include everything in the security proof, so it is maybe possible that some undescribed and unconsidered outside mechanism breaks the contract. But you are still following the rules of the simulation.

Then there is the Turing complete contract, where nobody bothers really to proof anything; and a fancy website, flimsy white-paper and pseudo rigorous arguing should be enough to convince some people to sign the contract. IMHO* all hope is lost.

What the Ethereum Foundation did was what I’d call *governance at the simulation level*. Some “hand of a (pretending) God” decided to change the rules of the simulation, to take a very specific smart contract and bail them out.

*This violated Szabo’s law directly**. What is now called Ethereum classic is the chain that kept running the unmodified simulation code, the ETH chain is the one that runs exceptional code that gives the funds back to the DAO contract, ie. the one where governance changes the rules of the universe.

Conclusion

A different reading of Szabo’s law could be something like this.

In general, less code = fewer opportunities for bugs or emergent behaviour.

But that is not all, as in algebraic methods, we seek to have well behaved, very restricted systems that have nice properties and are “reasonable” (= able to reason mathematically about it).

A small amount of code does not imply that, per se. For instance, in a few lines of code one can write a Turing complete virtual machine, the extreme case where we have a proof that there are unreasonable programs (halting problem).

Or in the other direction, **at Statebox we spend a nearly-insane amount of effort on avoiding Turing completeness, exactly for this reason**, but with a tiny addition (`AND NOT IS ZERO`) to a single if statement, we would gain the ability to simulate a Turing machine.

If you are a programmer and you don’t have an understanding of these subtle issues, you’d think, what’s the problem, a single line change and it does not make the semantics really any more complicated. Well, operationally speaking it doesn’t, but denotationally we are looking at a very different beast suddenly.

Some examples

Many great examples of hacks or exploits that use this fact are around. For instance, people playing Super Mario in Starcraft.

(screenshots from RECON-BRX2018 talk “Starcraft, emulating a buffer overflow for fun and profit”)

This is not supposed to be possible, Starcraft maps are Starcraft maps and the game should reject illegal maps. but the Super Mario map is legal, it just exploits the fact that it can simulate ANY kind of program. once the Turing machine is found, you can build tools on top to work in the *new simulation*:

This is more or less how such “privilege escalation” exploits usually work.

Furthermore, legal governance is something that *itself* is a contract, namely the ‘real world laws’.

So you want to move this up into the smart contract world, and not apply it to the simulation. Doing this at the simulation level is similar to backdoor-ing crypto.

If we cannot rely on the precise behaviour of the simulation and the smart contracts, then we cannot rely on our proofs anymore and we can NEVER build a fully secure system.

If *instead* we say code is the law, there is no bailout/undo unless you build it in, then we have something to rely on. This also immediately implies that you only want to have _the utmost max A-grade level security_ for smart contracts, similar to when you launch a satellite. Because you cannot easily go up into space and press the reset button, the effort is put upfront because the software MUST NEVER fail, precisely because there is no undo button or big brother that you can go to to bail you out of your own mistake.

Note on Mechanised Governance was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

You actually hear a lot of talking about functors in the context of functional programming. Together with other derived concepts such as applicatives and monads, functors are one of the basic abstractions used to structure the flow of programs.

In this post we will explore in detail the link between general category theory and functional programming, showing that the latter is just one example of the former.

Make sure to read it all until the end, where a little surprise is waiting for you.

Simply put, the main reason why category theory is so relevant for programming is that, in a certain sense, any programming language can be seen as a category.

This is quite a bold statement and in fact it is not one hundred percent true, but there is a lot of truth behind it, so let’s try to make it more precise.

To obtain a category from a given programming language we need to choose carefully which are the objects and which are the morphisms.

The objects will always be the types available in the type system of the language. They could be native types, like int or string, or more abstract types like (list int, string -> int). It’s important to note that in a dynamic language, where changing the type of values is allowed, there is only one big type which contains every possible value. On the other hand, in a statically typed language with a very expressive type system we can have a lot of objects in our category. This is why the categorical approach makes much more sense in strongly typed languages.

So, types are objects in our programming language category, but what are morphisms, then? Well, morphisms are the so-called pure functions, that is, functions which are referentially transparent as expressions. This excludes from being a morphism all the (so-called) functions which have side effects (e.g. throw exceptions, make network calls, generate random numbers, …) or which rely on some external state. Therefore in procedural languages many functions which we are used to write can not be taken into account as morphisms of our category.

Luckily enough, there are programming languages where we don’t have the possibility of writing impure functions, and in such a case every possible function corresponds to a morphism in the category.

Idris as a category

In Idris, thanks to dependent types, we have the possibility of encoding the above described category, specialized for the Idris programming language, in Idris itself! Let’s see how we can do it in practice, defining a Category made with Idris types and functions.

We said that objects of our category are types, so the type of our objects will just be Type.

If you recall, the signature of the record field mor which describes morphisms of a category is obj -> obj -> Type, where obj is the type of objects. So in our case we have Type -> Type -> Type; as we said above this needs to encode all the functions between two types, so it will be practically defined as

TypeMorphism : Type -> Type -> Type
TypeMorphism a b = a -> b

Our category is slowly shaping itself, now we need to define identities and composition, but that’s almost trivial, since we are talking about functions

identity : (a : Type) -> TypeMorphism a a
identity a = id

compose :
     (a, b, c : Type)
  -> (f : TypeMorphism a b)
  -> (g : TypeMorphism b c)
  -> TypeMorphism a c
compose a b c f g = g . f

As one could expect, identities and composition of the category are just identity functions and function composition.

The axioms for being a category, left and right identity and associativity, are at this point trivial and they can all be implemented as Refl.

Summing up, we can formally define our category as follows

typesAsCategory : Category
typesAsCategory = MkCategory
  Type
  TypeMorphism
  identity
  compose
  (\a, b, f => Refl)
  (\a, b, f => Refl)
  (\a, b, c, d, f, g, h => Refl)

Functors are functors (part 1)

As soon as we have a category, our instinct should be that of immediately looking for what functors are in that category. For the above category the answer is that functors are, well, functors.

In Idris we already have a concept of functor, which looks as follows

interface Functor (f : Type -> Type) where
  map : (func : a -> b) -> f a -> f b

interface Functor f => VerifiedFunctor (f : Type -> Type) where
  functorIdentity : {a : Type}
                 -> (g : a -> a)
                 -> ((v : a) -> g v = v)
                 -> (x : f a)
                 -> map g x = x
  functorComposition : {a : Type}
                    -> {b : Type}
                    -> (x : f a)
                    -> (g1 : a -> b)
                    -> (g2 : b -> c)
                    -> map (g2 . g1) x = (map g2 . map g1) x

We would like to prove that an Idris VerifiedFunctor can be seen as a CFunctor as we defined it, so we would like to implement a function with the following signature

functorToCFunctor :
     VerifiedFunctor f
  -> CFunctor typesAsCategory typesAsCategory
functorToCFunctor {f} func = ?cFunc

The first bits of the implementation are pretty straightforward

functorOnMorphisms :
     VerifiedFunctor f
  -> (a, b : Type)
  -> TypeMorphism a b
  -> TypeMorphism (f a) (f b)
functorOnMorphisms _ _ _ (MkTypeMorphism g) =
  MkTypeMorphism (map g)

functorToCFunctor {f} func = MkCFunctor
  f
  (functorOnMorphisms func)
  ?funcPreserveId
  ?funcPreserveComp

As you could probably guess, we use f itself to map objects and the map function provided to us by the Functor instance, to map the morphisms.

Now we are left to show that our definition of functor is lawful, that is, it respects identities and composition. But, as a matter of fact, with our current definitions this is actually not possible; in the next paragraph we’ll explain why and we’ll adapt things to solve the issue.

Intensional and extensional equality

If you try to prove that our functor preserves identity, you’ll find yourself at the point where you need to provide evidence that id : f a -> f a and (map id) : f a -> f a are the same function. It turns out that equality between functions is quite a complicated subject; the main question is: when do we say that two functions are equal?

From a mathematical standpoint, if we look at functions as relations, it makes sense to say that two functions f, g : a -> b are equal whenever, for any element x : a, we have f x = g x. This definition of equality is called extensional and it observes only the external behaviour of functions.

From a computational point of view, instead, it may make sense to have a more strict criterion to differentiate between functions. For example, if we consider the functions \x => 2 * x and \x => x + x defined on the natural numbers, do we want to always consider them as the same function? Or, if we consider several different sorting algorithms implementations, do we want to consider them equal as functions?

For a machine it is definitely easier to check whether the abstract syntax trees used to define two functions are equal, but it could turn out very hard to understand whether two functions are extensionally equal, because it would have to compute the functions for every possible value. Therefore in programming the default form of equality between functions, called intensional, concerns the equality of internal definitions.

Coming back to our functor definition, we can now spot where the problem is. Our definition of equality between functions uses intensional equality, while the VerifiedFunctor interface is using extensional equality. Since intensional equality is more fine-grained that the extensional one, we can not hope to adapt the VerifiedFunctor interface to our definition. We will need to slightly change our definitions to use extensional equality.

What we need to do is change our definition of morphisms, so that we can assert that extensional equality holds

record ExtensionalTypeMorphism (a : Type) (b : Type) where
  constructor MkExtensionalTypeMorphism
  func : a -> b

postulate
funExt :
     {f, g : ExtensionalTypeMorphism a b}
  -> ((x : a) -> func f x = func g x)
  -> f = g

We wrap functions in a new type ExtensionalTypeMorphism and we postulate that two elements of this type are equal whenever we have a proof of the extensional equality of the inner functions. This corresponds to quotienting the TypeMorphism type with respect to the equivalence relation given by extensional equality. Moreover, we can use this new type for defining morphisms of a new category which we will call typesAsCategoryExtensional.

Functors are functors (part 2)

We can now come back to prove that VerifiedFunctors can be seen as CFunctors. Let’s resume from where we left off, adjusting things with our newly introduced ExtensionalTypeMorphism and typesAsCategoryExtensional.

functorToCFunctor :
     VerifiedFunctor f
  -> CFunctor typesAsCategoryExtensional    
              typesAsCategoryExtensional
functorToCFunctor {f} func = MkCFunctor
  f
  (functorOnMorphisms func)
  ?funcPreserveId
  ?funcPreserveComp

We can now use our postulate funExt to complete the missing pieces

functorPreserveId :
     (func : VerifiedFunctor f)
  -> (a : Type)
  -> functorOnMorphisms func a a (extIdentity a)
   = extIdentity (f a)
functorPreserveId _ a =
  funExt (\x => functorIdentity {a} id (\v => Refl) x)

Here we use the functorIdentity field of the VerifiedFunctor interface, which gives us the extensional equality between id : f a -> f a and (map id) : f a -> f a. Using funExt we can transform the extensional equality into a concrete equality and complete the proof.

Similarly, we can prove that an Idris functor respects function composition according to our definition.

functorPreserveCompose :
     (func : VerifiedFunctor f)
  -> (a, b, c : Type)
  -> (g : ExtensionalTypeMorphism a b)
  -> (h : ExtensionalTypeMorphism b c)
  -> functorOnMorphisms func a c (extCompose a b c g h)
   = extCompose (f a) (f b) (f c) (functorOnMorphisms func a b g)  
                                  (functorOnMorphisms func b c h)
functorPreserveCompose
  func _ _ _
  (MkExtensionalTypeMorphism g’)
  (MkExtensionalTypeMorphism h’)
  = funExt (\x => functorComposition x g’ h’)

Conclusion

Today we saw how types and functions of a programming language, Idris in our case, can be interpreted as a category. Moreover, we proved that the concept of functor commonly used in functional programming correspond exactly to functors from a categorical point of view. This implies that we can use concepts from category theory, reason with them in their very abstract setting, and then apply what we found out to our software. Or, from another point of view, we can try to write our software thinking just in terms of categories, so that we know that our code can be used not only to talk about programming languages, but has a broader scope and application.

I promised a little surprise at the beginning, so here it is: we released open source our category theory library! You can have a look at the parts of the code which I didn’t have the time and space to investigate in this series of blog posts. It would be really awesome if you could provide us with some feedback on it and, if you will, maybe contribute with a new category or some other concept we haven’t defined yet.

Programming Languages as Categories was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

Trying to solve the same problems using the same tools over and over again and expecting to repeatedly get different and successful results is indeed pure insanity.

It is by no means an exaggeration to think that we are entrenched in and debilitated by the same patterns of action that formed our personal and professional selves. Whether we like it or not, we, as social animals, belong to certain cultures, (whether it is the Google culture or the Rust community or whichever nation state you’re from) and it’s only human that we appropriate thoughts and behaviours from those groups. I invite you to take a step back and try to analyze things from a different perspective.

In dealing with complex systems, (and we are dealing with complex systems on a daily basis; we are, as a matter of fact, immersed in one) it is imperative that we explore novel approaches. I understand that you feel very strongly about your insert imperative programming language here, because it gets things done and it’s good enough for what it is that you are doing, even though you spend x amount of hours trying to fix bugs, making your fellow devs understand what you were trying to do or even to understand yourself what you wrote a week ago. I also understand that you dismiss visual languages because that one time 2 years ago you played with a version of insert visual language name here and it sucked because of the UI, etc. But in order to understand what Statebox is about you need to get out of your comfort zone and be willing to embrace a change of perspective.

For Statebox to come into existence, that change of perspective needed to happen. The idea of using Petri nets and category theory in an intertwined manner does not come naturally, to say the least. It is, in a sense, an unprecedented way of thinking and solving problems — which turns out to be more efficient than anything else out there. And it helps immensely with the increasing complexity of systems. Statebox is actually built for that!

Moving fast and breaking things simply doesn’t cut it anymore

Nowadays, companies tend to pitch their business models of siloed and quasi innovative problem-solving technology. The whole idea of specialization and offering solutions to particular problems has been haunting us since the time of Adam Smith. Somehow, people seem to forget that no problem arises in isolation. Do we even consider anymore that for a particular problem to come into existence, a complex web of context dependent actions need to happen? And what is the point, may I ask, of solving those problems if they will keep happening, since the source that is causing them has not been addressed? The same way we feed pesticide infested food to millions of people who end up developing health problems from it (not to mention the ecological disaster caused by growing monocrops), then develop and capitalize on medicine that treats those same health problems, the approach to writing code seems to be just as flawed. Badly written code can have deep societal consequences, as well. If someone can change the course of this, it is the developers themselves.

A case for bottom-up formal verification

To illustrate, let’s take the over-referenced example of the DAO hack. We know what went wrong with it, but somehow, after all these years, typed languages are still not used to write smart contracts. Devs are still hammering away using the usual untyped tools, while other companies come into existence promising quick fixes to patch up what goes wrong with said method. And while operational semantics and model checking serve their purpose in the current ecosystem, there is a better way. We believe using formal tools to begin with is the way to go.

Bottom-up formal verification uses category theory and type theory. It creates a solid, verified foundation on which other layers can be built. This approach is very general and reusable. And while in the beginning it is abstract and limited in functionality, it proves extremely advantageous in the long run.

This is in contrast with the usual approach to formal verification, which consists in taking a piece of software, formalizing its operational semantics using an environment like Coq, and making sure that everything is correct. The top-down approach is particularly weak to scaling, since it allows the codebase to grow in any direction, often in an unprincipled way. It’s not a mystery that producing formally verified code in this way is a very slow and expensive process.

On the contrary, relying on a strong type-system — such as those with dependent types — allows to prove properties of the software bottom-up, as the developing goes. In this setting, developing is slower, but after a given “module” has been completed its behavior will be completely known, and we will be able to compositionally plug in into a bigger structure.

The beauty of category theory

This is the beauty of category theory: it allows you to build sound, verifiable code out of little pieces of code. Statebox has built-in compositionality both within its code (which is verified bottom-up) and within its paradigm (programming with Statebox ensures a compositional bottom-up approach to verification). Moreover, since programming with Statebox is visual, it offers what is probably the easiest way to produce verified software on the market.

If you are interested in functional programming and category theory, do check out our other Medium posts and the resources on our website.

Update

The first business application of the Statebox language is being developed on process.io. Sign up for a beta trial now!

What’s the Deal with Statebox, Anyway? was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.

In our last post we provided some examples of categories which show how, with our newly defined concept of category, we can generalize a lot of already well known mathematical structures.

We understood how a category gives us a context where we can talk about composition, being assured that the desired properties as identity and associativity hold. But sometimes, we would like to be able to jump from one context to another, making connections between the two. But what does this mean? When is a connection between two contexts meaningful? The answer a category theorist could give is that a connection between two contexts is meaningful when the invariants present in our starting context are preserved by the connection itself.

In the world of category theory, these connections are represented by functors, which provide ways to go from one category to another respecting the categorical structure.

What is a functor

Simply stated, a functor is a mapping between categories which preserves their structure, but let us see what this means in all its details.

First thing, a functor goes between two categories, which we will call cat1 and cat2, and we can start defining it in Idris as

record Functor (cat1 : Category) (cat2 : Category) where

Now we want to define how our functor acts on cat1. Remember that a category is composed by objects and morphisms, so we will need to define how Functor acts on both. Let us start with objects:

mapObj : obj cat1 -> obj cat2

We simply have a function, which we call mapObj, which provides a way to map objects of cat1 into objects of cat2.

For morphisms, we don’t want to have just a function that maps a morphism of cat1 to a generic morphism of cat1, but we want to impose some coherence conditions on the source and the target of the mapped morphism. This amounts to say that, if we have a morphism a -> b in cat1, then we would like to map it to a morphism mapObj a -> mapObj b, respecting the action of mapObj on the objects of cat1.

mapMor : (a, b : obj cat1)
      -> mor cat1 a b
      -> mor cat2 (mapObj a) (mapObj b)

To make this explicit we add to our Functor record a mapMor function which tells how, for any two objects a and b of cat1, we can map a morphism between a and b to a morphism, this time in cat2, between mapObj a and mapObj b.

It is probably the case to stress here that in general, in category theory mapObj and mapMor are indicated with the same symbol, because it is possible to distinguish between the two usages just by checking if their argument is an object or a morphism. But, since here we are actually trying to explain category theory to the Idris compiler, we are required to be extremely pedantic and precise, so we need to use two different symbols.

Are we done now, since we can map objects and morphisms? Don’t be in such a hurry, we have mapped only the bare structure, but that’s not all there is to a category. Actually, probably the main important idea laying around in a category is the one of composition, so when defining a functor we really need to ensure that we are preserving composition too.

preserveCompose : (a, b, c : obj cat1)
               -> (f : mor cat1 a b)
               -> (g : mor cat1 b c)
               -> mapMor a c (compose cat1 a b c f g)
                = compose cat2
                          (mapObj a)
                          (mapObj b)
                          (mapObj c)
                          (mapMor a b f)
                          (mapMor b c g)

We introduce a new field preserveCompose in our Functor record which tells us that for any objects a, a and c and morphisms f : a -> b and g: b-> c of cat1, we obtain the same result if we do on of the following:

• compose f and g in cat1 and then map the result with mapMor
• map f and g into cat2 using mapMor and then compose the results in cat2

In other words, we can say that we can swap the order of composition and functor application, or better yet, that functor application preserves composition.

Composition in a category actually comes also with the concept of identity, so a functor needs to preserve that too.

preserveId : (a : obj cat1)
          -> mapMor a a (identity cat1 a)
           = identity cat2 (mapObj a)

This condition tells us that, given any object a of cat1, the identity morphisms of a is mapped by mapMor to the identity morphism, this time in cat2, of mapObj a, as one would expect.

Examples of functors

Now that we have a complete definition of a functor, it is time to see some concrete examples, investigating what functors are in the categories we introduced in our previous post.

Discrete categories

As we discussed last time, discrete categories are categories where the only morphisms are the identities of the objects. This means that, in practice, we can’t talk about composition in discrete categories. Everything is isolated in its own world. As a consequence, when defining a functor between discrete categories, we don’t need to bother with how mapMor will work, because it will even send only identities to identities, but we can concentrate only on mapObj.

Actually, if we cave two discrete categories cat1 and cat1, which sets of objects are respectively object cat1 and object cat2, every function f : object cat1 -> object cat2 defines a functor. We can actually prove it as follows:

functionMapMor :
     (f : a -> b)
  -> (x, y : a)
  -> DiscreteMorphism x y
  -> DiscreteMorphism (f x) (f y)
functionMapMor f x x Refl = Refl

functionPreserveCompose :
     (f : a -> b)
  -> (x, y, z : a)
  -> (g : DiscreteMorphism x y)
  -> (h : DiscreteMorphism y z)
  -> functionMapMor f x z (discreteCompose x y z g h)
   = discreteCompose (f x)
                     (f y)
                     (f z)
                     (functionMapMor f x y g)
                     (functionMapMor f y z h)
functionPreserveCompose f x x x Refl Refl = Refl

functionAsFunctor :
     (f : a -> b)
  -> CFunctor (discreteCategory a) (discreteCategory b)
functionAsFunctor f = MkCFunctor f
                                 (functionMapMor f)
                                 (\_ => Refl)
                                 (functionPreserveCompose f)

Monoids

We know that a monoid could be seen as a degenerate category with only one object, where the composition in the category is nothing else than the binary operation of the monoid and the identity morphism is the identity element of the monoid.

What about functors between such categories? Suppose we want to define a functor between categories monoidAsCategory monoid1 and monoidAsCategory monoid2; well, we don’t have a lot of choice for mapObj, we need to map the only object of the starting category to the only object of the target category. For mapMor, we need to map morphisms of monoidAsCategory monoid1 to morphisms of monoidAsCategory monoid2; but morphisms in these categories are just elements of the respective monoids. Therefore we need a function fun from monoid1 to monoid2. Moreover, for it to be the morphism component of a functor, we need it to respect composition and the identity morphism; but this amounts exactly to say that fun must be a monoid homomorphism! We can actually prove that for every monoid homomorphism between monoids monoid1 and monoid2, we can build a functor between their associated categories monoidAsCategory monoid1 and monoidAsCategory monoid2.

record MorphismOfMonoids domain codomain where
  constructor MkMorphismOfMonoids
  func : domain -> codomain
  funcRespOp :
       (VerifiedSemigroup domain, VerifiedSemigroup codomain)
    => (a, b : domain)
    -> FunctionRespectsOperation a b func
funcRespId :
       (VerifiedMonoid domain, VerifiedMonoid codomain)
    => FunctionRespectsIdentity func
morphismOfMonoidsToFunctor :
     (monoid1, monoid2 : Monoid)
  -> MorphismOfMonoids monoid1 monoid2
  -> CFunctor (monoidAsCategory monoid1)
              (monoidAsCategory monoid2)

morphismOfMonoidsToFunctor
  monoid1
  monoid2
  (MkMorphismOfMonoids fun frOp frId) =
MkCFunctor
  id
  (\_, _ => fun)
  (\_ => frId)
  (\_, _, _, f, g => frOp f g)

Preorders

Let us recall that a preorder can be seen as a category with at most one morphism between any two objects, where the order structure is reflected in the presence or absence of a morphism.

Now, how does a functor between two such categories cat1 = preorderAsCategory {t1} {po1} and cat2 = preorderAsCategory {t2} {po2}, where po1 and po2 are partial orders respectively on t1 and t2, look like? It is constituted by a function f between mapObj cat1 = t1 and mapObj cat2 = t2 and, for any objects a and b, a function between mapMor cat1 a b = po1 a b and mapMor cat2 a b = po2 a b; since in these categories there is at most one morphism between any two objects a and b, the latter function can be interpreted by saying that if there is a morphism a -> b, there must exists a morphism f a -> f b. Translating this in preorder terms, this amounts to saying that a <= b in po1 implies f a <= f b in po2. This shows that functors between preorder categories are nothing else than order preserving functions! Let’s show in Idris that any order preserving function can be seen as a functor:

record MonotoneMap
  (t1 : Type)
  (po1 : t1 -> t1 -> Type)
  (t2 : Type)
  (po2 : t2 -> t2 -> Type)
where
  constructor MkMonotoneMap
  func : t1 -> t2
  funcRespOrd : (a, b : t1) -> po1 a b -> po2 (func a) (func b)
  
monotoneMapToFunctor :
     (UniquePreorder t1 po1, UniquePreorder t2 po2)
  => MonotoneMap t1 po1 t2 po2
  > CFunctor (preorderAsCategory {t = t1} {po = po1})          
            (preorderAsCategory {t = t2} {po = po2})
monotoneMapToFunctor
  {t1}
  {po1}
  {t2}
  {po2}
  (MkMonotoneMap fun fRespectsOrd) =
MkCFunctor
  fun
  fRespectsOrd
  (\a => unique (fun a)
                (fun a)
                (fRespectsOrd a a (reflexive a))
                (reflexive (fun a)))
  (\a, b, c, f, g =>
    unique (fun a)
           (fun c)
           (fRespectsOrd a c (transitive a b c f g))
           (transitive (fun a)
                       (fun b)
                       (fun c)
                       (fRespectsOrd a b f)
                       (fRespectsOrd b c g)))

Recall that reflexive and transitive are the functions associated with the Preorder interface, while unique comes from the UniquePreorder interface we introduced in our last post.

Notice also how the preservation of the identity morphisms and of composition follow directly from the fact that there is at most one morphism between two objects. To prove that two morphisms are equal it is then enough to observe that they have the same origin and the same target.

Conclusion

Functors are our precise way of defining a change of context where information is preserved. Whenever in your mind you make a nice connection between two different worlds, and there is some kind of preservation of structure, it is really probable that you could express your thought formally in terms of categories and functors!

In our last post we introduced three classes of categories, respectively discrete categories and categories associated to monoids and to preorders. Today we observed that functors between such categories are exactly structure preserving morphisms between those objects. In the case of monoids, the operational structure is preserved; in preorders, functors are order preserving morphisms; in discrete categories, there’s no structure to preserve, so any function is fine!

If you know a bit of functional programming and have been playing around with Haskell or Idris, you will probably know that there is already a concept of Functor defined in the language. How does it relate with what we defined today? That’s exactly the question we will tackle in our next post!

Fun with functors was originally published in Statebox on Medium, where people are continuing the conversation by highlighting and responding to this story.