From what I understand, Bertram’s version of Prompt and Unimo are based on very similar principles: if you define what is (return v) and what is (m >>= k) where m is an effect basis computation, you can mechanically construct a monad that satisfies all three laws. If you look at the definition of list monad and state monad in Prompt and Unimo (you can find the Unimo paper on my homepage), the resemblance is pretty striking.

Prompt has at least one advantage: the use of continuations makes it possible to package the entire monad-law enforcement mechanism in the Monad instance of (Prompt p), so there is no way to break it like how Nils broke Unimo. It would be interesting to try the Unimo-transformer construction on Prompt; I think it will work with very little modification.

]]>Prompt looks interesting as well. These frameworks are all based on similar ideas, the main question is how usable they are; compared to each other, compared to implementing monads from scratch, and compared to using a monad transformer library.

More monads? There may be some differences in raw expressibility (see the last paragraph of my post). But if you restrict yourself to those definitions which are “elegant” or “idiomatic” (in some sense), then the differences may be more interesting.

]]>1. Violation of right-unit law: Nils demonstrated that if you manually pattern match against Unit and Bind instead of consistently use observe_monad, you can construct a Unimo definition that does not observe the right-unit law.

This is a notable discovery; however Nils’ description “the right unit monad law is not actually satisfied in general”, while technically correct, seems to imply that Unimo has nothing to offer in that department. I feel that is a little unfair. Yes, if you go out of your way to defeat the monad-law enforcement mechanisms in Unimo, you can succeed. But for everyone else, Unimo remains a useful tool in constructing monads that abide by all three laws.

2. Termination of run_list: Section 3.3 states that Case 4 in run_list eliminates two data constructors without adding any, and Nils observed that the function application (k v) can introduce an arbitrary number of data constructors.

I agree with Nils: the text in the paper does not properly establish the termination of run_list. The big problem lies in what qualifies as a “finite Plus computation” to run_list: without clearly defining how to count the number of constructors in a Plus computation, we cannot make arguments using the count. Therefore, I think the text helps to give readers a good intuition on the behavior of run_list, but that is probably where its usefulness ends.

]]>For some examples, take a look at http://hpaste.org/5974

The original formulation is here:

http://www.haskell.org/pipermail/haskell-cafe/2007-November/034830.html

(it suffers from the same left-binding explosion as the free monad)

Bertram Felgenhauer re-interpreted and generalized the concept here:

http://www.haskell.org/pipermail/haskell-cafe/2008-January/038301.html

(which also solved the quadratic blowup behavior).

This code is all available at http://ryani.freeshell.org/haskell/prompt/

]]>