Hacker News new | past | comments | ask | show | jobs | submit login

Sure the values are. Any function `a -> b -> c` can be lifted into a function `m a -> m b -> m c` for any Monad. That's (part of) the exact thing that bind buys you.

"Escaping" from a monad is an artifact of a bad intuition. There's no reason for a monad (m a) to "contain" values a and thus no reason to believe that they can be removed.

Even Maybe is a sufficient model of this. I can make a whole big compositional pipeline with all kinds of compositions at the value level, but if my inputs are Nothing then there won't be anything to "pull out" at the end.

Ultimately, "monadic worlds" is a good intuition. Just realize that your monadic world may be a strange one when you pull it back into "your" world---the interpretation may not be obvious, it may demand something of you, and it may not look very much like the "values" you felt like you were playing around with.




Let's take a simple, quotidian example: logging and errors. I write functions that produce logs and may generate errors. If I were using monads, I'd have a log monad and an error monad. For logs, my functions would produce a value and a list of log messages. The monad would combine the list of messages. For errors, my functions return an OK and a value, or an error, and the monad short-circuits errors. Now I write functions that might produce both logs and errors. How do the two monads compose?


Of course there are two ways. The problem is that there is not enough information in the mere product of the two algebras to indicate what proper behavior is.

If you don't mind deferring the definition of "correct" to the interpreter writer then that intentional choice is captured by

    (MonadWriter Log m, MonadExcept m) => m a
If you want more controls then we need to start specifying laws. For instance, the following law distinguishes between the two instances

    throwError e >> m == throwError e
and this now clearly indicates that EitherT e (WriterT Log) is wrong while WriterT Log (Either e) is fine.

So how do we specify what additional laws are needed to cut down the free product of the effectful languages? Dunno, that's a hard one. You could clearly do it using dependent types, but that's still today very expensive.

But given that we literally lack proper information to make a choice it's very important that all of those choices are allowable. It's my position that there is no meaningful default. It's also my position that the `mtl` style free products are perfectly acceptable.


I would even go so far as to suggest that there are applications where we want the other ordering of these two.


Me too!




Applications are open for YC Winter 2020

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: