nikita-volkov / refined

Refinement types with static checking
http://hackage.haskell.org/package/refined
MIT License
183 stars 31 forks source link

RefineT revision #53

Closed nikita-volkov closed 4 years ago

nikita-volkov commented 4 years ago

@chessai Thanks for your hard work on the project! It's great to see how much progress has been made. I've taken some time to review a part of what the library has evolved into. Let's discuss it.

As I understand the RefineT abstraction mostly exists for the purpose of defining the following method:

validate :: Monad m => p -> x -> RefineT m ()

Since the signature requires the definition to be applicable to every monad, there is no actual use for RefineT being a transformer in the implementation of validate. This renders validate essentially the following:

validate :: p -> x -> Either RefineException ()

So it seems like we have a redundant abstraction over there. Abstractions extend the complexity of the API. More so, we also involve an advanced concept of monad transformers, thus immediately raising the bar for the potential audience of the library. Those are serious sacrifices which we seemingly could avoid, but what's the gain? Am I missing something?

Going further, if we're restricting a monad to always return a unit, then it's a sign that monad is too powerful for us. What we actually need is a monoid. E.g., Alt over Maybe:

validate :: p -> x -> Alt Maybe RefineException

That'll make our validate more correct, keeping the composability, just with the monoidal interface instead of monadic.

However, I'd also like to argue that we don't actually need it to be composable. All we need is to provide a way for the user to implement a predicate. Imposing a particular composition method wouldn't be wise. Some people program with combinators over abstractions, others prefer pattern-matching. Also avoiding another advanced concept (which Alt is) would be beneficial for the UX as well. That brings us to the following definition:

validate :: p -> x -> Maybe RefineException

Which ironically is not much different from what we've had in the first version of the library, but I hope you can now see that it has a reasoning behind.

Those, who want to compose with Alt are still able to using Alt/getAlt. All the current refine* functions can still be implemented in terms of validate.

chessai commented 4 years ago

Over the last year or so I have also come to dislike transformers in most APIs exposed to the end user. People can always hoist Maybe/Either etc. as needed. Your points about having to work in any Monad and also having to return unit are exactly issues with this code I've come to see since. Also, I think most people don't even use RefineT/validate except to implement instances, but instead refine*. This definitely speaks a lot to their usefulness.

All that to say, I agree, except for one small bit: I prefer Either ErrorType () over Maybe ErrorType, since it is easier to follow the convention that Nothing corresponds to failure, which I find helps in reasoning. YMMV. Additionally, you can hoist Either ErrorType () into ExceptT, but i don't see the point of hoisting Maybe RefineException into MaybeT

chessai commented 4 years ago

Though with Either, you do lose the Alt extension, which I don't see a need for other than some short-circuiting fold that could also be achieved with reifyPredicate. Maybe you had some prior thoughts about Alt

nikita-volkov commented 4 years ago

The point of validate is not about being used directly, but about providing minimal means necessary for other utilities to be derived. And it appears that a Maybe-based implementation is enough. All the functions of the refine* family can be derived from it.

I understand your itch to express validate with Either or a similar type. I've even gone thru that stage in the beginnings of this project myself. After all, we're dealing with errors here and this is the type we're used to seeing in functions that may fail, but the thing is that this is not the kind of a function we're dealing with.

Either or Except are about representing failure as a side effect of getting a result. Specifying () for the result means that we don't produce a result and only care about the side effect. That means that Either is too powerful for our case, and that means that there must be something less powerful that fits our case.

Equating the meaning of Nothing to "failure" sets a false premise. Maybe is only about presence/absense of something. There is no failure in something being absent. You may interpret it as such in a particular context, but not all of them. E.g., consider a context of a lookup operation on a map: is it a failure if it doesn't find an element? No, the element is just not in the map and it's just as expected as it being there. Is it a failure if a user doesn't supply an optional parameter? No.

Same applies to validate if you consider its purpose as finding an error in the value: maybe there is an error and maybe not. And that's actually all we're doing in validate: finding an error, which is a perfectly normal operation. After all the whole library is about helping users find errors.

I believe that confusion can be resolved by adding a documentation to validate explaining its purpose.