> that is as ridiculous as saying "the reduction of `(λx.x)4` is an effect". What I'd do is consider the use of recursion to put your computation in a partiali

> that is as ridiculous as saying "the reduction of `(λx.x)4` is an effect". What I'd do is consider the use of recursion to put your computation in a partiality monad. The identity function isn't recursive, so `(λx.x)4` is a pure computation. I'd also require a positivity check on recursive datatypes, to prevent users from sneaking nontermination into pure functions via datatype constructors. > Non-termination is a property of a computation, not something that a program does to the outside world. Non-termination gets in the way of producing a result, so it's an effect. > There's nothing wrong with letting a computer churn away forever trying to reduce a divergent expression (with no effects!) I wouldn't call it “wrong” either, because effects aren't intrinsically “wrong”.