LambdaConf's video: Nihil Shah- Environmental Dependencies as Coeffects- C 2019

Effects modify the environment of an executed program, which includes anything from writing a file to launching missiles. Thankfully, monads help us reason about side effects. But what about dependencies on the environment? I’ll show how these coeffects can be modeled, dually, as comonads. Computational side effects are the consequences of a computation on the environment that are not the output of the computation. Exceptions, changing global state, modifying a file system, and launching missiles all fall into this category of “side effects.” Side effects make it difficult to reason about and debug code. Thankfully, in 1991, Eugenio Moggi’s seminal paper, “Notions of Computation and Monads” showed how side effects could be reasoned about and even composed together using the abstraction called “monads.” Monads were baked into Haskell, and the rest is history. But what about coeffects? “Coeffects,” informally dual to effects, are the dependencies a computation has on the environment that are not the input of the computation. Delightfully, just as effects can be modeled using monads, coeffects can be modeled using indexed comonads. This term was first coined by Thomas Petrieck and others in his PhD thesis. In this talk, I give a gentle introduction to the definition of coeffects, and how they are modeled using indexed comonads, and then show how they can be used to give better type safety to your programs. Examples of coeffects include API versioning, implicit parameters, data flow computations, and bounded resource management.