If you’re a seasoned functional programmer in Haskell, OCaml, Rust, or Scala, chances are you’ve worked with Algebraic Data Types (ADTs) before. But if you’re new to the world of ADTs and looking for a beginner-friendly introduction to Simplicity, this post (and series) is for you!
This post is the first in a series that covers the foundational concepts of values and types, and the next will be about functions, expressions, and combinators.
But before getting too deep into this, we should first define what values, types, and expressions are. To understand this concept better, let’s consider a simple mathematical expression.
(2 > 1) = True
For our purposes, the Boolean expression (2 > 1) results in the Boolean value True. The Boolean type represents a binary choice where an expression can evaluate to either True or False. These two values make up the entire set of possible values within the Boolean type. Sometimes, expressions that evaluate to a Boolean value are referred to as propositions, which is a term from the field of logic. However, we won't explore that term further here.
A type represents a set of possible values with defined characteristics. Types enable us to reason about values in a structured manner. Unlike most programming languages where expressions represent values of a certain type, in Simplicity, expressions represent functions that map values from a source type to a target type. When evaluated, these expressions produce a result by transforming the input value. And a value is a concrete piece of data of a specific type.
name := expression : source type → target type
Translating logic into code requires the developer to consider implementation details, such as control flow, error handling, and efficiency. Mishandling any of these aspects can lead to the introduction of bugs in the codebase. Languages like Haskell, Coq, and Agda are designed specifically to express mathematical concepts and computations, resulting in code that more closely aligns with underlying mathematics, leading to fewer bugs than your typical programming languages. Mathematical languages excel in two key areas: (1) writing code for mathematical computations and (2) formal reasoning. Both of which are highly valuable in the context of programmable money, and are in line with the core principles that underpin the design of Simplicity.
Simplicity is a smart contracting language, similar in spirit to Bitcoin Script or EVM. Like Hacspec (or TLA+, or Alloy), Simplicity is also a specification language, meaning its semantics have a precise mathematical model that allows formally proving statements about programs. If the contract is written in Simplicity, you can prove correctness properties directly. For instance, you can prove that the coins cannot move without signature X, or that the program cannot exceed Y memory threshold.
Types in Simplicity come in three basic forms:
- A unit type defines exactly one possible value. Of type 1 (or alternatively ONE)
- A product type composes a pair of types using an “and” operation. A × B
- A sum type combines two types in an “or” operation. A + B
Simplicity's type system consists entirely of the unit type, sum types, and product types. All types in Simplicity are combinations from these three low-level type operations.
There are also many types that can be derived from these foundational types, which we will explore further in this post.
- The bit type is the sum of two unit types. 2 (or alternatively TWO)
- An option type is the sum of a unit type and a second arbitrary type. 1 + A
- A word type is the repeated product of the bit type. 2ⁿ
But let’s start at the beginning.
In the beginning, there was nothing. And from nothing, the concept of the unit type emerged!
Unit Type (1, Empty)
The unit type has exactly one value, confusingly also called “unit”. Beautiful! But what does this mean?
The unit type is written as 1, or ONE.
The unit value is written as (). We may write () : 1 to indicate that () is of type 1.
The unit type is a special type, an empty tuple, because it carries no information. It is often referred to as “empty” because it contains a single value. There is no way to encode any information because you have no choice in the value; there is only one. The entropy is zero. You might wonder, what’s the purpose of a type that has no distinguishable elements?
Despite its apparent emptiness, the unit type enables the composition of more complex types in Simplicity, allowing us to build up larger concepts.
Sum Type (Tagged Union)
Given two types, the sum of those types contains values that wrap either a value of the left type or a value of the right type. We write these choices as:
left(a) : A + B where value a : of type A
right(b) : A + B where value b : of type B
A sum type is the set of all values that wrap either a value of type A or a value of type B. By summing the pair together, we create a new type that can hold values of either A or B type. Fundamentally, the sum type forces you to choose between left and right. If you want to have both at the same time, you can use the product type, which we cover later in this post.
The unit type represents a lack of information, whereas the sum type carries information by representing choices or combinations of values of their constituent types. The sum type includes a label or tag that identifies the specific type of the value, enabling the distinction between different possibilities. Even when the two values of a pair are identical, as with left(a) and right(a) of A + A type, the fact that they are wrapped with different labels (left and right) is significant.
The Either type in Haskell is a sum type, and allows us to represent a choice between two alternative types. The Result type in Rust is also a sum type, which ensures that code handles both success and error cases. The sum type in Simplicity is the same concept that encompasses the idea of combining multiple options into one.
With the ability to sum, the concept of a bit naturally emerges.
Bit Type (2, Boolean Type)
The bit type is the sum of two unit types.
Bit, defined by Bit := 1 + 1, 2, or TWO.
0 := left(()) : Bit
1 := right(()) : Bit
The bit type is a fundamental type that represents a binary choice. It can have one of two distinct values, 0 or 1. In a sum type, the values correspond to either of the two child types and are accompanied by a label indicating which one it is. In the case of the bit type, the child types are both units and do not provide any additional information. The left and right labels carry the actual bit, providing the new information.
Boolean type (as found in languages like Python, Java, and C++) is just a bit type with a different name that also defines a choice between two values: True and False.
Boolean, written as Boolean := 1 + 1, 2, or TWO.
false := left(()) : Boolean
true := right(()) : Boolean
In Simplicity, these types are both 2. Because they are structurally equal, they are actually the same type. If instead of summing two unit types, we sum a single unit type with a second arbitrary type, we get the option type.
Option Type (Nullable, Maybe)
An option type is the sum of a unit type and any other arbitrary type.
Option[A] := 1 + A or A?
An option type, also known as a nullable or maybe type, encapsulates two possibilities: either the absence of a value (represented by the 1 unit type) or the presence of a value (represented by the other type A).
In Haskell, this is called Maybe; in Rust it is called Option. Both are examples of this type. The type allows for handling situations where a value may or may not be present. It provides a way to explicitly handle and express the absence of a value.
Product Type (Tuple)
Given two types A and B, the product type of A and B contains values that wrap a value from A and a value from B in a pair.
Products, written as (a, b) : A × B, where (a,b) is a pair of values of A × B type.
A product type represents a set of pairs of values with one of type A and one of type B. In a product type, any value of type A may be paired with any value of type B, resulting in |A| * |B| possible combinations of values.
This pair can be visualized as an “AND” operation, since it combines two values into a single entity. It’s referred to as the product type because its number of values is the product of the number of values in A and the number of values in B. We wrap values from the left and right type in the same product value, which is different from the sum type where we had to decide between the left or the right type. The product type is powerful because it provides a way to express compound values and enables us to build hierarchical structures and compose larger data models.
Another term for a product type is a tuple. Tuples are a common data structure and are supported by most programming languages. They allow us to define and return multiple values, and conveniently represent related data or key-value pairs.
In Simplicity, a point can be defined using a product type. Let’s say that we have an Int type, and we want to represent a point in two-dimensional space with x and y coordinates:
Point := Int × Int
This defines a type called Point that represents a pair of integer values.
We can then create an instance of a point by providing values for x and y:
p := (3, 5) : Point
To represent a line, we can define a product type that consists of two points, representing the start and end points of the line.
Line := Point × Point
But we’re jumping a bit ahead by assuming the use of integers. The problem with this example is that Simplicity does not have a built-in integer type that can represent arbitrarily large numbers like integers in some other languages such as Common Lisp or Python. In Simplicity, we have to work with fixed-size types.
For a fun example of this limitation, readers might recall that in the game “The Legend of Zelda,” Link’s maximum coin count was limited to 255, because the coins were stored as an 8-bit integer. This means that the coin count could only range from 0 to 255, the maximum value that can be represented by an 8-bit integer.
So, how do we approach the concept of bit size in Simplicity?
Word Types (Fixed-Width Integers, Characters)
A word type is constructed by combining multiple instances of bits in a product. The bit width refers to the number of bits that are combined. It determines the size of binary data, such as integers or words, and establishes the range of values that can be expressed.
For example:
2¹ := 2, represents a 1-bit integer, which is simply the bit type.
2² := 2¹ × 2¹, represents the product of two bit types, or a 2-bit word.
2⁴ := 2² × 2², represents the product of two 2-bit types, or to a 4-bit word.
2⁸ := 2⁴ × 2⁴, represents the product of two 4-bit types, or to a 8-bit word.
And so on, with increasing bit widths.
A 4-bit word is any of 16 possible combinations of four 0s or 1s. The 4-bit word type can be used to represent numbers from 0000 to 1111 in binary notation. However, binary values can quickly become lengthy and hard to read, especially for larger numbers. Hexadecimal condenses four binary digits into one, making it easier to represent numbers.
HexDigit := 2⁴
B := 1011 : HexDigit
Or we can define a Char using ASCII encoding:
Char := 2⁸
‘k’ := 0110 1011 : Char
We can define a 8-bit word as an Int:
Int8 := 2⁸
And we can use an 8-bit Int, to implement RGB colors:
RGB := ((Int8, Int8), Int8) : (2⁸ × 2⁸) × 2⁸
Each Int8 in RGB, represents the red, green, and blue components of the color, and each component can take any value from 0 to 255 (2⁸ - 1) to represent the intensity of that color channel.
To create an instance of an RGB color, we can provide specific values for each component:
BitcoinOrange := ((255, 153), 0) : RGB
Finite Types
The notation used for types in Simplicity not only represents the structure of a type but also provides insights into the number of distinct values possible. For instance, the type 2 + 2⁴, has a total of 18 different values.
In Simplicity all types are finite. This means that certain types, such as an infinite list defined as List := Item + (Item × List), are not possible. Infinite or recursive types introduce challenges in terms of termination, resource management, and reasoning about program behavior.
By restricting types to be finite, Simplicity can provide stronger guarantees about program behavior, ensure termination, and enable rigorous analysis and verification of code. Finite types are more than sufficient for cryptographic protocols. Additionally, things like STARKs and SNARKs (even roll-ups) have the ability to condense extensive computations into cryptographic analysis on data from relatively small finite types.
Simplicity Resources
If you’re eager to delve deeper into Simplicity, the primary technical documentation on the language can be found in the whitepaper and the Core Language Overview on the Simplicity Wiki. However, these resources may prove somewhat challenging for non-functional programmers, so we've started a general Simplicity thread on the Build On L2 community. Feel free to ask us any questions there.
My goal with these examples is to bridge that gap and offer a more accessible explanation of these concepts. Simplicity as a mathematically-inspired language, could bring us into a world of fully programmable money, with formally verified smart contracts. By grokking the core types in Simplicity, we can establish a solid foundation for exploring functions, expressions, and combinators in the upcoming installment of this series.