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 =
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
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.
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).
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
(except :: Except e'), you get a row that is equal to
(except :: Except e' | r)—or, if you prefer,
(except :: Except e') catenated with
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 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.
Thank you @rhendric! Your explanation cleared a lot of stuff up for me.