In the functional programming language Haskell IO is encapsulated in the IO monad. But how do we reason about programs performing IO? How can we integrate IO into a language with dependent types, where IO may appear within the types? I am suggesting to use functional programs to specify effects and sketch how this can be applied to members of Simon Peyton Jones' awkward squad (references, stream IO and concurrency). I'll also look at some more unusual candidates: partiality (non termination as an effect) and quantum computing.

This is based on joint work with my student Wouter Swierstra, the material on partiality is based on joint work with Venanzio Capretta and Tarmo Uustalu. A draft paper is available from my webpage.