Types and functions
This is the third article in the series "Theory of Categories for Programmers."
The category of types and functions plays an important role in programming, so let's talk about what types are and why we need them.
There is some disagreement in the community about the advantages of static typing versus dynamic and strong typing versus weak typing. Let me illustrate the choice of typing with a thought experiment. Imagine millions of monkeys with keyboards happily pressing random keys that write, compile, and run programs.
')
With a machine language, any combination of bytes produced by monkeys will be accepted and launched. But in high-level languages, it is highly appreciated that the compiler is able to detect lexical and grammatical errors. Many programs will simply be rejected, and the monkeys will remain without bananas, but the rest will be more likely to be meaningful. Type checking provides another barrier against meaningless programs. In addition, while in dynamically typed languages, type mismatches will only be detected at runtime, in strongly typed statically checked languages, type mismatches are detected at compile time, which eliminates many incorrect programs before they have a chance to be launched.
So the question is, do we want the monkeys to be happy, or to create correct programs?
(comment of the translator: do not be offended, the author just loves less boring metaphors than RNGs and "random byte sequences", rather than calling programmers monkeys).
Usually the goal of a mental experiment with printing monkeys is the creation of the complete works of Shakespeare. Checking spelling and grammar in a cycle will dramatically increase the chances of success. The analog of type checking will go even further: after Romeo is declared by man, the type check will make sure that leaves do not grow on him and that he does not catch photons with his powerful gravitational field.
Category theory studies the composition of arrows. Not any two arrows can be arranged: the target object of one arrow must match the original object of the next. In programming, we transfer the results from one function to another. The program will not work if the second function cannot correctly interpret the data obtained using the first one. Both functions must fit together in order for their composition to work. The stronger the language type system, the better this fit can be described and automatically verified.
The only serious argument I hear against strong static typing: it can reject some programs that are semantically correct. In practice, this happens extremely rarely (note of the translator: in order to avoid sracha, I note that the author did not take into account, or disagree that there are many styles, and the duck-typing familiar to the programmer in scripting languages ​​also has the right to life. On the other hand, duck -typing is possible in the strict type system through templates, traits, type classes, interfaces, there are a lot of technologies, so the author’s opinion cannot be considered strictly wrong.) and, in any case, each language contains some kind of backdoor to bypass the system types when it is really necessary. Even Haskell has unsafeCoerce. But such constructions should be used wisely. Franz Kafka's character, Gregor Zamza, violates the type system when he turns into a giant beetle, and we all know how it ended. (Translator's comment: bad :) .
Another argument I often hear is that strong typing puts too much stress on the programmer. I can sympathize with this problem, since I myself wrote a few declarations of iterators in C ++, except that there is a technology, type inference, which allows the compiler to deduce most types from the context in which they are used. In C ++, you can declare an auto variable, and the compiler will output the type for you.
In Haskell, except in rare cases, type annotations are optional. Programmers, as a rule, still use them, because types can tell a lot about the semantics of the code, and type declarations help to understand compilation errors. A common practice in Haskell is to start a project with type development. Later, type annotations are the basis for implementation and become guaranteed compiler comments.
Strict static typing is often used as a pretext for not testing code. Sometimes you can hear Haskell programmers say, “If the code is compiled, it is correct.” Of course, there is no guarantee that a program that is correct in terms of types is correct in the sense of a correct result. As a result of this attitude, in a number of studies, Haskell did not begin to strongly outperform other languages ​​in terms of the quality of the code, as one would expect. It seems that under commercial conditions, the need to repair bugs exists only to a certain level of quality, which is mainly related to the economics of software development and end-user tolerance, and is very weakly related to a programming language or development methodology. The best criterion would be to measure how many projects are lagging behind the schedule or delivered with greatly reduced functionality.
Now, with regard to the assertion that unit testing can replace strong typing. Consider the general practice of refactoring in strongly typed languages: changing the type of the argument of a function. In strongly typed languages, it is enough to change the declaration of this function and then fix all the build errors. In weakly typed languages, the fact that the function in now expects other data cannot be associated with the caller.
Unit testing can catch some of the inconsistencies, but testing is almost always a probabilistic rather than a deterministic process (note of the translator: perhaps the test suite was meant: you cover not all possible inputs, but some representative sample.) Testing is a poor substitute for proof of correctness.
The simplest type description: they are sets of values. Type Bool (remember, specific types begin with a capital letter in Haskell) correspond to a set of two elements: True and False. Type Char is the set of all Unicode characters, for example, 'a' or 'Ä…'.
Sets can be finite or infinite. The String type, which is essentially synonymous with the list Char, is an example of an infinite set.
When we declare x as an integer:
we say that it is an element of the set of integers. Haskell's Integer is infinite, and can be used for arithmetic of any accuracy. There is also a finite set Int, which corresponds to a machine type, like int in C ++.
There are some subtleties that make tying types to sets complex. There are problems with polymorphic functions that have cyclical definitions, as well as the fact that you cannot have a set of all sets; but, as I promised, I will not be a strict mathematician. The important thing is that there is a category of sets called Set, and we will work with it.
In Set, objects are sets, and morphisms (arrows) are functions.
Set is a special category, because we can look inside its objects and this will help to understand a lot of things intuitively. For example, we know that an empty set has no elements. We know that there are special sets from one element. We know that functions map elements of one set to elements of another. They can display two elements in one, but not one element in two. We know that the identical function maps each element of the set into itself, and so on. I plan to gradually forget all this information and instead express all these concepts in a purely categorical form, that is, in terms of objects and arrows.
In an ideal world, we could just say that types in Haskell are sets, and functions in Haskell are mathematical functions between them. There is only one small problem: a mathematical function does not execute any code — it only knows the answer. A function in Haskell must evaluate the response. This is not a problem if the answer can be obtained in a finite number of steps, no matter how large. But there are some calculations that involve recursion, and they may never complete. We can't just ban non-terminating functions in Haskell because discerning whether a function is terminating or not — the famous stop problem is insoluble. That is why computer scientists came up with a brilliant idea, or a dirty hack, depending on your point of view, to expand each type with a special meaning, called bottom (fooltski) in Russian, somehow who knows a good option, please suggest.) , which is denoted by _ | _ or in Unicode. This “value” corresponds to an incomplete calculation. So the function declared as:
can return True, False, or _ | _; the latter means that the function never terminates.
Interestingly, as soon as you take bottom to the type system, it is convenient to consider every runtime error for the bottom, and even allow the function to return the bottom explicitly. The latter is usually accomplished using the expression undefined:
This definition passes type checking because undefined is evaluated at the bottom, which is included in all types, including Bool. You can even write:
(without x) because bottom is also a member of the type Bool -> Bool.
Functions that can return bottom are called partial, as opposed to regular functions that return correct results for all possible arguments.
Because of the bottom, the category of Haskell types and functions is called Hask, not Set. From a theoretical point of view, this is a source of endless complications, so at this stage I will use my butcher knife and complete these considerations. From a pragmatic point of view, it is possible to ignore non-terminating functions and bottom and work with Hask as with a full Set.
As a programmer, you are familiar with the syntax and grammar of a programming language. These aspects of the language are usually formally described at the very beginning of the language specification. But the meaning and semantics of a language is much more difficult to describe; This description takes up much more pages, rarely quite formally, and almost never complete. Hence the never ending discussions among language lawyers, and the whole artisanal industry of books devoted to the interpretation of the subtleties of language standards.
There are formal means for describing the semantics of a language, but because of their complexity, they are mainly used for simplified, academic languages, and not real giants of industrial programming. One of these tools is called operational semantics and describes the mechanics of program execution. It defines a formalized, idealized interpreter. The semantics of industrial languages, such as C ++, are usually described using informal reasoning, often in terms of "abstract machine".
The problem is that it is very difficult to prove something about programs using operational semantics. To show a certain property of a program, you essentially have to “launch it” through an idealized interpreter.
It does not matter that programmers never formally prove correctness. We always “think” that we write the right programs. Nobody is sitting at the keyboard, saying, “Oh, I’ll just write a few lines of code and see what happens.” (Comment of the translator: oh, if ...) We believe that the code we write will perform certain actions that produce the desired results. We are usually very surprised if this is not the case. This means that we really think about the programs we write and we usually do this by running the interpreter in our heads. , it's very difficult to keep track of all the variables. Computers are good for executing programs, people - No. If we were, we would not need a computer!.
But there is an alternative. It is called denotational semantics and is based on mathematics. In the denotational semantics for each language construct a mathematical interpretation is described. Thus, if you want to prove a property of a program, you simply prove a mathematical theorem. You think that proving theorems is difficult, but in fact we humans have built mathematical methods for thousands of years, so there is a lot of accumulated knowledge that can be used. In addition, compared with theorems that prove professional mathematics, the problems we encounter in programming are usually quite simple, if not trivial. (comment of the translator: for proof, the author does not try to offend programmers.)
Consider the definition of the factorial function in Haskell, a language that is easy to denotative semantics:
The expression [1..n] is a list of integers from 1 to n. The product function multiplies all the items in the list. Just as the definition of factorial taken from the textbook. Compare this to C:
Do I need to continue? (comment of the translator: the author slightly cheated by taking a library function in Haskell. In fact, there was no need for cunning, an honest description is by definition no more difficult) :
Well, I immediately admit that it was a cheap reception! Factorial has an obvious mathematical definition. An astute reader may ask: What is the mathematical model for reading a character from the keyboard, or sending a packet over the network? For a long time, this would be an awkward question, leading to rather confusing explanations. It seemed that denotational semantics is not suitable for a significant number of important tasks that are necessary for writing useful programs, and which can be easily solved by operational semantics. The breakthrough came from category theory. Eugenio Modji discovered that computational effects can be converted to monads. This turned out to be an important observation, which not only gave the denotational semantics a new life and made purely functional programs more convenient, but also gave new information about traditional programming. I will talk about monads later when we develop more categorical tools.
One of the important advantages of having a mathematical model for programming is the ability to perform a formal proof of software correctness. This may not seem so important when you are writing consumer software, but there are areas of programming where the cost of failure can be huge, or where human life is at risk. But even when writing web applications for the healthcare system, you can appreciate the idea that functions and algorithms from the Haskell standard library come with proof of correctness.
What we call functions in C ++ or any other imperative language is not the same thing that mathematicians call functions. A math function is simply a mapping of values ​​to values.
We can implement a mathematical function in a programming language: such a function, having an input value, will calculate the output value. The function for getting the square of a number is likely to multiply the input value by itself. It will do this on every call, and is guaranteed to produce the same result each time it is called with the same argument. The square of the number does not change with the phases of the moon.
In addition, calculating the square of the number should not have a side effect, like giving a delicious nishtyachka to your dog. The “function” that does this cannot be easily modeled by a mathematical function.
In programming languages, functions that always give the same result on the same arguments and have no side effects are called pure. In a pure functional language, like Haskell, all functions are pure. Thanks to this, it is easier to determine the denotational semantics of these languages ​​and model them using category theory. As for other languages, you can always limit yourself to a pure subset, or think about side effects separately. Later we will see how monads allow you to simulate all kinds of effects using only pure functions. As a result, we lose nothing, being limited to mathematical functions.
Once you decide that types are sets, you can come up with some very exotic examples. For example, which type corresponds to the empty set? No, this is not void in C ++, although this type is called Void in Haskell. This is a type that is not filled with any value. You can define a function that accepts Void, but you can never call it. To call it, you will have to provide a value of type Void, but it is simply not there. As for the fact that this function can return - there are no restrictions. It can return any type (although this will never happen because it cannot be called). In other words, this is a function that is polymorphic in a return type. Haskellers called it:
(comment of translator: it is impossible to define such a function in C ++: in C ++, each type has at least one value.)
(Remember that a is a type variable, which can be any type.) This name is not accidental. There is a deeper interpretation of types and functions from the point of view of logic called the Curry-Howard isomorphism. The Void type is untrue, and the absurd function is a statement that something follows from a falsehood, as in the Latin phrase “ex falso sequitur quodlibet.” (Note of the translator: anything follows from a falsehood.)
Next comes the type corresponding to the singleton set. This is a type that has only one possible value. This value is simply "is." You might not immediately recognize it, but this is void in C ++. Think about the functions from and to this type. The function from void can always be called. If it is a pure function, it will always return the same result. Here is an example of such a function:
You might think that this function accepts "nothing", but, as we have just seen, a function that accepts "nothing" cannot be called, because there is no value representing the type "nothing". So what does this feature accept? Conceptually, it takes a dummy value that has only a single instance, so that we can explicitly omit it in the code. In Haskell, however, there is a symbol for this value: an empty pair of parentheses (). Thus, because of a funny coincidence (or not a coincidence?), The function call from void looks the same in C ++ and in Haskell. In addition, because of Haskell’s love for conciseness, the same symbol () is also used for the type, the constructor, and the only value corresponding to the singleton set. Here is the function in Haskell:
The first line declares that f44 converts the type (), named "one", into the type Integer. The second line specifies that f44, using pattern matching, converts a single constructor for the unit, namely () to the number 44. You call this function by providing the value ():
Note that each function from one is equivalent to choosing one element from the target type (here, select Integer 44). In fact, you can think of f44 as a different representation of the number 44. This is an example of how we can replace the direct mention of the elements of a set with a function (arrow). The functions from one to some type A are in one-to-one correspondence with the elements of the set A.
What about functions that return void, or, in Haskell, return ones? In C ++, such functions are used for side effects, but we know that such functions are not real, in the mathematical sense of the word. A pure function that returns a unit does nothing: it drops its argument.
Mathematically, a function from the set A to a singleton set maps each element to a single element of this set. For each A there is exactly one such function. Here it is for Integer:
You give it any integer, and it returns a one. Following the spirit of brevity, Haskell allows the use of an underscore as an argument, which is discarded. Thus, no need to invent a name for it. The code above can be rewritten as:
Please note that the execution of this function is not only independent of the value passed to it, but also on the type of the argument.
Functions that can be defined by the same formula for any type are called parametrically polymorphic. You can implement a whole family of such functions with a single equation, using a parameter instead of a specific type. How to name a polymorphic function from any type into a unit? Of course, we will call its unit:
In C ++, you would implement it like this:
(comment of the translator: in order to help the compiler to optimize it in noop, it's better this way):
Further, in the "typology of types" a set of two elements. In C ++, it is called bool, and in Haskell, not surprisingly, Bool. The difference is that in C ++ bool is a built-in type, while in Haskell it can be defined as follows:
(It’s worth reading this definition: Bool can be either True or False.) In principle, one could also describe this type in C ++:
But the C ++ enum is actually an integer. You could use C ++ 11 “class enum”, but then you would have to specify the value with the class name: bool :: true or bool :: false, not to mention the need to include the corresponding header in each file that uses it.
Pure functions from Bool simply select two values ​​from the target type, one corresponding to True and the other False.
Functions in Bool are called predicates. For example, the Data.Char library in Haskell contains many predicates, such as IsAlpha or isDigit. In C ++, there is a similar <cctype> library, which declares, among other things, the isalpha and isdigit functions, but they return an int, not a boolean value. These predicates are defined in <locale> and are called ctype :: is (alpha, c) and ctype :: is (digit, c).
Category Theory for Programmers: Preface
Category: essence of composition
Types and functions
Categories big and small
Categories
The category of types and functions plays an important role in programming, so let's talk about what types are and why we need them.
Who needs types?
There is some disagreement in the community about the advantages of static typing versus dynamic and strong typing versus weak typing. Let me illustrate the choice of typing with a thought experiment. Imagine millions of monkeys with keyboards happily pressing random keys that write, compile, and run programs.
')
With a machine language, any combination of bytes produced by monkeys will be accepted and launched. But in high-level languages, it is highly appreciated that the compiler is able to detect lexical and grammatical errors. Many programs will simply be rejected, and the monkeys will remain without bananas, but the rest will be more likely to be meaningful. Type checking provides another barrier against meaningless programs. In addition, while in dynamically typed languages, type mismatches will only be detected at runtime, in strongly typed statically checked languages, type mismatches are detected at compile time, which eliminates many incorrect programs before they have a chance to be launched.
So the question is, do we want the monkeys to be happy, or to create correct programs?
(comment of the translator: do not be offended, the author just loves less boring metaphors than RNGs and "random byte sequences", rather than calling programmers monkeys).
Usually the goal of a mental experiment with printing monkeys is the creation of the complete works of Shakespeare. Checking spelling and grammar in a cycle will dramatically increase the chances of success. The analog of type checking will go even further: after Romeo is declared by man, the type check will make sure that leaves do not grow on him and that he does not catch photons with his powerful gravitational field.
Types needed for composability
Category theory studies the composition of arrows. Not any two arrows can be arranged: the target object of one arrow must match the original object of the next. In programming, we transfer the results from one function to another. The program will not work if the second function cannot correctly interpret the data obtained using the first one. Both functions must fit together in order for their composition to work. The stronger the language type system, the better this fit can be described and automatically verified.
The only serious argument I hear against strong static typing: it can reject some programs that are semantically correct. In practice, this happens extremely rarely (note of the translator: in order to avoid sracha, I note that the author did not take into account, or disagree that there are many styles, and the duck-typing familiar to the programmer in scripting languages ​​also has the right to life. On the other hand, duck -typing is possible in the strict type system through templates, traits, type classes, interfaces, there are a lot of technologies, so the author’s opinion cannot be considered strictly wrong.) and, in any case, each language contains some kind of backdoor to bypass the system types when it is really necessary. Even Haskell has unsafeCoerce. But such constructions should be used wisely. Franz Kafka's character, Gregor Zamza, violates the type system when he turns into a giant beetle, and we all know how it ended. (Translator's comment: bad :) .
Another argument I often hear is that strong typing puts too much stress on the programmer. I can sympathize with this problem, since I myself wrote a few declarations of iterators in C ++, except that there is a technology, type inference, which allows the compiler to deduce most types from the context in which they are used. In C ++, you can declare an auto variable, and the compiler will output the type for you.
In Haskell, except in rare cases, type annotations are optional. Programmers, as a rule, still use them, because types can tell a lot about the semantics of the code, and type declarations help to understand compilation errors. A common practice in Haskell is to start a project with type development. Later, type annotations are the basis for implementation and become guaranteed compiler comments.
Strict static typing is often used as a pretext for not testing code. Sometimes you can hear Haskell programmers say, “If the code is compiled, it is correct.” Of course, there is no guarantee that a program that is correct in terms of types is correct in the sense of a correct result. As a result of this attitude, in a number of studies, Haskell did not begin to strongly outperform other languages ​​in terms of the quality of the code, as one would expect. It seems that under commercial conditions, the need to repair bugs exists only to a certain level of quality, which is mainly related to the economics of software development and end-user tolerance, and is very weakly related to a programming language or development methodology. The best criterion would be to measure how many projects are lagging behind the schedule or delivered with greatly reduced functionality.
Now, with regard to the assertion that unit testing can replace strong typing. Consider the general practice of refactoring in strongly typed languages: changing the type of the argument of a function. In strongly typed languages, it is enough to change the declaration of this function and then fix all the build errors. In weakly typed languages, the fact that the function in now expects other data cannot be associated with the caller.
Unit testing can catch some of the inconsistencies, but testing is almost always a probabilistic rather than a deterministic process (note of the translator: perhaps the test suite was meant: you cover not all possible inputs, but some representative sample.) Testing is a poor substitute for proof of correctness.
What are types?
The simplest type description: they are sets of values. Type Bool (remember, specific types begin with a capital letter in Haskell) correspond to a set of two elements: True and False. Type Char is the set of all Unicode characters, for example, 'a' or 'Ä…'.
Sets can be finite or infinite. The String type, which is essentially synonymous with the list Char, is an example of an infinite set.
When we declare x as an integer:
x :: Integer we say that it is an element of the set of integers. Haskell's Integer is infinite, and can be used for arithmetic of any accuracy. There is also a finite set Int, which corresponds to a machine type, like int in C ++.
There are some subtleties that make tying types to sets complex. There are problems with polymorphic functions that have cyclical definitions, as well as the fact that you cannot have a set of all sets; but, as I promised, I will not be a strict mathematician. The important thing is that there is a category of sets called Set, and we will work with it.
In Set, objects are sets, and morphisms (arrows) are functions.
Set is a special category, because we can look inside its objects and this will help to understand a lot of things intuitively. For example, we know that an empty set has no elements. We know that there are special sets from one element. We know that functions map elements of one set to elements of another. They can display two elements in one, but not one element in two. We know that the identical function maps each element of the set into itself, and so on. I plan to gradually forget all this information and instead express all these concepts in a purely categorical form, that is, in terms of objects and arrows.
In an ideal world, we could just say that types in Haskell are sets, and functions in Haskell are mathematical functions between them. There is only one small problem: a mathematical function does not execute any code — it only knows the answer. A function in Haskell must evaluate the response. This is not a problem if the answer can be obtained in a finite number of steps, no matter how large. But there are some calculations that involve recursion, and they may never complete. We can't just ban non-terminating functions in Haskell because discerning whether a function is terminating or not — the famous stop problem is insoluble. That is why computer scientists came up with a brilliant idea, or a dirty hack, depending on your point of view, to expand each type with a special meaning, called bottom (fooltski) in Russian, somehow who knows a good option, please suggest.) , which is denoted by _ | _ or in Unicode. This “value” corresponds to an incomplete calculation. So the function declared as:
f :: Bool -> Bool can return True, False, or _ | _; the latter means that the function never terminates.
Interestingly, as soon as you take bottom to the type system, it is convenient to consider every runtime error for the bottom, and even allow the function to return the bottom explicitly. The latter is usually accomplished using the expression undefined:
f :: Bool -> Bool fx = undefined This definition passes type checking because undefined is evaluated at the bottom, which is included in all types, including Bool. You can even write:
f :: Bool -> Bool f = undefined (without x) because bottom is also a member of the type Bool -> Bool.
Functions that can return bottom are called partial, as opposed to regular functions that return correct results for all possible arguments.
Because of the bottom, the category of Haskell types and functions is called Hask, not Set. From a theoretical point of view, this is a source of endless complications, so at this stage I will use my butcher knife and complete these considerations. From a pragmatic point of view, it is possible to ignore non-terminating functions and bottom and work with Hask as with a full Set.
Why do we need a mathematical model?
As a programmer, you are familiar with the syntax and grammar of a programming language. These aspects of the language are usually formally described at the very beginning of the language specification. But the meaning and semantics of a language is much more difficult to describe; This description takes up much more pages, rarely quite formally, and almost never complete. Hence the never ending discussions among language lawyers, and the whole artisanal industry of books devoted to the interpretation of the subtleties of language standards.
There are formal means for describing the semantics of a language, but because of their complexity, they are mainly used for simplified, academic languages, and not real giants of industrial programming. One of these tools is called operational semantics and describes the mechanics of program execution. It defines a formalized, idealized interpreter. The semantics of industrial languages, such as C ++, are usually described using informal reasoning, often in terms of "abstract machine".
The problem is that it is very difficult to prove something about programs using operational semantics. To show a certain property of a program, you essentially have to “launch it” through an idealized interpreter.
It does not matter that programmers never formally prove correctness. We always “think” that we write the right programs. Nobody is sitting at the keyboard, saying, “Oh, I’ll just write a few lines of code and see what happens.” (Comment of the translator: oh, if ...) We believe that the code we write will perform certain actions that produce the desired results. We are usually very surprised if this is not the case. This means that we really think about the programs we write and we usually do this by running the interpreter in our heads. , it's very difficult to keep track of all the variables. Computers are good for executing programs, people - No. If we were, we would not need a computer!.
But there is an alternative. It is called denotational semantics and is based on mathematics. In the denotational semantics for each language construct a mathematical interpretation is described. Thus, if you want to prove a property of a program, you simply prove a mathematical theorem. You think that proving theorems is difficult, but in fact we humans have built mathematical methods for thousands of years, so there is a lot of accumulated knowledge that can be used. In addition, compared with theorems that prove professional mathematics, the problems we encounter in programming are usually quite simple, if not trivial. (comment of the translator: for proof, the author does not try to offend programmers.)
Consider the definition of the factorial function in Haskell, a language that is easy to denotative semantics:
fact n = product [1..n] The expression [1..n] is a list of integers from 1 to n. The product function multiplies all the items in the list. Just as the definition of factorial taken from the textbook. Compare this to C:
int fact(int n) { int i; int result = 1; for (i = 2; i <= n; ++i) result *= i; return result; } Do I need to continue? (comment of the translator: the author slightly cheated by taking a library function in Haskell. In fact, there was no need for cunning, an honest description is by definition no more difficult) :
fact 0 = 1 fact n = n * fact (n - 1) Well, I immediately admit that it was a cheap reception! Factorial has an obvious mathematical definition. An astute reader may ask: What is the mathematical model for reading a character from the keyboard, or sending a packet over the network? For a long time, this would be an awkward question, leading to rather confusing explanations. It seemed that denotational semantics is not suitable for a significant number of important tasks that are necessary for writing useful programs, and which can be easily solved by operational semantics. The breakthrough came from category theory. Eugenio Modji discovered that computational effects can be converted to monads. This turned out to be an important observation, which not only gave the denotational semantics a new life and made purely functional programs more convenient, but also gave new information about traditional programming. I will talk about monads later when we develop more categorical tools.
One of the important advantages of having a mathematical model for programming is the ability to perform a formal proof of software correctness. This may not seem so important when you are writing consumer software, but there are areas of programming where the cost of failure can be huge, or where human life is at risk. But even when writing web applications for the healthcare system, you can appreciate the idea that functions and algorithms from the Haskell standard library come with proof of correctness.
Clean and Dirty Functions
What we call functions in C ++ or any other imperative language is not the same thing that mathematicians call functions. A math function is simply a mapping of values ​​to values.
We can implement a mathematical function in a programming language: such a function, having an input value, will calculate the output value. The function for getting the square of a number is likely to multiply the input value by itself. It will do this on every call, and is guaranteed to produce the same result each time it is called with the same argument. The square of the number does not change with the phases of the moon.
In addition, calculating the square of the number should not have a side effect, like giving a delicious nishtyachka to your dog. The “function” that does this cannot be easily modeled by a mathematical function.
In programming languages, functions that always give the same result on the same arguments and have no side effects are called pure. In a pure functional language, like Haskell, all functions are pure. Thanks to this, it is easier to determine the denotational semantics of these languages ​​and model them using category theory. As for other languages, you can always limit yourself to a pure subset, or think about side effects separately. Later we will see how monads allow you to simulate all kinds of effects using only pure functions. As a result, we lose nothing, being limited to mathematical functions.
Type examples
Once you decide that types are sets, you can come up with some very exotic examples. For example, which type corresponds to the empty set? No, this is not void in C ++, although this type is called Void in Haskell. This is a type that is not filled with any value. You can define a function that accepts Void, but you can never call it. To call it, you will have to provide a value of type Void, but it is simply not there. As for the fact that this function can return - there are no restrictions. It can return any type (although this will never happen because it cannot be called). In other words, this is a function that is polymorphic in a return type. Haskellers called it:
absurd :: Void -> a (comment of translator: it is impossible to define such a function in C ++: in C ++, each type has at least one value.)
(Remember that a is a type variable, which can be any type.) This name is not accidental. There is a deeper interpretation of types and functions from the point of view of logic called the Curry-Howard isomorphism. The Void type is untrue, and the absurd function is a statement that something follows from a falsehood, as in the Latin phrase “ex falso sequitur quodlibet.” (Note of the translator: anything follows from a falsehood.)
Next comes the type corresponding to the singleton set. This is a type that has only one possible value. This value is simply "is." You might not immediately recognize it, but this is void in C ++. Think about the functions from and to this type. The function from void can always be called. If it is a pure function, it will always return the same result. Here is an example of such a function:
int f44() { return 44; } You might think that this function accepts "nothing", but, as we have just seen, a function that accepts "nothing" cannot be called, because there is no value representing the type "nothing". So what does this feature accept? Conceptually, it takes a dummy value that has only a single instance, so that we can explicitly omit it in the code. In Haskell, however, there is a symbol for this value: an empty pair of parentheses (). Thus, because of a funny coincidence (or not a coincidence?), The function call from void looks the same in C ++ and in Haskell. In addition, because of Haskell’s love for conciseness, the same symbol () is also used for the type, the constructor, and the only value corresponding to the singleton set. Here is the function in Haskell:
f44 :: () -> Integer f44 () = 44 The first line declares that f44 converts the type (), named "one", into the type Integer. The second line specifies that f44, using pattern matching, converts a single constructor for the unit, namely () to the number 44. You call this function by providing the value ():
f44 () Note that each function from one is equivalent to choosing one element from the target type (here, select Integer 44). In fact, you can think of f44 as a different representation of the number 44. This is an example of how we can replace the direct mention of the elements of a set with a function (arrow). The functions from one to some type A are in one-to-one correspondence with the elements of the set A.
What about functions that return void, or, in Haskell, return ones? In C ++, such functions are used for side effects, but we know that such functions are not real, in the mathematical sense of the word. A pure function that returns a unit does nothing: it drops its argument.
Mathematically, a function from the set A to a singleton set maps each element to a single element of this set. For each A there is exactly one such function. Here it is for Integer:
fInt :: Integer -> () fInt x = () You give it any integer, and it returns a one. Following the spirit of brevity, Haskell allows the use of an underscore as an argument, which is discarded. Thus, no need to invent a name for it. The code above can be rewritten as:
fInt :: Integer -> () fInt _ = () Please note that the execution of this function is not only independent of the value passed to it, but also on the type of the argument.
Functions that can be defined by the same formula for any type are called parametrically polymorphic. You can implement a whole family of such functions with a single equation, using a parameter instead of a specific type. How to name a polymorphic function from any type into a unit? Of course, we will call its unit:
unit :: a -> () unit _ = () In C ++, you would implement it like this:
template<class T> void unit(T) {} (comment of the translator: in order to help the compiler to optimize it in noop, it's better this way):
template<class T> void unit(T&&) {} Further, in the "typology of types" a set of two elements. In C ++, it is called bool, and in Haskell, not surprisingly, Bool. The difference is that in C ++ bool is a built-in type, while in Haskell it can be defined as follows:
data Bool = True | False (It’s worth reading this definition: Bool can be either True or False.) In principle, one could also describe this type in C ++:
enum bool { true, false }; But the C ++ enum is actually an integer. You could use C ++ 11 “class enum”, but then you would have to specify the value with the class name: bool :: true or bool :: false, not to mention the need to include the corresponding header in each file that uses it.
Pure functions from Bool simply select two values ​​from the target type, one corresponding to True and the other False.
Functions in Bool are called predicates. For example, the Data.Char library in Haskell contains many predicates, such as IsAlpha or isDigit. In C ++, there is a similar <cctype> library, which declares, among other things, the isalpha and isdigit functions, but they return an int, not a boolean value. These predicates are defined in <locale> and are called ctype :: is (alpha, c) and ctype :: is (digit, c).
Category Theory for Programmers: Preface
Category: essence of composition
Types and functions
Categories big and small
Categories
Source: https://habr.com/ru/post/247765/
All Articles