effectful copy-discard do-notation Effectful copy-discard from a strong promonad References. Premonoidal Categories and a Graphical View of Programs (Jeffrey, 1997) Call-By-Push-Value, A Functional-Imperative Synthesis (Levy, 2004) Environments, continuation semantics and indexed categories (Power, Thielecke) Effectful Traces via Effectful Streams (Bonchi, Di Lavore, Román, 2024)