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 typesi64
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 }
Conclusion
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.
Most Recent Articles
- From State Machine to Stateless Microservice
- Entangled ways of product development in the area of cybersecurity #3 - LogMan.io
- Entangled ways of product development in the area of cybersecurity #2 - BitSwan
- Entangled ways of product development in the area of cybersecurity #1 - Asynchronous or parallel?
- State machine miracle
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.
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.
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.
Published on September 27, 2016