  We extend intersection types to a computational $\lambda$-calculus with
algebraic operations \`a la Plotkin and Power. We achieve this by considering
monadic intersections, whereby computational effects appear not only in the
operational semantics, but also in the type system. Since in the effectful
setting termination is not anymore the only property of interest, we want to
analyze the interactive behavior of typed programs with the environment.
Indeed, our type system is able to characterize the natural notion of
observation, both in the finite and in the infinitary setting, and for a wide
class of effects, such as output, cost, pure and probabilistic nondeterminism,
and combinations thereof. The main technical tool is a novel combination of
syntactic techniques with abstract relational reasoning, which allows us to
lift all the required notions, e.g. of typability and logical relation, to the
monadic setting.
