Alex Rozenshteyn wrote:
I also found myself thinking about list as a monad in terms of this discussion. I think it's an interesting case: it's pure, but it doesn't really make sense to "come out of it". Head, indexing, and last all break out of it, but none of them can be the default, and all of them require you to consider it as something more than its monad-ness.
The proper monad for nondeterminism is a set of values. If we think of the machine as a nondeterministic automaton, then this set is the set of current states in the machine. The bind operation represents taking a step (or multiple steps) in the automaton. If we generalize this to a weighted set then we get a distribution monad. This corresponds to current states in a weighted nondeterministic automaton. In the limit case our weights are unit, in which case this is isomorphic to the nondeterminism monad. The next interesting step is discrete weights (which, in this case, is isomorphic to using a multiset), corresponding to counts of current positions in a nondeterministic automaton. If we allow continuous weights, then this brings us over towards probability theory, hence calling it the "distribution" monad. If we generalize this to a (weighted) set of values annotated by the history of choices leading to their derivation, then we would get a path/proof (distribution) monad. This corresponds to the current set of (weighted) *paths* through a (weighted) nondeterministic automaton. The bind operation represents extending the paths. If we erase the histories in the set, then we get a multiset of values, which is why this is different from the distribution monad. Generalizing this further, We can also think of proof theoretic systems as automata which allow hyperarcs (i.e., arrows with multiple inputs). In this case, the histories in the path monad become trees instead of just linear chains. These histories are the proof trees for their values. ... All of these monads have natural ways of exiting them. Set-theoretic operations generally make sense as corresponding operations on the underlying automata, though there may be a few that don't. Unfortunately, the list monad isn't any of these. It's closest to the distribution monad with discrete weights, since lists are close to multisets. However, lists have additional structure, namely they are ordered multisets (not ordered weighted sets), and the ordering has nothing to do with the type of the values. This ordering is why they have so many other weird ways of being manipulated. While lists form a perfectly good monad, they don't have any clean and elegant translation into automata theory that I can think of. -- Live well, ~wren