Simple algebraic data types

This is the sixth article from the series "Theory of Categories for Programmers." Previous articles have already been published on Habré:
0. Category Theory for Programmers: Preface
1. Category: essence of composition
2. Types and functions
3. Categories, large and small
4. Categories Claisley
5. Works and Copies

In the previous article the basic operations on types were considered: product and coproduct. We now show that combining these mechanisms allows us to construct many of the everyday data structures. Such a construction has significant applied value. For example, if we are able to check basic data types for equality, and also know how to reduce the equality of work and coproduct to equality of components, then the equality operators for composite types can be inferred automatically. In Haskell, for an extensive subset of complex types, the equality and comparison operators, conversion to and from the string, and many other operations are automatically output.

Let us take a closer look at the place of creation and type creation in programming.
')

Type product

The canonical implementation of a work of types in programming languages ​​is a pair. In Haskell, a pair is a primitive type constructor, and in C ++ it is a relatively complex template from the standard library.

Strictly speaking, a product of types is not commutative: it is impossible to substitute a pair of type (Int, Bool) instead of (Bool, Int) , although they contain the same data. However, the product is commutative up to an isomorphism defined by the swap function, which is inverse to itself:

 swap :: (a, b) -> (b, a) swap (x, y) = (y, x) 

Couples can be viewed as different storage formats for the same information, like big endian and little endian.

By investing one pair into another, you can combine as many types as you like into your work. The same can be obtained more easily if you notice that nested pairs are equivalent to tuples. This is a consequence of the fact that different orders of imbedding of pairs are isomorphic to each other. There are two possible combining order in the product of the three types a , b and c (in a given sequence). Namely,

 ((a, b), c) 

or

 (a, (b, c)) 

These types are different in the sense that a function that expects an argument of the first type cannot pass the argument of the second, but the values ​​of the types are in one-to-one correspondence. Here is the function that sets this display in one direction:

 alpha :: ((a, b), c) -> (a, (b, c)) alpha ((x, y), z) = (x, (y, z)) 

But back to her:

 alpha_inv :: (a, (b, c)) -> ((a, b), c) alpha_inv (x, (y, z)) = ((x, y), z) 

So, there is an isomorphism of types; these are just different ways of repacking the same data.

Considering the product of types as a binary operation, we see that the isomorphism above is very similar to the associative law in monoids:

 (a * b) * c = a * (b * c) 

The only difference is that in a monoid both products are absolutely identical, and for types they are equal up to isomorphism.

If we consider this distinction unimportant, then we can extend the analogy with monoids further and show that Singleton () is a neutral element with respect to the multiplication of types, just as 1 is neutral with respect to the multiplication of numbers. Indeed, attaching () to an element of type a does not add any information. Type of

 (a, ()) 

isomorphic to a , where isomorphism is given by functions

 rho :: (a, ()) -> a rho (x, ()) = x 

 rho_inv :: a -> (a, ()) rho_inv x = (x, ()) 

Our observations can be formalized as a statement that the category of the set Set is monoidal , that is, a category that is also a monoid with respect to the multiplication of objects (in this case with respect to the Cartesian product). A strict definition will be given below.

Haskell has a more general way of defining works, especially convenient, as we will soon see when they are combined with type sums. We use named constructors with several arguments. For example, an alternative definition of a pair looks like this:

 data Pair ab = P ab 

Here, Pair ab is the name of the type constructor, parametrized by two other types, a and b , and P is the name of the data constructor. We define a specific type, passing two types to the Pair type constructor, and create a pair of this type, passing the appropriately typed values ​​to the P constructor. For example, we define the variable stmt as a pair from String and Bool :

 stmt :: Pair String Bool stmt = P "This statement is" False 

The first line is a type declaration. It consists of the Pair type constructor with String and Bool instead of a and b . The second line defines the value of a variable, obtained by applying the data constructor P to a specific line and a logical value. Once again: type constructors are used to construct types, data constructors are used to construct values.

Since the namespaces of the types and data in Haskell do not overlap, often the same name is used for both constructors. For example,

 data Pair ab = Pair ab 

If you look at the built-in type of a pair with Lenin's squint, then it is recognized that it is in fact a variation on the topic of the last declaration, only the Pair constructor is replaced with a binary operator (,) . You can use (,) in the same way as any other named constructor, in prefix notation:

 stmt = (,) "This statement is" False 

Similarly, (,,) constructs triples, etc.

Instead of using generic pairs or tuples, you can enter a separate name for the product of specific types. For example,

 data Stmt = Stmt String Bool 

is a product of String and Bool , but has its own name and constructor. The advantage of this definition is that you can create many types with the same content, but with different semantics and functionality that the type system will not allow to mix with each other.

Programming on tuples and multi-argument constructors often leads to confusion and errors, because you have to keep track of which component is responsible for what. It would be better to be able to give the components proper names. The product of types with named fields is called a Haskell entry and a struct in C.

Records

Consider a simple example. We will describe the chemical elements of a single structure consisting of two lines (Latin name and symbol) and an integer corresponding to the atomic mass. To do this, you can use a tuple (String, String, Int) and keep in mind what component is responsible for what. To extract components from a tuple, we will apply pattern matching. The following function checks whether the character of a chemical element is a prefix of its Latin name (for example, He is the Helium prefix):

 startsWithSymbol :: (String, String, Int) -> Bool startsWithSymbol (name, symbol, _) = isPrefixOf symbol name 

In such code, it is easy to make a mistake, it is difficult to read and maintain. Much better to define instead of a tuple entry:

 data Element = Element { name :: String , symbol :: String , atomicNumber :: Int } 

These representations are isomorphic, as can be seen with the help of the following reciprocal transformations:

 tupleToElem :: (String, String, Int) -> Element tupleToElem (n, s, a) = Element { name = n , symbol = s , atomicNumber = a } 

 elemToTuple :: Element -> (String, String, Int) elemToTuple e = (name e, symbol e, atomicNumber e) 

Note that the field names of the record are simultaneously accessor functions. For example, atomicNumber e returns the atomicNumber field of the atomicNumber record. Thus, the atomicNumber function has the type:

 atomicNumber :: Element -> Int 

Using Element type entries, the startsWithSymbol function becomes more readable:

 startsWithSymbol :: Element -> Bool startsWithSymbol e = isPrefixOf (symbol e) (name e) 

In Haskell, you can crank a trick that turns the isPrefixOf function into an infix operator, framing it with reverse apostrophes. This makes the code more readable:

 startsWithSymbol e = symbol e `isPrefixOf` name e 

We were able to omit the brackets due to the fact that the priority of the infix operator is lower than the priority of the function call.

Sum of Types

In the same way that a product in the category of sets induces the products of types, coproduction produces sums of types. The canonical implementation of the sum of types in Haskell is:

 data Either ab = Left a | Right b 

Like pairs, Either commutative (up to isomorphism) can be nested, and the order of nesting is not important (up to isomorphism). For example, the sum of three types looks like this:

 data OneOfThree abc = Sinistral a | Medial b | Dextral c 

It turns out that Set forms a (symmetric) monoidal category with respect to the coproduct operation. The binary operation takes the disjoint sum, and the neutral element is the initial object. In terms of types, Either is a monoidal operation, and an uninhabited Void type is its neutral element. Consider that Either is addition, and Void is zero. Indeed, adding Void to the sum of types does not change the set of values ​​of the type. For example,

 Either a Void 

isomorphic to a . Indeed, since the Void type is not populated, there is no way to construct the Right value. Hence, the only inhabitants of Either a Void are Left values, which are simply a wrapper over a value of type a . Symbolically, this can be written as a + 0 = a .

Sums of types are very common in Haskell. In C ++, their analogs (combinations or variants) are used much less frequently for a number of reasons.

First, the simplest sums of types are enums that are implemented in C ++ using enum . By equivalent

 data Color = Red | Green | Blue 

in C ++ will

 enum { Red, Green, Blue }; 

An even simpler sum of types.

 data Bool = True | False 

in C ++ it is a primitive type bool .

Further, the sums of types encoding the presence or absence of a value are implemented in C ++ using various tricks with "impossible" values, such as empty strings, negative numbers, null pointers, etc. In Haskell, the explicit, intentional optional values ​​are written using Maybe :

 data Maybe a = Nothing | Just a 

The type of Maybe is the sum of two types. Mentally turn its designers into separate types. The first will take the form:

 data NothingType = Nothing 

This is an enumeration with a single value of Nothing . In other words, it is a singleton equivalent to a type () . The second part of

 data JustType a = Just a 

is a wrapper over type a . We could write Maybe as

 data Maybe a = Either () a 

More complex sums of types are fabricated in C ++ using pointers. A pointer can either be null or point to a value of a particular type. For example, in Haskell the list is defined as a (recursive) sum of types:

 List a = Nil | Cons a (List a) 

In C ++, the same type is written as:

 template<class A> class List { Node<A> * _head; public: List() : _head(nullptr) {} // Nil List(A a, List<A> l) // Cons : _head(new Node<A>(a, l)) {} }; 

The null pointer here encodes an empty list.

Note that the Haskell Nil and Cons constructors have turned into two overloaded constructors of the List class with similar arguments: no arguments in the Nil case, a value and a list for Cons . The List class does not need a label that would distinguish the components of the sum of types; instead, it uses the special value nullptr for _head to represent Nil .

An important distinction between types in Haskell and in C ++ is that Haskell has data structures that are immutable. If an object was created using a specific constructor, it will remember forever which constructor was used with which arguments. So an instance of the class Maybe , created as Just "energy" , will never turn into Nothing . Similarly, an empty list will always remain empty, and a three-element list will always store the same three elements.

Immunity makes constructors reversible: an object can always be disassembled into its component parts used in its creation. Such deconstruction is carried out by comparison with a sample, which is a particular designer. Constructor arguments are replaced with variable names (or other patterns).

The List type has two constructors, so the deconstruction of an arbitrary List consists of two corresponding pattern matching. The first sample matches the empty Nil list, the second one with the list created with Cons . For example, we define a simple function:

 maybeTail :: List a -> Maybe (List a) maybeTail Nil = Nothing maybeTail (Cons _ t) = Just t 

The first part of the maybeTail definition uses the Nil constructor as a pattern for matching and returns Nothing . The second part uses the Cons constructor as a sample. The first argument of the sample is represented by a dash, since we are not interested in the value contained in it. The second argument, Cons associated with the variable t (hereinafter, we will talk about variables, although, strictly speaking, they are unchanged: the variable that is once associated with the value never changes). The value of the function on this sample is Just t . So, depending on how the value of the List type is created, it will coincide with one of the samples. If it was created with Cons , the function will get both arguments used (the first of which will be ignored).

More complex sums of types are implemented in C ++ by a hierarchy of polymorphic classes. A family of classes with a common ancestor can be interpreted as a sum of types in which the table of virtual functions serves as an implicit label of the component. What Haskell serves as pattern matching is implemented in C ++ by calling the dispatch function.

The reader is rarely seen in C ++ using union as a sum of types due to its excessive limitations. You can't even put std::string in a union , because this class has a copy constructor.

Type algebra

Separately, the product and the sum of the types allow you to define many useful data structures, but the real power comes from their combination.

Let's summarize the above. We considered two commutative monoidal structures underlying the type system. These are the sum of types with a neutral element Void and the product of types with a neutral element () . It is convenient to imagine them as addition and multiplication. In this case, Void zero, and () is one.

Let's see how far this analogy goes. For example, is it true that multiplying by zero gives zero? In other words, is any product isomorphic to a Void type Void ?

Are there pairs of, say, Int and Void ? To create a pair, both values ​​are needed. The value of the Int type is not a problem, but there is a catch with Void : this type is not populated (there is not a single value of this type). Thus, for any type a type (a, Void) also not populated and, therefore, equivalent to Void . In other words, a*0 = 0 .

Addition and multiplication of numbers are connected by the distribution law:

 a * (b + c) = a * b + a * c 

Is it for sum and product types? Yes, up to isomorphism. The left part of the identity corresponds to the type

 (a, Either bc) 

and right -

 Either (a, b) (a, c) 

Let's present functions which will transform types there and back:

 prodToSum :: (a, Either bc) -> Either (a, b) (a, c) prodToSum (x, e) = case e of Left y -> Left (x, y) Right z -> Right (x, z) 

 sumToProd :: Either (a, b) (a, c) -> (a, Either bc) sumToProd e = case e of Left (x, y) -> (x, Left y) Right (x, z) -> (x, Right z) 

The case of construction is used for pattern matching within a function. The arrow separates the sample and its corresponding expression. For example, when calling prodToSum with an argument

 prod1 :: (Int, Either String Float) prod1 = (2, Left "Hi!") 

the variable e in case e of will be equal Left "Hi!" . It will match the Left y pattern, substituting "Hi!" instead of y . Since the variable x previously associated with 2 , the result of the case of construction (and the entire function) will be, as expected, Left (2, "Hi!") .

The proof that the functions above are mutually inverse will be left to the reader as an exercise. They only repack the same data from one format to another.

Two monoids connected by distributive law are called semi-rings in mathematics. This is not a complete ring , since we cannot determine the subtraction of types. The set of statements true for the generators of the semiring of natural numbers can be transferred to types. Here are some examples:

Numbers	Types
0	Void
one	()
a + b	Either ab = Left a | Right b
a * b	(a, b) or Pair ab = Pair ab
2 = 1 + 1	data Bool = True | False
1 + a	data Maybe = Nothing | Just a

The list type is of particular interest because it is defined as a solution to the equation. The type defined is found on both sides of the equality:

 List a = Nil | Cons a (List a) 

Making the usual substitutions and replacing List a with x , we get

 x = 1 + a * x 

This equation cannot be solved by traditional algebraic methods, since types cannot be subtracted or divided. Let us recursively substitute the expression (1 + a*x) instead of x on the right and expand the brackets by distributivity. Will get

 x = 1 + a*x x = 1 + a*(1 + a*x) = 1 + a + a*a*x x = 1 + a + a*a*(1 + a*x) = 1 + a + a*a + a*a*a*x ... x = 1 + a + a*a + a*a*a + a*a*a*a... 

In the end, we come to an infinite sum of products (tuples), which can be interpreted as follows: the list is either empty, 1 ; either consists of a single element, a ; either consists of a pair, a*a ; either from a triplet, a*a*a , and so on. The formal definition obtained fully corresponds to the intuitive notion of the list as a line, where instead of letters are values ​​of type a .

We will return to lists and other recursive structures further, after studying functors and fixed points.

Solving equations with symbolic variables is an algebra! Therefore, these data types are called algebraic (ADT).

Summing up, we give one very important interpretation of type algebra. Note that the product of types a and b must contain both a value of type a and a value of type b , which implies a population of both types. On the other hand, the sum of types contains either a value of type a , or a value of type b , so it is enough that at least one of them is populated. The logical operations of conjunction and disjunction form a semiring, which is in accordance with the following type algebra:

Logics	Types
false	Void
true	()
a || b	Either ab = Left a | Right b
a && b	(a, b)

This analogy can be deepened and is the basis of the Curry-Howard isomorphism between logic and type theory. We will return to this issue when considering functional types.

Exercises

1. Show that Maybe a and Either () a is isomorphic.
   
2. Consider the following sum of types in Haskell:
   

    data Shape = Circle Float | Rect Float Float 

   
   To define the area function on the Shape type, we use the pattern matching:
   

    area :: Shape -> Float area (Circle r) = pi * r * r area (Rect dh) = d * h 

   
   Implement Shape in C ++ or Java as an interface and create two classes: Circle and Rect . Then write the area as a virtual function.
   
3. (Continued) It’s easy to add a new circ function that calculates the perimeter of a Shape . In Haskell, the definition of the Shape type will remain unchanged; The following code can be added anywhere in the program:
   

    circ :: Shape -> Float circ (Circle r) = 2.0 * pi * r circ (Rect dh) = 2.0 * (d + h) 

   
   Add circ to your C ++ or Java program. What parts of the original program had to be modified?
   
4. (Continued) Add a new Shape Square Shape type and make the appropriate updates to the rest of the code. What had to change in Haskell? What about C ++ or Java? (Even if you don't know Haskell, the changes should be pretty obvious.)
   
5. Show that the formal identity a + a = 2 * a holds for types (up to isomorphism). Recall that 2 in the type language corresponds to Bool (see the table above).
   

Thanks

The author is grateful to Gershom Bazerman for reviewing the post and helpful comments.