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.
> I haven't claimed that equational reasoning is limited to pure languages
Sorry, I may have read that into your comment.
> the code itself needs to be pure
But that's also incorrect. Just because you can't replace an effectful computation with a value doesn't mean you can't reason equationally. You can also have benign effects that are unobservable, for example, memoization.
> Not sure how to parse that
I meant that functions with effects are just functions with computation type at the meta level. I.e. there's nothing more "mathematical" about only allowing nontermination in your language. It's just the simplest case.
> 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.