# Dependent Types and Algebraic Effects

We can specify notions of computational effect by giving signatures of operations together with their equational theories, inducing an initial monadic characterisation of effectful computation. I'll sketch what happens when we give the same sort of treatment to effects in a dependently typed setting, where sets can be indexed over values in some way abstracting "states of the world". By contrast with Bob Atkey's indexed monads over ordinary sets, I'll work with ordinary monads over indexed sets, which turn out to be old and dear logical friends seen through Curry-Howard spectacles. Signatures of operations specify their behaviour relative to "states of the world". But what happens to the equational theories? How much of the meaning of operations might be carried by the equational theory and how much by indexing in the signature? I wish I knew. Let's explore.