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

[Chris Smith]

On Fri, Jun 11, 2021 at 8:24 PM Askar Safin <safinaskar at mail.ru> wrote:

> So, we need this function instead:
>
> fromEither :: Parser (Either String a) -> Parser a

Now we can write this:
> -----
> q :: Parser Int
> q = fromEither $ do { -- applicative do
>   char '(';
>   a <- p;
>   char '/';
>   b <- p;
>   char ')';
>   pure $ do { -- normal monadic do
>     when (b == 0) $ Left "division by zero";
>     return $ a / b;
>   };
> }
> ------
> Yay! Now everything works with Applicative. Moreover, it seems we can
> embed arbitrary Monad this way. But this is ugly. Because:
> 1. We use two-level do. One applicative and one monadic
> 2. We need to prepend "fromEither" before each parser, in which we plan to
> fail with error messages.
>

Indeed.  You can see this as a clear expression of the two-phase nature of
the problem at hand.  You want monadic effects (such as Either String) to
be executed for type checking, but not during parsing, so that you can
check for an ambiguous parse prior to performing type checking.  Then you
must have a separation between non-determinism in parsing (the Parser
functor) and type checking failures (the nested Either monad).  This
appears in your types and code, by saying that a type checking failure
counts as a successful parse, whose associated value is an error from the
type checker.

So, I think arrow parsing will be more natural
>

That's an interesting hypothesis.  I'm not familiar with any arrow-based
parsing libraries, so if you try and find a better way to express this
there, I hope you'll share your findings with us.

Chris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210612/b42453c4/attachment.html>