do-notation

Last updated Oct 7, 2024

• Do notation
• Arrow notation

I want to be calling Arrow notation to the arrow do-notation of Haskell, internal language for strong promonads.

• arrow notation for Freyd categories
• do-notation - theory of symmetric monoidal categories
• do-notation - theory of copy-discard-compare categories
• do-notation - composition
• do-notation - terms have a unique derivation
• do-notation - quotienting by interchange
• do-notation - theory of effectful copy-discard categories
• do-notation - loop do-notation

Prerequisites

• Freyd category
• effectful category
• symmetric monoidal category
• adjunction

Tags: internal language.