SP-Lang: Category theory in the wild

Our techonology uses a stream processing language called SP-Lang. SP-Lang is aimed at people who don’t program, with a comparable simplicity to, e.g. spreadsheet macros or SQL. SP-Lang tries to do as much heavy lifting transparently for the user as possible.

On the other side, SP-Lang is compiled down to the machine code of the CPU for the best possible performance.

We recently encountered several interesting problems that demonstrate how seemingly abstract category theory finds its practical applications and helps us solve these problems sustainably.

Dictionary and type inference

The dictionary (or a map) is a type that composes two types into a pair. There is a type of key Tk, and a type of value Tv. These two types are composed into a dictionary type of {Tk:Tv}.

Our goal is to avoid explicit type specifications as much as possible because our users don't understand the concept of types. It means that we need to infer types from clues in the code.
It represents a challenge for a dictionary because you can have various types of different values and keys in the dictionary.

Note: A similar issue is found in the list type, which is the other container type.

Practically, this problem is illustrated in following example:

    "Key1": "Hello!",
    "Key2": 123

What is the type of this dictionary? The first value is a string "Hello!" and the second is an integer 123.

Let's try to write a type signature for it:

{ str : ( str + si64 ) }
  • str is for a string type
  • si64 is for an integer type (Signed Integer 64bit)

The type ( str + si64 ) is a so-called "sum type", using the terminology of the category theory. You declare that the value can be of a string type PLUS an integer type. We added one type to another using a logic operator of + (PLUS). The "sum type" is an algebraic type for this reason. It allows adding (PLUS or SUM) one type to another.

Note: An algebraic operator of + (PLUS) is equivalent to | (OR) in this context. The alternative name of the "sum type" is "COPRODUCT".

Type inference can construct this sum type from the type clues in the code itself.

Type any

There is a particular type in SP-Lang: any. This type is a sum of all possible types in SP-Lang.

We can extend the above example:

{ str : any }

And the type signature is valid.

The any type is a fundamental building block for sum types, and it is very powerful. However, there is a downside to this: it is less efficient than using scalar types because there is a particular overhead in a runtime of a compiled SP-Lang.

Tuples with None items

Another problem we encounter is that people want to use tuples as dictionary keys (that's ok), but some of the tuple members could be None.

It looks like this:

    ("One", 1): "Foo",
    ("Two", None): "Bar",

Please notice None in the second key of the dictionary.

Naively, you would type this dictionary as:

{ ( str, si64 ) : str }

... but this doesn't allow None in the tuple.
So the sum type has to come to help us again:

{ ( str, ( si64 + None ) ) : str }

... and yes, None is a type. We state that the second member of a tuple can be either an integer PLUS (OR) None.

For the sake of completeness, any type can be employed here as well:

{ ( str, any ) : str }


SP-Lang has a wide spread of goals: very high performance on one side the ease of use for language users on the other side. It represents a lot of work that SP-Lang has to do instead of the user. In these specific cases, it is about the SP-Lang approach to types. SP-Lang is designed to avoid explicit type specifications. It provides a similar feeling to the user as Python or SQL regarding types. Users can simply avoid them completely, so they have one less thing to worry about. On the other hand, because the SP-Lang is compiled into the machine code, types have to be explicitly known during compilation. Figuring types in runtime slows the execution a lot (see Python).

To solve this, SP-Lang is using type inference. It is a powerful technique that uses clues provided by the user in the code to infer types automatically. The type inference feels a bit magical, and for sure, it is a complex algorithm. The tricky part is how to make it right. "Right" means sustainable in this context. We want to build more language features on top of it.

And this is where category theory, algebraic types, and particularly sum type helped us. It provides proof that we correctly analyze and solve practical problems that we meet in the wild.

About the Author

Ales Teska

TeskaLabs’ founder and CEO, Ales Teska, is a driven innovator who proactively builds things and comes up with solutions to solve practical IT problems.

You Might Be Interested in Reading These Articles

SeaCat Mobile Secure Gateways' Performance Test

We decided to perform this test to validate our architectural, design and implementation decisions in regards to SeaCat performance. Our goal was to build the best-in-class product using the most advanced techniques to deliver highest possible throughput yet not compromising the security of the communication. Results of the test have been fed back into our development team to improve further overall performance characteristics of the solution.

Continue reading ...


Published on July 21, 2014

SeaCat trial for iOS on Mac OSX

This blog entry is meant to help you to start using SeaCat component on your Xcode iOS development environment. It contains instructions how to install and configure SeaCat gateway and how to integrate SeaCat client into your iOS application. SeaCat gateway is a secure gate to the restricted network. It allows access only to selected HTTP hosts and prevents exposure of others. It also secures communication with SeaCat clients that are typically in the Internet. SeaCat client becomes part of said mobile application and provides secured channel to SeaCat gateway and to target hosts in the restricted network. It ensures mutual security of the connection and transferred data.

Continue reading ...

tech trial ios osx

Published on March 14, 2014

What Is Mobile Application Containerization or Wrapper, and Why It Needs to Go?

Containerization is an alternative for full machine virtualization. You probably know well-known containerization technology from Docker or Rocket. However, this article addresses the pros and cons of mobile “containerization” or wrapper used to isolate the mobile app from the mobile operating system or other applications installed on the same device. These type of “containerization” work in a different way.

Continue reading ...

tech security

Published on September 27, 2016