Module Preface_stdlib.Approximation

Over and Under allows Static analysis of selective functors with over-approximation.(mentioned in Selective Applicative Functor by A. Mokhov, G. Lukyanov, S. Marlow and J. Dimino.

Over approximation

The selective functor Over can be used for computing a list of all effects embedded in a computation, i.e. an "over-approximation" of the effects that will actually occur. This is achieved by keeping track of effects in both arguments of the select operator.

Under approximation

The selective functor Under discards the second argument of select, and therefore computes an "under-approximation", i.e. a list of effects that are guaranteed to occur.