I’m trying to convert a project from mtl (mostly ExceptT) to purescript-run. The main thing I’m missing is the purescript-run version of withExceptT. I think I’ve got a working version that I wrote myself (sorry for all the extra annotations, it was a bit tough for me to wrap my head around)
withExcept :: ∀ e e' a r.
Union r (except :: Except e') (except :: Except e' | r) =>
(e -> e') -> Run (EXCEPT e + r) a -> Run (EXCEPT e' + r) a
withExcept fn r =
let
x = runExcept r :: Run r (Either e a)
y = lmap fn <$> x :: Run r (Either e' a)
z = expand y :: Run (EXCEPT e' + r) (Either e' a)
in z >>= rethrow
which compiles, but what I’m confused about is why the compiler demands this
Union r (except :: Except e') (except :: Except e' | r) constraint. That seems like that’s just part of the definition of how rows work. Whenever I try to use withExcept, it complains about the same missing Union constraint until I add it to whatever function I’m calling withExcept from, so the ergonomics are really terrible.
Of course if there’s just another way to get a withExcept function that bypasses this altogether, having that function is my real goal, so I wouldn’t need to understand the Union constraint.
The key thing to understand here is that rows are not unordered. Think of a row as like a Map String (Array k)—for any two distinct labels, it doesn’t matter in which order they appear in the row. But the compiler will keep track of the order of two instances of the same label. Union appends one row to the other in a way that respects this ordering.
So Union r (except :: Except e') (except :: Except e' | r) is only a tautology if the label except doesn’t appear in r. You could have Union (except :: Array) (except :: Except e') (except :: Array, except :: Except e'), and (except :: Array, except :: Except e') is not the same as (except :: Except e' | (except :: Array)) = (except :: Except e', except :: Array).
2 Likes
Oh wow, that’s a great insight! Thanks for the help in understanding. I did absolutely think that rows were unordered. That does lead me to several more questions though.
Would it be fair to say that if I flipped the order to
Union (except :: Except e') r (except :: Except e' | r), it is always a tautology? And can you help me develop an intuition of what
Union r (except :: Except e') (except :: Except e' | r) means then? Is that essentially going to end up meaning the same thing as Lacks "except" r? Or is it still possible for that Union to hold if r does contain the label "except"? And if it can still hold, I don’t really know what the Union constraint is really saying…
Yes, and the compiler should be able to provide you with such an instance any time it’s needed.
It means precisely what it says: that if you catenate r and (except :: Except e'), you get a row that is equal to (except :: Except e' | r)—or, if you prefer, (except :: Except e') catenated with r.
It is still possible for that Union to hold for such an r, and it’s a good puzzle to think about under what conditions it’s possible!
Click to reveal answer
The constraint will hold as long as every occurrence of except in r is Except e'. In that case, and only in that case, appending another Except e' to the back or prepending it to the front doesn’t make a difference.
2 Likes
Thank you @rhendric! Your explanation cleared a lot of stuff up for me.