Type system in mathematics

From time to time I encounter questions in mathematics, which in some sense can be called "grammatically incorrect."

Example. "Interval $$$[0, 1]$ is closed or open? "
Example. "Does it $$$\ {1, 2, 3 \}$ group? "
Example. "What is the Fourier series for $$$\ sin x + \ sin \ pi x$ ?

More stupid examples.
')
Example. "Is the rectangle simple?"
Example. " $$$17 \ in 3$ ? "
Example. "What is the Fourier series for the empty set?"

All these examples are united by the fact that they are typing errors : these are attempts to apply a certain mathematical process to a mathematical object that can in no way be input data for it. If to answer these questions you try to write a program in some highly mathematical programming language, then it (I hope!) Will not compile.

Mathematical objects are usually not perceived explicitly as having types in the same sense as objects in programming languages ​​with a type system . It is assumed that ordinary mathematics should be formalized in the Zermelo – Fraenkel system (ZF), possibly with the axiom of choice, and in ZF each mathematical object is constructed as a set. In this sense, all these objects are of the same type. (In particular, the question " $$$17 \ in 3$ "It is quite logical in ZF! And this is one of the reasons why it’s worth not to love ZF as a basis for mathematics.) However, it seems to me that in practice mathematical objects are implicitly perceived as having types, and this way of thinking is learned by mathematics, but not often discussed.

Instead of reasoning from the point of view of set theory, it is worthwhile to consider mathematical objects as having types, which will allow us to import various useful concepts into mathematics, such as the concepts of type safety , type conversion , subtyping and overload , which will allow us to more specifically define “grammatical fallacy »Mathematical sentences. For the remainder of the post, I will relaxly discuss how these and other types of concepts apply to mathematics in general. The article will contain many categorical concepts, but for the sake of simplicity of understanding, I will limit myself to making them notes in brackets.

Informal description of mathematical types

Informally, it can be said that a type of mathematical object describes a kind of this object.

Example. An object $$$2$ has a type $$$\ texttt {Nat}$ (natural number).
Example. An object $$$-2$ has a type $$$\ texttt {int}$ (whole).
Example. An object $$$\ frac {1} {2}$ has a type $$$\ texttt {Rat}$ (rational number).
Example. An object $$$(2, 3)$ has a type $$$\ texttt {Nat} \ times \ texttt {Nat}$ (a pair of positive integers).
Example. An object $$$30 ^ {\ circ}$ has a type $$$\ texttt {deg}$ (degree).
Example. An object $$$x \ mapsto x ^ 2$ has a type $$$\ texttt {Nat} \ to \ texttt {Nat}$ (function is displayed from natural numbers to natural numbers).
Example. An object $$$\ texttt {true}$ has a type $$$\ texttt {Bool}$ ( Boolean ).

But less simple examples:

Example. An object $$$\ mathbb {Z}$ has a type $$$\ texttt {Grp}$ (Group).
Example. An object $$$S ^ 2$ has a type $$$\ texttt {Top}$ (topological space).
Example. An object $$$X \ mapsto H_1 (X)$ has a type $$$\ texttt {Top} \ to \ texttt {Grp}$ (the function is mapped from topological spaces to groups).

Types help us understand what actions we can perform with a set of mathematical objects.

Example. You can take two objects of type $$$\ texttt {Nat}$ and add or multiply them. In other words, there are functions $$$+, \ times: \ texttt {Nat} \ times \ texttt {Nat} \ to \ texttt {Nat}$ .
Example. You can take two objects of type $$$\ texttt {int}$ in addition to addition and multiplication subtract them. In other words, there are functions $$$+, \ times, -: \ texttt {Int} \ times \ texttt {Int} \ to \ texttt {Int}$ .
Example. You can take an object like $$$\ texttt {deg}$ and apply trigonometric functions to it. In other words, there are functions $$$\ texttt {sin}, \ texttt {cos}: \ texttt {Deg} \ to \ texttt {Real}$ .
Example. If a $$$\ texttt {A}, \ texttt {B}$ are types, then we can take an object of type $$$\ texttt {A}$ and another object of type $$$\ texttt {A} \ to \ texttt {B}$ to apply the latter to the first. In other words, there is a function $$$\ texttt {eval}: \ texttt {A} \ times (\ texttt {A} \ to \ texttt {B}) \ to \ texttt {B}$ .

Type of $$$\ texttt {Bool}$ occupies a special place in this theory. There are only two objects of this type, namely $$$\ texttt {true}$ and $$$\ texttt {false}$ , and functions, giving output values $$$\ text {Bool}$ , can be used to check if the property is true.

Example. You can take a natural number and ask if it is simple. In other words, there is a function $$$\ texttt {isPrime}: \ texttt {Nat} \ to \ texttt {Bool}$ .
Example. If a $$$\ texttt {A}$ is a type, then we can take two objects of type $$$\ texttt {A}$ and ask if they are equal. In other words, there is a function

$$

$$\ displaystyle \ texttt {isEqual}: \ texttt {A} \ times \ texttt {A} \ to \ texttt {Bool}$$

which we can also write using the equal sign $$$=$ .
Example. You can take two integers and ask whether the first is greater than or equal to the second. In other words, there is a function

$$

$$\ ge: \ texttt {Int} \ times \ texttt {Int} \ to \ texttt {Bool}$$

As follows from these examples, there are many ways to combine types to create new types; they are called type constructors .
Example. An object having a work type $$$\ texttt {A} \ times \ texttt {B}$ , is a pair of objects of type $$$\ texttt {A}$ and $$$\ texttt {B}$ .
Example. An object of type sum $$$\ texttt {A} + \ texttt {B}$ is or object of type $$$\ texttt {A}$ or object type $$$\ texttt {B}$ .
Example. Functional object $$$\ texttt {A} \ to \ texttt {B}$ , also sometimes written as $$$\ texttt {B} ^ {\ texttt {A}}$ Is a function that receives objects of type at the input $$$\ texttt {A}$ and returning objects of type on output $$$\ texttt {B}$ .

(These constructions may seem familiar to lovers of category theory: they all are just products, coproducts and exponentials. In other words, the categories of types are bidecarte closed categories.)

Using the above simple type constructors, we can create more complex type constructors. For example, having type $$$\ texttt {A}$ we can create a type list $$$\ texttt {[A]}$ which is the type of (finite) lists of elements of type $$$\ texttt {A}$ :

$$

$$\ displaystyle \ texttt {[A]} = \ texttt {1} + \ texttt {A} + \ texttt {A} \ times \ texttt {A} + \ texttt {A} \ times \ texttt {A} \ times \ texttt {A} + ...$$

(Where $$$\ texttt {1}$ - this is a special type called unit type ; its defining characteristic is that there is only one object of type-unit, which we will call a point ). Heuristic type-list can be written as a "geometric series" $$$\ frac {\ texttt {1}} {\ texttt {1} - \ texttt {A}}$ .

Notation system

Above we used the record $$$\ texttt {f}: \ texttt {A} \ to \ texttt {B}$ to indicate that $$$\ texttt {f}$ was an object of type $$$\ texttt {A} \ to \ texttt {B}$ . It would be logical to generalize this entry to arbitrary types so that $$$\ texttt {a}: \ texttt {A}$ meant that $$$a$ is an object of type $$$\ texttt {A}$ . This will be a type declaration .

Type safety and typing errors

In addition to helping us understand what we can do with a set of mathematical objects, types also help us understand what we cannot do. Let's look at the examples presented at the beginning of the post, taking into account this idea.

Example. "Does it $$$\ {1, 2, 3 \}$ group? "
Example. "What is the Fourier series for $$$\ sin x + \ sin \ pi x$ ?

Example. "Interval $$$[0, 1]$ is closed or open? "Functions $$$\ texttt {isClosed}$ and $$$\ texttt {isOpen}$ they cannot receive at the entrance a multitude or even a topographic space; they get in pairs $$$(X, S)$ where $$$X$ Is a topological space, and $$$S$ - subspace $$$X$ (and give out on output is whether $$$S$ closed or open subset $$$X$ ). In other words, they are of type not $$$\ texttt {Top} \ to \ texttt {Bool}$ and type $$$\ texttt {Pairs} \ to \ texttt {Bool}$ . Question is whether $$$[0, 1]$ open or closed, depends on whether it is considered as a subset of itself or, say, $$$\ mathbb {R}$ .

Example. "Does it $$$\ {1, 2, 3 \}$ group? "function $$$\ texttt {isGroup}$ does not get a lot at the entrance; she gets inlet couples $$$(X, \ cdot)$ where $$$X$ - this is a lot, but $$$\ cdot$ - binary operation on $$$X$ ( magma ). In other words, she has type not $$$\ texttt {Set} \ to \ texttt {Bool}$ and type $$$\ texttt {Magma} \ to \ texttt {Bool}$ .

Example. "What is the Fourier series for $$$\ sin x + \ sin \ pi x$ ? "Function $$$\ texttt {FourierSeries}$ does not receive the input function on $$$\ mathbb {R}$ ; it receives at the input a periodic function on $$$\ mathbb {R}$ for example with a period $$$2 \ pi$ or, similarly, the function on $$$\ sin x + \ sin \ pi x$ is not periodic with any period. In other words, $$$\ texttt {FourierSeries}$ has no type $$$(\ texttt {Real} \ to \ texttt {Complex}) \ to (\ texttt {Int} \ to \ texttt {Complex})$ and type $$$(\ texttt {Circle} \ to \ texttt {Complex}) \ to (\ texttt {Int} \ to \ texttt {Complex})$ .

More stupid examples can be analyzed similarly.

Finding typing errors, or type checking, helps in debugging mathematical calculations in the same way that a compiler looks for typing errors for debugging code. For example, when we see an expression in the form $$$a = b$ then before checking its truth, you can check whether it makes sense at all by making sure that $$$a$ and $$$b$ have one type. This is a very generalized version of dimension analysis .

Type checking is also a way of understanding new mathematical topics. If you still can not yet pronounce correctly typed sentences on the desired topic (which can be determined by other people who know the subject), then you have not yet figured out the types of basic objects or functions of this area. For example, if you say "fundamental group ...", then you need to end the sentence with either the phrase "point topological space" or "linearly connected topological space". Otherwise, you do not understand the important aspect of defining the fundamental group, namely the role of base points.

Type casting, subtype creation and overloading

Type checking for a nontrivial task can be done by the fact that most mathematical objects are naturally considered to be of several types. For example, the above we said that the number $$$2$ has a type $$$\ texttt {Nat}$ but it is also obvious that it has type $$$\ texttt {Int}, \ texttt {Rat}, \ texttt {Real}$ and even $$$\ texttt {Complex}$ . One way to describe this situation is in the cast functions .

$$

$$\ displaystyle \ texttt {Nat} \ to \ texttt {Int} \ to \ texttt {Rat} \ to \ texttt {Real} \ to \ texttt {Complex}$$

which transform objects into different types. If there is a cast operator $$$\ texttt {A} \ to \ texttt {B}$ , then we can use objects of type $$$\ texttt {A}$ as input to functions waiting for objects of type $$$\ texttt {B}$ if we first cast the type.

Another way to describe this situation is that some types are subtypes of other types; in other words, instead of a set of cast functions, the above situation describes a chain of inclusions of subtypes. The creation of subtypes allows objects to have several types at the same time, and not to be of a certain type at a certain point of any calculations.

Subtypes have an interesting relationship with functional types. If a $$$\ texttt {B} '$ is a subtype $$$\ texttt {B}$ then functional type $$$\ texttt {A} \ to \ texttt {B} '$ is a subtype $$$\ texttt {A} \ to \ texttt {B}$ , but if $$$\ texttt {A} '$ is a subtype $$$\ texttt {A}$ (a function that outputs objects of type $$$\ texttt {B} '$ , also produces output type $$$\ texttt {B}$ ), then the functional type $$$\ texttt {A} '\ to \ texttt {B}$ is not a subtype, but a supertype $$$\ texttt {A} \ to \ texttt {B}$ (a function that receives objects of the type $$$\ texttt {A}$ can also receive objects of type $$$\ texttt {A} '$ ). In other words, the creation of functional types is covariant in output types, but contravariant in input types with respect to subtypes.

(And this should also be familiar to lovers of category theory: this phenomenon reflects the fact that the creation of exponential objects is covariantly functorial in final objects, but contravariantly functorial in the original objects.)

The third way to describe this situation is that the functions in mathematics are overloaded , and this description is probably closest to mathematical practice. Overloading is the practice of defining functions that have the same name but receive different types of input data. For example, the addition symbol $$$+$ refers not to one, but to several functions that have the same name, i.e.

$$

$$+: \ texttt {Nat} \ times \ texttt {Nat} \ to \ texttt {Nat}$$

$$

$$+: \ texttt {Int} \ times \ texttt {Int} \ to \ texttt {Int}$$

$$

$$+: \ texttt {Rat} \ times \ texttt {Rat} \ to \ texttt {Rat}$$

$$

$$+: \ texttt {Real} \ times \ texttt {Real} \ to \ texttt {Real}$$

$$

$$+: \ texttt {Complex} \ times \ texttt {Complex} \ to \ texttt {Complex}$$

and so on. More generally we can use $$$+$ for the operation of addition on any ring, and even more generally for the operation of grouping in any Abelian group. We even used it above to designate types of sums!

With indicative record $$$a ^ b$ business is much worse. It can refer to functions of any of the following types:

$$

$$\ displaystyle \ texttt {Nat} \ times \ texttt {Nat} \ to \ texttt {Nat}$$

$$

$$\ displaystyle \ texttt {PosReal} \ times \ texttt {Real} \ to \ texttt {Real}$$

$$

$$\ displaystyle \ texttt {PosReal} \ times \ texttt {Complex} \ to \ texttt {Complex}$$

or even more generally, $$$a$ can be a member of a group, but $$$b$ may be whole or $$$a$ may be $$$e$ , but $$$b$ may be an element and we even used an indicative notation to denote functional types! See also this question in math.se.

It seems that overloading students is confusing, and I think part of the reason is that mathematicians rarely explicitly talk about it when they use it. Overloading is not so bad as long as all its different instances are at least logically connected with each other, but sometimes mathematical concepts are overloaded for no reason other than historical ones, for example, the words “normal” and “correct”. It confuses students even more: sometimes one word is used in two different contexts because of a logical connection, for example, “normal expansion” and “normal subgroups”, but sometimes it simply does not exist. See also this question on MO .

Recursive types

In type theory, some types can be defined recursively , relative to themselves, and not directly relative to other types. In this way, surprisingly many important types of mathematical objects can be defined.

Example. Type of $$$\ texttt {Nat}$ natural numbers can be recursively defined as

$$

$$\ texttt {Nat} = \ texttt {1} + \ texttt {Nat}$$

that is, a natural number is either a point (namely $$$1$ ), or another natural number (namely, its previous).

Example. More generally, type list $$$\ texttt {[A]}$ can be recursively defined as

$$

$$\ displaystyle \ texttt {[A]} = \ texttt {1} + \ texttt {A} \ times \ texttt {[A]}$$

that is, the list of elements of type $$$\ texttt {A}$ is either a point or an element of type $$$\ texttt {A}$ (namely the beginning of the list) along with the list of elements of the type $$$\ texttt {A}$ (i.e. the remaining part of the list). In particular, $$$\ texttt {Nat}$ - it's just a type $$$\ texttt {[1]}$ list of points. It is worth noting that this is exactly the ratio that must be satisfied by the "geometric series" $$$\ frac {\ texttt {1}} {\ texttt {1} - \ texttt {A}}$ .

Example. Type of $$$\ texttt {Tree}$ (fully binary) trees (with root) can be recursively defined as

$$

$$\ displaystyle \ texttt {Tree} = \ texttt {1} + \ texttt {Tree} \ times \ texttt {Tree}$$

that is, a tree is either a point or a pair of trees (namely, a pair of trees obtained by removing their root).

Example. Type variation $$$\ texttt {Set}$ sets can be recursively defined as

$$

$$\ displaystyle \ texttt {Set} = (\ texttt {Set} \ to \ texttt {Bool})$$

that is, a set is a set function that returns either true (for the elements contained in it) or false (for elements that are not in it).

Example. Type of $$$\ texttt {Game}$ (not necessarily finite) combinatorial games can be recursively defined as

$$

$$\ displaystyle \ texttt {Game} = (\ texttt {Game} \ to \ texttt {Bool}) \ times (\ texttt {Game} \ to \ texttt {Bool})$$

that is, a game is a pair of game functions that we can call $$$\ texttt {L}$ and $$$\ texttt {R}$ . Strictly speaking, the combinatorial game actually needs to be called the position of the game, since it describes a specific moment of the game (for example, the beginning of a game of chess), and not what we usually call a game (for example, chess). We perceive games as something in which two people play, left and right, and in any position of the game the left has possible options for the positions of the game into which he can move it, namely, such positions for which $$$\ texttt {L}$ returns true, and the right one also has some possible positions of the game to which it can move, namely, such positions for which $$$\ texttt {R}$ returns true.

Conway noted that combinatorial games resemble a generalization of both ordinal numbers (which can be described relative to the set of ordinal numbers) and Dedekind sections (which can be described by a pair of sets of rational numbers). He used this connection to determine a large class of numbers using games; see more in On Numbers and Games .

The type we defined earlier $$$\ texttt {Set} = (\ texttt {Set} \ to \ texttt {Bool})$ , can also be perceived as a type of impartial games , that is, games in which possible moves do not depend on which player is playing.

(For lovers of category theory: recursive types are initial algebras with respect to the corresponding endofunctor of the category of types.)

Functions that receive a recursive type as an input can also be defined recursively. Examples with natural numbers should already be familiar to you; Here are some other examples.

Example. The length of the list can be defined recursively as follows: dot length is $$$0$ . If the list is not a point, then it consists of an element and a sublist, and then the list length is one more than the length of the sublist. (I could write it with pseudocode, but I don’t know a clear way to display pseudo code on a WordPress site.)

Example. More generally, for any two types $$$\ texttt {A}, \ texttt {B}$ there is a function

$$

$$\ texttt {map}: (\ texttt {A} \ to \ texttt {B}) \ to (\ texttt {[A]} \ to \ texttt {[B]})$$

called map , the input function $$$\ texttt {f}: \ texttt {A} \ to \ texttt {B}$ , and the output returns function $$$\ texttt {map (f)}: \ texttt {[A]} \ to \ texttt {[B]}$ , recursively defined as follows: if the input list is empty, then the output list is the same. Otherwise, the input list consists of an object of type $$$\ texttt {A}$ and sublists, and $$$\ texttt {map (f)}$ applies $$$\ texttt {f}$ to the object and then $$$\ texttt {map} (f)$ to sub-list, and all of them together make the output list. The length of the function list is obtained using $$$\ texttt {map}$ to unique function $$$\ texttt {A} \ to \ texttt {1}$ .

(Fans of category theory will see that, in fact, in this entry, the list constructor is a functor. There are even programming languages ​​like Haskell that recognize this fact and use it.)

Example. The height of the tree can be recursively defined as follows: the height of a point is equal to $$$0$ . If a tree is not a point, then it has two subtrees, and then the tree height is one more than the maximum height of its subtrees.

Example. Games with guaranteed completion can be organized into four non-overlapping classes: the game is

• positive if the left one wins regardless of who goes first,
• negative if the right one wins regardless of who goes first,
• , , ,
• , , .

Here, “victory” means victories in a normal game, when the first player who cannot make a move loses. The above classes correspond to the four functions.

$$

$$\texttt{isPositive}, \texttt{isNegative}, \texttt{isZero}, \texttt{isFuzzy} : \texttt{Game} \to \texttt{Bool}$$

which can be recursively defined through each other as follows:

• A game is positive if and only if at least one of the variants of the left is positive or zero, and all the variants of the right are positive or fuzzy.
• A game is negative if and only if all variants of the left are negative or indistinct, and at least one of the variants of the right is negative or zero.
• A game is zero if and only if none of the variants of the left are positive or non-zero, and none of the variants of the right are negative or non-zero.
• A game is fuzzy if and only if at least one of the variants of the left is positive or zero and at least one of the variants of the right is negative or zero.

(For lovers of category theory: recursively defined functions are the application of the universal property of initial algebras.)

Recursive types are another reason to assume that mathematics has a type system: they allow much more recursion to be recorded than it is usually explicitly mentioned in mathematics, where write it using induction (recursion over$$Nat ) or sometimestransfinite induction$\texttt{Nat}$ (recursion over altered$$$\texttt{Set}$ ).Recursive types, on the contrary, provide a general record of structural induction . Often we can reduce the cases of structural induction we need to ordinary induction (for example, if we want to perform structural induction for trees, then we can perform ordinary induction for their vertices), but conceptually structural induction is clearer (for example, we can perform structural induction for trees without highlighting a specific vertex function).

Conclusion

Although theoretically mathematics is not often described as having a type system, in practice it turns out to be both more useful and more accurate to describe mathematics as having such a system. This gives us a language to understand certain types of mathematical errors (typing errors), as well as to understand certain implied mathematical actions (overloads). In addition, types have an interesting mathematical structure and provide a richer language for defining and working with recursively defined mathematical objects than traditional methods.