> 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.
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.