Before we start digging into the main topic, I will establish the state of the literature surrounding the topic at the time I started it.
My main thesis is that containers and their morphisms are a prime data structure to describe and implement interactive programs. Before we study them, we should know what people have done with containers, their morphisms and with interactive systems. There are broadly three categories that can classify the existing literature on those topics:
- The pure mathematics of containers and programs.
- The type theory of interactive programs.
- Programming interfaces using containers and dependent types
The first one encompasses the literature around categorical structures of programs, the categorical semantics of containers, and the mathematical descriptions of interactive systems. In that realm I would put Abbott, ghani, spivak, thorsten and moggi.
The second one classifies literature decribibg type systems which primary concern is to provide rules and syntax for interactive programs. Hot topics in that area are session types, linear types, quantitative and graded type theories, refinement types and separation logic to some extent. authors include bob atkey, my supervisor, but also Dominic orchard, Niki vazou