I haven't claimed that equational reasoning is limited to pure languages, that's more a property of the code, rather than the language. But you can only achieve equational reasoning with referential transparency and that means the code itself needs to be pure. TFA does not show pure code.

> Effectful functions, as you probably are aware, are just functions of type A -> T B

Not sure how to parse that. But if T in your example is meant to be some IO type, then it is pure along with any transformations on it, until you do unsafePerformIO or something equivalent and you only need to do that once, at the end of the program.