In the Idris language, one best practice is to relegate to the outer shell not only IO effects, but also "partiality"—in the sense of computations that might en

In the Idris language, one best practice is to relegate to the outer shell not only IO effects, but also "partiality"—in the sense of computations that might enter an unproductive infinite loop. (In Haskell, one way of getting into unproductive infinite loops is by mistakenly asking "parse elements until the first failure" to a parser combinator that can always succeed without consuming input.) The ideal is that the core of the application should be both pure and total, purity and totality being tracked by the type system. In fact, one can often relegate partiality to a single function of the outer shell.