For the purpose of verifying Haskell programs in Coq, we build on previous work that demonstrates how to reason about existing Haskell programs by translating them into monadic Coq programs. A model of Haskell programs in Coq that is polymorphic over an arbitrary monad is not accepted by Coq’s termination checker. Therefore, instead of a model that is generic over the monad, we use a concrete monad instance, namely the free monad, to model various kinds of effects. This model allows proofs that are generic over the concrete kind of effect.

In this paper we consider implicit effects that may occur in Haskell, namely partiality, errors, and tracing, in detail. We observe that, while proving propositions that hold for all kinds of effects is attractive, not all propositions of interest hold for all kinds of effects. Some propositions fail for certain effects because the common monadic translation models call-by-name and not call-by-need. As modeling call-by-need makes proofs more complex and is not necessary for a variety of effects, we identify a specific class of effects for which we cannot distinguish between call-by-name and call-by-need denotationally. Using this class of effects we can prove propositions for all effects that do not require a model of call-by-need. Besides specifying this class we show how various Haskell language features that are related to implicit effects can be modeled.