Journal de Chaource's Journal
[Most Recent Entries]
[Calendar View]
Sunday, March 4th, 2018
| Time |
Event |
| 7:49a |
The ubiquitous premonads: The simplest way to formulate monad laws
Monad laws are usually formulated in terms of the `bind` function that has 3 laws together with the `return` function. However, this formulation is both unintuitive (it's hard to remember the laws) and too strong: the `return` function is not necessary in most practical cases.
Consider the `join` function instead. The `join` has the type `M (M a) -> M a` and needs to be a natural transformation.
It turns out that this single requirement (what I earlier called "pre-monadic") is actually sufficient for practical purposes. There is no need to introduce `return` or to require any more laws.
The associativity law for `join` states that reducing `M (M (M a))` to `M (M a)` and then to `M a` gives the same results whether we first reduce the outer pair of `M`'s or the inner pair.
fmap join . join = join . join
I always thought that this was a separate law.
However, now it seems that it is a consequence of naturality for `join`:
fmap h . join = join . h
I will need to check some examples to become fully convinced, but so far this seems to be correct.
If so, this significantly simplifies checking the laws for monads. It is quite cumbersome to check the associativity law because of the (usually) complicated type `M (M (M a))`. On the other hand, naturality is perfectly obvious in most cases.
In my previous posts I have found that a large class of functors admits a natural transformation with the type signature of `join`. I thought that I would have to check associativity additionally. Now it appears that it is not necessary.
For instance, all polynomial functors admit a natural transformation with the type signature of `join` (the type can be inhabited). It follows that all polynomial functors are pre-monadic, with the associativity law holding automatically. It's a great simplification that the associativity law does not need to be proved.
Update: This is a mistake! Associativity does not follow from naturality. I mixed up the types of functions in the naturality property. It must be fmap (fmap h) . join = join . fmap h; also I found a counterexample where naturality holds but associativity does not.
The reason for not including `return` is that, in many practical cases, `return` is not directly useful for coding. Most monads have several additional constructors and methods necessary for using them; having just `return` would be far insufficient.
For instance, the `List` monad has constructors from any number of values (not just one), and also methods such as `append` or `concat`. Having `return` for a `List` means constructing a list of one element only; this would be insufficient for practical use of `List`.
Any "validation-like" monad has constructors for success and failure; having only `return` as a constructor for success values would be insufficient for practical use.
Therefore, insisting on `return` but omitting any other constructors does not serve much practical purpose. It is perhaps mathematically more elegant because it makes connection with monoids, but that's about it.
A proper premonad that has only `join` but no `return` is related to a Kleisli semigroupoid (as opposed to a Kleisli category for full monads).
I found some use cases for premonads. The simplest one is the `Writer` premonad.
The standard `Writer` monad is the type constructor `W m a = (m, a)`, considered as a functor in `a`, where `m` is a monoid type. Now, replace monoid with semigroup. Then we can still define `join` as before, with all properties holding since `join` is a natural transformation in `a`:
join (m1, (m2, a)) = (m1 `combine` m2, a)
The `combine` method must obey semigroup laws but may not be a monoid if it does not admit an identity element. A simple example of the `combine` method that gives a semigroup but not a monoid is
combine1 m1 m2 = m1
or
combine2 m1 m2 = m2
It is easy to see that no identity element can be found here.
A use case for this is a chain of computations that need to trace the time spent in the entire chain.
The values `m` represent timestamps, and "combining" them using `combine1` or `combine2` will trace the initial time or the final time. This is certainly a useful example of using a premonad that cannot be made into a full monad. | | 9:02p |
Что нужно намъ знать о вѣрѣ истинной и о людяхъ такъ называемыхъ "ученыхъ" ...въ послѣднѣе время все болѣе и болѣе распространялось и распространяется грубое суевѣрiе, въ много разъ вреднѣйшее, чѣмъ всѣ суевѣрiя древности, суевѣрiе о томъ, что религiя вообще есть нѣчто ненужное, отжитое, что безъ религiи человѣчество можетъ жить разумной жизнью.
Суевѣрiе это особенно свойственно людямъ ограниченнымъ. А какъ таковыхъ большинство людей въ наше время, то грубое суевѣрiе это все болѣе и болѣе распространяется. Люди эти, имѣя въ виду самыя извращенiя религiи, воображаютъ, что религiя вообще есть нѣчто отсталое, пережитое человѣчествомъ, и что теперь люди узнали, что они могутъ жить безъ религiи, то-есть безъ отвѣта на вопросъ: зачѣмъ живутъ люди, и чѣмъ имъ, какъ разумнымъ существамъ, надо руководиться.
Грубое суевѣрiе это распространяется преимущественно людьми, такъ называемыми учеными, то-есть людьми особенно ограниченными и потерявшими способность самобытнаго, разумнаго мышленiя, вслѣдствiе постояннаго изученiя чужихъ мыслей и занятiя самыми праздными и ненужными вопросами. Особенно же легко и охотно воспринимается это суевѣрiе отупѣвшими отъ машинной работы городскими фабричными рабочими, количество которыхъ становится все больше и больше, въ самыхъ считающихся просвѣщенными, то-есть въ сущности самыхъ отсталыхъ и извращенныхъ людяхъ нашаго времени.
...
Людямъ нашаго времени и мiра не нужно, какъ это думаютъ ограниченные и легкомысленные люди, такъ называемые ученые, придумывать какiя-то новыя основы жизни, могущiя соединить всѣхъ людей, а нужно только откинуть всѣ тѣ извращенiя, которыя скрываютъ отъ насъ истинную вѣру, и эта вѣра, единая со всѣми разумными основами вѣръ всего человѣчества, откроется передъ нами во всемъ своемъ не только величiи, но всѣй обязательности своей для всякаго человѣка, обладающаго разумомъ.Гр. Л. Н. Толстой, Почему христiанскiе народы вообще и въ особенности русскiй находятся теперь въ бѣдственномъ положенiи. http://az.lib.ru/t/tolstoj_lew_nikolaewich/text_0690.shtml...a gross superstition is lately spreading further and further, a superstition many times more harmful than all ancient superstitions, the superstition that religion in general is something unnecessary, outdated, and that mankind can live a reasonable life without a religion.
This superstition is particularly inherent to narrow-minded people. And because they are the majority of people in our time, this gross superstition is becoming more and more widely spread. These people, having in mind the very perversions of religion, imagine that religion in general is something outdated, outlived by humanity, and that now people have learned that they can live without religion, i.e. without answer to the question: why do people live, and what they, as rational beings, should be guided by.
This gross superstition is spread mainly by so-called scientists, i.e. by people especially narrow minded and having lost their facility for original, reasonable thinking as a result of never-ending studying of each other's thoughts and of engaging with the most idle and irrelevant questions. But especially easily and readily this superstition is perceived by city-dwelling factory workers stupefied by automated production lines, whose number is growing more and more, -- that is, in people considered to be the most enlightened, but who are in fact the most regressive and corrupt people of our time.
...
Our world and people of our time do not need, as the narrow-minded and frivolous people think, - the so-called scientists, -- to invent any new foundations of social life that can connect all people. They need to throw away all the perversions, which hide from us the true faith, and this faith, unified with all the reasonable fundamentals of faiths of mankind, will open before us in all its, not just grandeur, but in all its compulsion for any person possessing the reason.http://www.earthlyfireflies.org/why-the-christian-people-are-in-such-distress-now-by-lev-tolstoy/И еще о "людяхъ, такъ называемыхъ ученыхъ": Многiе читатели будутъ непрiятно поражены моими словами, однако я считаю своимъ долгомъ высказаться. Книгъ подобнаго рода мнѣ еще не приходилось писать; а такъ какъ среди математиковъ не принято предварять свои труды излiянiями на личныя темы, раньше я обходился безъ такихъ излiянiй. По не зависящимъ отъ меня обстоятельствамъ я оказался вовлеченнымъ въ событiя, которыя собираюсь тутъ описать. Причины, побудившiя меня предварить изложенiе чемъ-то вродѣ исповѣди, станутъ ясны позже.
Главенствующими чертами своего характера я считаю трусость, злобность и высокомѣрiе. Такъ вышло, что эта троица имѣла къ своимъ услугамъ кое-какой талантъ, который завуалировалъ ее и, по видимости, переиначилъ; а помогъ въ этомъ умъ, одно изъ самыхъ удобныхъ орудiй для маскировки, въ случаѣ надобности, нашихъ природныхъ изъяновъ. Вотъ уже сорокъ съ лишнимъ лѣтъ я веду себя какъ человѣкъ отзывчивый и скромный, чуждый профессiональной спеси - потому что я очень долго и упорно прiучалъ себя къ этому. Съ ранняго дѣтства, сколько я себя помню, мною руководило стремленiе къ злу - о чемъ я, разумѣется, не догадывался.Станиславъ Лемъ. "Голосъ неба" http://librebook.me/glas_gospoda/vol1/2 | | 10:25p |
Monoids and co-monoids
The writer monad, `W a = (a, w)` usually assumes a monoid as its fixed type `w`. The reader monad, `R a = r -> a`, does not assume any properties for its fixed type `r`. I realized that this asymmetry is an illusion. In fact, the reader monad assumes a co-monoid for `r`.
A type `w` is a monoid if there exist two methods, `unit: 1 -> w` and `combine: (w, w) -> w`. The `combine` operation must be associative. The unit must be the identity element for the `combine` operation.
Inverting the arrow directions, we obtain the definition of co-monoid:
A type `r` is a co-monoid if there exist two methods, `counit: r -> 1` and `expand: r -> (r, r)`. The `expand` operation must be co-associative.
The co-associativity means that fst (expand (snd (expand r))) = snd( expand (fst (expand r))).
In other words, `expand` is a function product made of two functions, `expand1 : r -> r` and `expand2 : r -> r`. Co-associativity means that these two functions must commute.
Note that the `counit` always exists and even is unique because `1` is the terminal object in the category, which always exists as far as functional programming is concerned. So we can just omit `counit` from the definition of the co-monoid. The result is the definition of co-semigroup. So, co-semigroups and co-monoids are the same thing for the purposes of functional programming.
The reader monad is defined via the `join` method:
`join: (r -> (r -> a)) -> r -> a`
`join rra = r -> rra r r`
To implement `join`, we need two copies of `r`. Clearly, we are tacitly using the `expand` operation here. The trivial definition `expand r = (r, r)` is a co-monoid for any type r. For this reason, we did not notice that a co-monoid is actually being used. Making this explicit, we find the definition of `join` like this:
`join rra = r -> (uncurry rra) (expand r)`
Now, the writer monad can be weakened to the writer pre-monad, by omitting the `unit` operation and reducing the monoid W to a semigroup. No such weakening is necessary for the reader monad, because co-monoids and co-semigroups are the same.
We have seen that any type `r` is trivially a co-monoid. What are nontrivial examples of generic co-monoid types?
I found two examples so far.
1. Consider the triple `(t, t, t)` of the same type `t`. The `expand` operation will copy the middle value towards the middle:
expand (x, y, z) = ((x, y, y), (y, y, z))
Co-associativity is achieved because any composition of `expand` will always yield a structure of the form (x, y, y), (y, y, y), ..., (y, y, y), (y, y, z).
The two functions are `expand1 (x,y,z) = (x, y, y)` and `expand2 (x,y,z) = (y, y, z)`.
The composition of `expand1` and `expand2` in any order gives `(y, y, y)`, which shows co-associativity of `expand`.
2. Consider a list type `List t` and define `expand` as follows:
expand [] = ([], [])
expand [x] = ([], [])
expand [x, ..., y] = ([x, ...], [..., y])
The composition of `expand1` and `expand2` gives the middle piece `...` from the initial list, or the empty list if it's too short.
These examples are similar because they operate on the "accordion" principle: the data type has a "middle piece" that is being expanded by copying. Are there other examples of nontrivial co-monoids that operate in a different way? |
|