Monads are a notion from category theory that is very powerful with many applications. Monads can formalise and generalise both term substitutions as well as computational effects.