September 16, 2011 at 03:13Another Monad Guide (Part 3: Monad Laws)
- Transfer
By Mike Vanier
In a previous article, I talked about two fundamental monadic operations of the Monad type class: the bind operator (bind, >> =) and the return function. In this article, I will end up with the definition of the Monad type class and talk about monad laws.
Let's take a look at the entire Monad type class definition:
We see the familiar: the >> = operator and the return function with the same types, but besides them there is also the >> operator and the fail function. What do they mean?
The fail function is initially a very primitive way of reporting an error. It is called when the >> = operator cannot bind a value of type a to a function of type a -> mb due to matching errors. I do not want to go into the details of this mechanism now, because it is boring; see the documentation on the Haskell website if you need it. In most cases, worry about fail is not necessary.
The >> operator is a little more interesting. He has this type:
This operator is a monadic sequence operator. In particular, it is a variant of monadic application (>> = or “bind”), which discards an unpacked value of type a before performing an “action” of type m b. It is defined as follows:
We can see here that any value unpacked from the monadic value mv1 is rejected, and then the final monadic value mv2 is returned. The operator is useful when the type of the unpacked value is (), that is, it is an empty type. The putStrLn function can be considered a good example:
Imagine you want to print two lines, one after the other, with line breaks after each. You can do this:
And why does this work? Let's look at the types:
That is, the >> operator combines two monadic values of type IO () into one resulting monadic value of type IO (). Let's take the >> operator and specialize it for our case:
If m is IO, and a and b are (), then we get:
By writing, we can say that, probably, the >> operator performs two “actions” in a row - printing a line.
Now a more complex example. We need to read a line of text from the terminal and print it twice. We can do it like this:
Due to the priorities of the operators, the record can be left without brackets:
So what does this mean? getLine - monadic value ("action"), which reads a line of text from the terminal. The >> = operator “unpacks” this string from a monadic value and associates it with the name s (because \ s -> putStrLn s >> putStrLn s is a monadic function, the second argument of the >> = operator). Then the line called s is used by the monadic value putStrLn s >> putStrLn s, which prints it two times in succession.
If what you say seems mystic, it is not your fault. Something strange is happening here in the depths, but until I talked about the state monad, I can’t explain it. But now you must be able to trace what is happening, even if you still do not fully understand how it happens.
Right now I'm going to go back a bit and look at the monad laws. They play a large role in using the >> = operator and the return function for each particular monad. After that we will turn to more practical materials.
Many important laws go in groups of three: three mechanical laws of Newton, three laws of thermodynamics, Three Laws of Azimov Robotics, three Kepler laws of planetary motion, and so on and so on. Monads in this do not differ, well, of course, with the exception that the "Three Monad Laws" are more important than anything else. ;-)
For the >> = operator and the return function to be correct for a particular monad, they must have the correct types of this monad. So, for example, the definitions >> = and return for Maybe monad contain its type:
And for monads, IOs contain type IO:
However, this is not enough. These functions / operators are also required to satisfy the three “monad laws”. Monad laws are actually very simple; they are designed to ensure that the monadic composition works in a predictable way. First I will give you a “nice” version of the monad laws, and then I will show the (ugly) way, as they are usually described. (Tell me thanks: the “nice” option is much easier to understand.)
Here is a nice definition of the three monadic laws expressed in terms of monadic composition (remember that the operator (> =>) is a monadic operator of composition of functions):
What are these laws telling us?
Laws 1 and 2 say what return should be: this is the unit (neutral element) for the monadic composition of functions (the first rule states that return is the left unit, and the second that the right). In other words, composing the monadic function f and return (in any order) simply returns the function f. Analogs can be considered 0 - a neutral element for the function of adding integers, and 1 - a neutral element for the integer multiplication function; in each of the cases, the neutral element connected to the usual value using the corresponding function will simply return this value back.
Law 3 states that the monadic function of composition is associative: when we want to combine three monadic functions (f, g, h), it does not matter which two we connect first. This is analogous to the fact that addition and multiplication are also associative when applied to integers.
Don't these laws seem vaguely familiar to you? Let us take a look at the corresponding “laws”, which are satisfied by the usual function of composition:
where id is a neutral element, unit. Did you catch the resemblance? The composition of a function with a unit on the left or right will give the same function again, and the composition function is associative. The monadic function of the composition must be associative, and return must be the monadic equivalent of a single function, so that the behavior of the monadic composition is as predictable as the behavior of a regular composition.
What is the meaning of these laws from the point of view of a programmer? Since we want our monads to behave intelligently, our definitions of return and >> = must satisfy these laws. We will soon learn how to verify the definitions of >> = and return. [Note that monadic laws are expressed in terms of the>>> operator, not the >> = operator, but we will see the version using >> =, it is equivalent.
, there is a catch: Haskell does not check monad laws! The only thing that is checked is that the return and >> = definition types are correct. Whether laws are being implemented or not, the programmer must check.
Many people ask, “Why can't Haskell check monadic laws?” The answer is simple: Haskell is not yet powerful enough! In order to get a sufficiently powerful language that proves the correctness of monad laws, you need something like a theorem prover (teorem prover). Proofs of theorems are breathtaking, and they may be the future of programming, but they are much more complex than traditional programming languages. If you're interested, there is a respected proof of Coq theorems, it is available here.. But in Haskell, the programmer must take care that the monad he wrote does not violate monad laws.
The problem with the nice version is that the> => operator is not defined directly in the Monad type class; instead, the >> = operator is defined, and the> => operator is derived from it, as I showed above. So if we restrict the definitions to the >> >> and return operators, we need monadic laws containing only return and >> =. And in this form they are served in most books and documentation on monads in Haskell, despite being less intuitive than shown in the previous section.
In terms of the >> = operator and the return function, the monad laws look like this:
where the types of different values are:
for some types a, b, c and some kind of monad m.
Let's have fun and try to deduce an ugly version of monad laws from a nice version. In our calculations, we need the definition of monadic composition, which we examined above:
Law 1:
Note that \ x -> fx is the same as just f.
Law 2:
f> => return == f
\ x -> (fx >> = return) == \ x -> fx
fx >> = return == fx
let mv == fx
mv >> = return == mv - QED
Law 3:
In the calculation step (\ y -> (fy >> = g)) x, we simply apply the entire function (\ y -> ...) to the argument x; in this case, y is replaced by the variable x in the function body (it is indicated by the ellipsis (...)), and the function body is returned as a result. In the Lingo functional programming language, this operation is called beta reduction . {1: In this case, we are talking about a section of mathematics called lambda calculus, which describes, among other things, beta reduction.} Beta reduction is the main way to calculate functions. The last step, where y is replaced by x, is correct because the following two functions are correct:
- this is one and the same (the name of the formal argument does not matter). In the Lingo functional language, we would say that two functions are alpha equivalent . You must have understood the other steps.
Monad laws can sometimes be used in code, replacing a long expression with a shorter one (for example, instead of return x >> = f, you can simply write fx). However, we will show in the following articles that the main benefit of monad laws is that they allow us to derive definitions of return and >> = for specific monads.
At the end of this article, I want to show you a neat syntactic form of writing, with the help of which the monadic code looks much nicer.
Recall the readAndPrintLineTwice function defined above:
She has one advantage: it is written in one line. The disadvantage is not the most readable line in the world. Haskell designers noticed that monadic definitions are often difficult to read, and they come up with really nice syntactic sugar that makes definitions more readable.
The basis of this syntactic sugar is the observation that a huge number of operations in the monadic code are written in two forms:
Notation was designed with the intention of making these two forms readable. It starts with the do keyword, followed by some monadic operations. So these two of our examples will be written in do-notation:
In Form 1, the first line means that we take the monadic value mv and “unpack” it into a regular one called v. The second line is just calculating f from v. The result of the string fv is the result of the whole expression.
In Form 2, the monadic value (“action”) mv is “executed” in the first line. The second line “runs” another monadic value (“action”) mv2. Thus, we simply have a notation that concatenates mv and mv2 into a sequence, as the >> operator does.
The Haskell compiler converts a convenient do-notation to a non-do entry for Form 1 and Form 2. This is just a syntax conversion, and the meaning of both entries is identical. In addition, both forms can be mixed in one expression of each of the notations. Example:
This is exactly the same as:
Or without skokbok:
You can imagine that when monadic expressions expand, the do-form remains just as easy to read, while the form without do (also called “Sugared”) often becomes unreadable. That's why do-notation exists. It's great that do-notation works for all monads, not just one.
In addition, you can mix do-notation and sugarless notation in one expression. Like this:
This is sometimes useful, but can often cause poor code readability.
Let's see how our previous examples will look in do-notation.
Here the code is much easier to read thanks to do-notation. Interestingly, it has an additional advantage (or disadvantage, depending on which views you hold): the code in Haskell looks imperative! If we read the code from top to bottom, it looks like an imperative language, which instead of assigning the arrow <-. Let's say readAndPrintLine can be described as follows: “call getLine to read the line that we put in the line variable; then we call putStrLn to print this variable. ”This is definitely not what really happens (for example, line is not a variable), but you can read it that way. For a lot of code that does a lot of input and output, do-notation is a very convenient way to write.
Do notation has other useful properties. For example, you can embed let-expressions and case-expressions in the body of do-notation, which is often convenient. I will not go into details because this is a routine - take any other Haskell tutorial to explore this point.
In the next article, I will start talking about monads, starting with Maybe (the monad for calculations in which an error may occur) and ending with the list monad (for calculations with multiple results).
Part 1: basics
Part 2: functions >> = and return
Part 3: Monadic Laws
Part 4: Maybe monad and list monad
In a previous article, I talked about two fundamental monadic operations of the Monad type class: the bind operator (bind, >> =) and the return function. In this article, I will end up with the definition of the Monad type class and talk about monad laws.
Full Monad Type Class
Let's take a look at the entire Monad type class definition:
class Monad m where
(>> =) :: m a -> (a -> m b) -> m b
return :: a -> m a
(>>) :: m a -> m b -> m b
fail :: String -> m a
We see the familiar: the >> = operator and the return function with the same types, but besides them there is also the >> operator and the fail function. What do they mean?
The fail function is initially a very primitive way of reporting an error. It is called when the >> = operator cannot bind a value of type a to a function of type a -> mb due to matching errors. I do not want to go into the details of this mechanism now, because it is boring; see the documentation on the Haskell website if you need it. In most cases, worry about fail is not necessary.
The >> operator is a little more interesting. He has this type:
(>>) :: m a -> m b -> m b
This operator is a monadic sequence operator. In particular, it is a variant of monadic application (>> = or “bind”), which discards an unpacked value of type a before performing an “action” of type m b. It is defined as follows:
mv1 >> mv2 = mv1 >> = (\ _ -> mv2)
We can see here that any value unpacked from the monadic value mv1 is rejected, and then the final monadic value mv2 is returned. The operator is useful when the type of the unpacked value is (), that is, it is an empty type. The putStrLn function can be considered a good example:
putStrLn :: String -> IO ()
Imagine you want to print two lines, one after the other, with line breaks after each. You can do this:
putStrLn "This is string 1." >> putStrLn "This is string 2."
And why does this work? Let's look at the types:
(putStrLn "This is string 1.") :: IO ()
(putStrLn "This is string 2.") :: IO ()
That is, the >> operator combines two monadic values of type IO () into one resulting monadic value of type IO (). Let's take the >> operator and specialize it for our case:
(>>) :: m a -> m b -> m b
If m is IO, and a and b are (), then we get:
(>>) :: IO () -> IO () -> IO ()
By writing, we can say that, probably, the >> operator performs two “actions” in a row - printing a line.
Now a more complex example. We need to read a line of text from the terminal and print it twice. We can do it like this:
readAndPrintLineTwice :: IO ()
readAndPrintLineTwice = getLine >> = (\ s -> (putStrLn s >> putStrLn s))
Due to the priorities of the operators, the record can be left without brackets:
readAndPrintLineTwice :: IO ()
readAndPrintLineTwice = getLine >> = \ s -> putStrLn s >> putStrLn s
So what does this mean? getLine - monadic value ("action"), which reads a line of text from the terminal. The >> = operator “unpacks” this string from a monadic value and associates it with the name s (because \ s -> putStrLn s >> putStrLn s is a monadic function, the second argument of the >> = operator). Then the line called s is used by the monadic value putStrLn s >> putStrLn s, which prints it two times in succession.
If what you say seems mystic, it is not your fault. Something strange is happening here in the depths, but until I talked about the state monad, I can’t explain it. But now you must be able to trace what is happening, even if you still do not fully understand how it happens.
Right now I'm going to go back a bit and look at the monad laws. They play a large role in using the >> = operator and the return function for each particular monad. After that we will turn to more practical materials.
The Three Laws of Monadism
Many important laws go in groups of three: three mechanical laws of Newton, three laws of thermodynamics, Three Laws of Azimov Robotics, three Kepler laws of planetary motion, and so on and so on. Monads in this do not differ, well, of course, with the exception that the "Three Monad Laws" are more important than anything else. ;-)
For the >> = operator and the return function to be correct for a particular monad, they must have the correct types of this monad. So, for example, the definitions >> = and return for Maybe monad contain its type:
(>> =) :: Maybe a -> (a -> Maybe b) -> Maybe b
return :: a -> Maybe a
And for monads, IOs contain type IO:
(>> =) :: IO a -> (a -> IO b) -> IO b
return :: a -> IO b
However, this is not enough. These functions / operators are also required to satisfy the three “monad laws”. Monad laws are actually very simple; they are designed to ensure that the monadic composition works in a predictable way. First I will give you a “nice” version of the monad laws, and then I will show the (ugly) way, as they are usually described. (Tell me thanks: the “nice” option is much easier to understand.)
Nice version
Here is a nice definition of the three monadic laws expressed in terms of monadic composition (remember that the operator (> =>) is a monadic operator of composition of functions):
1. return> => f == f
2. f> => return == f
3. (f> => g)> => h == f> => (g> => h)
What are these laws telling us?
Laws 1 and 2 say what return should be: this is the unit (neutral element) for the monadic composition of functions (the first rule states that return is the left unit, and the second that the right). In other words, composing the monadic function f and return (in any order) simply returns the function f. Analogs can be considered 0 - a neutral element for the function of adding integers, and 1 - a neutral element for the integer multiplication function; in each of the cases, the neutral element connected to the usual value using the corresponding function will simply return this value back.
Law 3 states that the monadic function of composition is associative: when we want to combine three monadic functions (f, g, h), it does not matter which two we connect first. This is analogous to the fact that addition and multiplication are also associative when applied to integers.
Don't these laws seem vaguely familiar to you? Let us take a look at the corresponding “laws”, which are satisfied by the usual function of composition:
1. id. f == f
2.f. id == f
3. (f. g). h == f. (g. h)
where id is a neutral element, unit. Did you catch the resemblance? The composition of a function with a unit on the left or right will give the same function again, and the composition function is associative. The monadic function of the composition must be associative, and return must be the monadic equivalent of a single function, so that the behavior of the monadic composition is as predictable as the behavior of a regular composition.
What is the meaning of these laws from the point of view of a programmer? Since we want our monads to behave intelligently, our definitions of return and >> = must satisfy these laws. We will soon learn how to verify the definitions of >> = and return. [Note that monadic laws are expressed in terms of the>>> operator, not the >> = operator, but we will see the version using >> =, it is equivalent.
, there is a catch: Haskell does not check monad laws! The only thing that is checked is that the return and >> = definition types are correct. Whether laws are being implemented or not, the programmer must check.
Many people ask, “Why can't Haskell check monadic laws?” The answer is simple: Haskell is not yet powerful enough! In order to get a sufficiently powerful language that proves the correctness of monad laws, you need something like a theorem prover (teorem prover). Proofs of theorems are breathtaking, and they may be the future of programming, but they are much more complex than traditional programming languages. If you're interested, there is a respected proof of Coq theorems, it is available here.. But in Haskell, the programmer must take care that the monad he wrote does not violate monad laws.
Ugly version
The problem with the nice version is that the> => operator is not defined directly in the Monad type class; instead, the >> = operator is defined, and the> => operator is derived from it, as I showed above. So if we restrict the definitions to the >> >> and return operators, we need monadic laws containing only return and >> =. And in this form they are served in most books and documentation on monads in Haskell, despite being less intuitive than shown in the previous section.
In terms of the >> = operator and the return function, the monad laws look like this:
1. return x >> = f == f x
2. mv >> = return == mv
3. (mv >> = f) >> = g == mv >> = (\ x -> (fx >> = g))
where the types of different values are:
mv :: m a
f :: a -> m b
g :: b -> m c
for some types a, b, c and some kind of monad m.
Deriving an ugly version of monad laws from a nice version
Let's have fun and try to deduce an ugly version of monad laws from a nice version. In our calculations, we need the definition of monadic composition, which we examined above:
f> => g = \ x -> (f x >> = g)
Law 1:
return> => f == f
\ x -> (return x >> = f) == \ x -> f x
return x >> = f == f x - QED ("Which was to be proved")
Note that \ x -> fx is the same as just f.
Law 2:
f> => return == f
\ x -> (fx >> = return) == \ x -> fx
fx >> = return == fx
let mv == fx
mv >> = return == mv - QED
Law 3:
(f> => g)> => h == f> => (g> => h)
\ x -> ((f> => g) x >> = h) == \ x -> (fx >> = (g> => h))
(f> => g) x >> = h == f x >> = (g> => h)
(\ y -> (fy >> = g)) x >> = h == fx >> = (\ y -> (gy >> = h))
- Calculate (\ y -> (f y >> = g)) x we get: (f x >> = g)
( fx >> = g) >> = h == fx >> = (\ y -> (gy >> = h))
- Let mv = f x, then:
(mv >> = g) >> = h = = mv >> = (\ y -> (gy >> = h))
- Replace g with f, h with g:
(mv >> = f) >> = g == mv >> = (\ y - > (fy >> = g))
- Replace y with x in the right expression and get:
(mv >> = f) >> = g == mv >> = (\ x -> (f x >> = g)) - QED
In the calculation step (\ y -> (fy >> = g)) x, we simply apply the entire function (\ y -> ...) to the argument x; in this case, y is replaced by the variable x in the function body (it is indicated by the ellipsis (...)), and the function body is returned as a result. In the Lingo functional programming language, this operation is called beta reduction . {1: In this case, we are talking about a section of mathematics called lambda calculus, which describes, among other things, beta reduction.} Beta reduction is the main way to calculate functions. The last step, where y is replaced by x, is correct because the following two functions are correct:
\ x -> f x
\ y -> f y
- this is one and the same (the name of the formal argument does not matter). In the Lingo functional language, we would say that two functions are alpha equivalent . You must have understood the other steps.
What is the idea?
Monad laws can sometimes be used in code, replacing a long expression with a shorter one (for example, instead of return x >> = f, you can simply write fx). However, we will show in the following articles that the main benefit of monad laws is that they allow us to derive definitions of return and >> = for specific monads.
At the end of this article, I want to show you a neat syntactic form of writing, with the help of which the monadic code looks much nicer.
Do notation
Recall the readAndPrintLineTwice function defined above:
readAndPrintLineTwice :: IO ()
readAndPrintLineTwice = getLine >> = \ s -> putStrLn s >> putStrLn s
She has one advantage: it is written in one line. The disadvantage is not the most readable line in the world. Haskell designers noticed that monadic definitions are often difficult to read, and they come up with really nice syntactic sugar that makes definitions more readable.
The basis of this syntactic sugar is the observation that a huge number of operations in the monadic code are written in two forms:
- Form 1.
- mv :: m a
- f :: a -> m b
mv >> = \ x -> mf x
- Form 2.
- mv :: m a
- mv2 :: m b
mv >> mv2
Notation was designed with the intention of making these two forms readable. It starts with the do keyword, followed by some monadic operations. So these two of our examples will be written in do-notation:
- Form 1, do-notation.
do v <- mv
f v
- Form 2, do-notation.
do mv
mv2
In Form 1, the first line means that we take the monadic value mv and “unpack” it into a regular one called v. The second line is just calculating f from v. The result of the string fv is the result of the whole expression.
In Form 2, the monadic value (“action”) mv is “executed” in the first line. The second line “runs” another monadic value (“action”) mv2. Thus, we simply have a notation that concatenates mv and mv2 into a sequence, as the >> operator does.
The Haskell compiler converts a convenient do-notation to a non-do entry for Form 1 and Form 2. This is just a syntax conversion, and the meaning of both entries is identical. In addition, both forms can be mixed in one expression of each of the notations. Example:
- mv :: m a
- v1 :: a
- f :: a -> m b
- v2 :: b
- mv3 :: m c
do
v1 <- mv
v2 <- f v1
mv3
return v2
This is exactly the same as:
mv >> = (\ v1 ->
(f v1 >> = (\ v2 ->
(mv3 >>
(return v2)))))
Or without skokbok:
mv >> = \ v1 ->
f v1 >> = \ v2 ->
mv3 >> return v2
You can imagine that when monadic expressions expand, the do-form remains just as easy to read, while the form without do (also called “Sugared”) often becomes unreadable. That's why do-notation exists. It's great that do-notation works for all monads, not just one.
In addition, you can mix do-notation and sugarless notation in one expression. Like this:
do v1 <- mv
v2 <- f v1
mv3 >> return v2
This is sometimes useful, but can often cause poor code readability.
Let's see how our previous examples will look in do-notation.
-- Считываем строку, затем печатаем ее.
readAndPrintLine :: IO ()
readAndPrintLine =
do
line <- getLine
putStrLn line
-- Печатаем две строки, одну за другой.
-- Не функция.
do
putStrLn "This is string 1."
putStrLn "This is string 2."
-- Считываем строку и дважды ее печатаем.
readAndPrintLineTwice :: IO ()
readAndPrintLineTwice =
do
line <- getLine
putStrLn line
putStrLn line
Here the code is much easier to read thanks to do-notation. Interestingly, it has an additional advantage (or disadvantage, depending on which views you hold): the code in Haskell looks imperative! If we read the code from top to bottom, it looks like an imperative language, which instead of assigning the arrow <-. Let's say readAndPrintLine can be described as follows: “call getLine to read the line that we put in the line variable; then we call putStrLn to print this variable. ”This is definitely not what really happens (for example, line is not a variable), but you can read it that way. For a lot of code that does a lot of input and output, do-notation is a very convenient way to write.
Do notation has other useful properties. For example, you can embed let-expressions and case-expressions in the body of do-notation, which is often convenient. I will not go into details because this is a routine - take any other Haskell tutorial to explore this point.
Next
In the next article, I will start talking about monads, starting with Maybe (the monad for calculations in which an error may occur) and ending with the list monad (for calculations with multiple results).
Content
Part 1: basics
Part 2: functions >> = and return
Part 3: Monadic Laws
Part 4: Maybe monad and list monad