Re: [Haskell-cafe] Pearl! I just proved theorem about impossibility of monad transformer for parsing with (1) unbiased choice and (2) ambiguity checking before running embedded monadic action (also, I THREAT I will create another parsing lib)

Hi. Thanks for answer! I already wrote arrow parsing lib. I will publish it when I was done. Also, you forgot to add haskell-cafe@haskell.org to CC. Понедельник, 21 июня 2021, 21:53 +03:00 от "Olaf Klinke" :

Dear Askar,

your theorem is convincing. While a counterexample is sufficient for a rigorous proof, I'll try to add some mathematical theory to this. Many monad transformers are of the form FooT m a = g (m (f a)) where (f,g) is an adjoint pair of functors. The Kleisli lifting operation (=<<) for such a composite monad uses the Kleisli lifting of m. For your application that means that you can not use monadic actions of your monad transformer without executing the monadic actions of the transformed monad m. I conjecture that any transformer FooT with the property that FooT m is a monad provided m is a monad necessarily runs m-actions.

A transformer that does not require m to be a monad is the continuation transformer ContT m r a = (a -> m r) -> m r. However, for this transformer the lift operation is interdefinable with an operation m (m r) -> m r so it seems that at least lift will run m-actions.

As Chris Smith pointed out, this does not rule out that Applicative- style parsing code may be able to prevent executing the m-actions.

Olaf

== Askar Safin http://safinaskar.com https://sr.ht/~safinaskar https://github.com/safinaskar