There are many binary infix operators in first-class-families like ++ that are hard to use since they expect evaluated types, but most of the time the types will be wrapped in Exp. Are there “lifted” versions of these operators that can use types wrapped in Exp? If not, why?
Also, is first-class-families something that should still be used?
You might want to know about phadej’s defun library, which achieves defunctionalization with a slightly different design. Neither is more expressive than the other, as far as I understand.
Actually, I think I probably should have said LiftM2 (++). But that cannot be used as an infix operator (without a further binding, say type (.++) = LiftM2 (++)).