by Dan R. Ghica
The interaction between (pure) computation and the physical world happens in two ways. The computation may act upon the world, which is usually called an effect, which is managed using the well known mechanism of monads in the type system of the programming language. But the computation may also require a resource, which is by symmetry called a co-effect, which is managed the less well known mechanism of co-monads in the type system. This talk is an informal tour of the subject area, with particular emphasis on the ! monad of linear types (which indicates that an argument to a function !A⊸B may be reused or discarded) and its elaborations to bounded linear types and generalised resource types, and their applications to high-level synthesis.

Talk was given on Sep 24 2020.

Thursday Tech Talk: Coeffects (resource management through types) / Huawei-Edinburgh Joint Lab by blogadmin is licensed under a Creative Commons Attribution CC BY 3.0