[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)

[Askar Safin]

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 at haskell.org to CC.

Понедельник, 21 июня 2021, 21:53 +03:00 от "Olaf Klinke" <olf at aatal-apotheke.de>:
> 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