This is (IMO) very similar in use-case to Idris' bang-notation. I'll give a brief summary of what that is and then explain the pros/cons that I see between them. In Idris the do notation has the added notation that do return $ !a + !b would desugar to do a' <- a b' <- b return $ a' + b' So !a unwraps a higher up and then uses the unwrapped version. Thus if you want to apply a function to apply a function to some wrapped and some unwrapped values: do return $ f !a b !c !d Pros/Cons: - Idris notation is (IMO) more visually appealing. - In particular, it puts the information about which arguments are lifted next to the arguments themselves, which matches our intuition about what's going on - While it matches our intuition, it does *not* match what's actually going on, so that's a con. - Idris notation can lift things more than once: do return $ f !!a !b !!!!c - Idris notation is syntactic sugar, not a first-class operator - So that means no currying, no passing it in as an argument, etc. (though with lambdas this is not as bad as it otherwise would be) - Idris notation is for monads, so it would not work for things that are applicative but not monads (though I'm not entirely sure what falls into this category) What do you y'all think? Do they operate in different enough spaces that they should both exist (like applicatives and moands), or is one clearly better? --Taeer