Mario Román

Home

❯

notes

❯

arrow notation

arrow notation

Jan 16, 20241 min read

I will be calling Arrow notation to the arrow do-notation of Haskell, internal language for strong promonads. This is different from do-notation, the internal language of strong monads over cartesian categories.

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

Prerequisites

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

Considerations

  • quotient to hypergraph
  • arrow notation modules in the host language

Tags: internal language.


Graph View

Backlinks

  • Simple type theory
  • three Covid tests
  • do-notation for Freyd categories
  • Do-notation in type theory
  • another do-notation
  • do-notation substitution
  • copy-discard arrow notation
  • do-notation - theory of copy-discard-compare categories
  • do-notation for copy-discard-compare categories
  • do-notation in Racket
  • do notation
  • internal language
  • interventions via Markov magmoids
  • conditionals using do-notation
  • quotient to hypergraph
  • symmetric monoidal category
  • two styles for monoidal streams
  • A Simple Formal Language for Probabilistic Decision Problems (Di Lavore, Jacobs, Román, 2024)

Mario Román (2026), CC-BY-SA. Human written, using Quartz and Write.

  • GitHub
  • ArXiv
  • OrcID