Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Container Morphisms for Composable Interactive Systems

André Videla

TL;DR

This paper develops a formal, dependently typed framework for composing multi-tier interactive systems by modeling interfaces as containers and translations between them as container morphisms, enabling modular assembly of client, server, and storage layers. It introduces a session model via the Kleene star on containers and a monadic perspective through $MaybeAll$, along with context-, state-, and costate-based execution to run composed API transformers with effects using $Lift$ and $IO$. The approach is mechanised in Idris2 and demonstrated with a To-do application and a filesystem-like example to illustrate correct-by-construction behavior across surfaces and underlying APIs. Overall, the work offers a principled, reusable methodology for building end-to-end systems that span different protocols, while providing formal guarantees about composition and effect management.

Abstract

This paper provides a mathematical framework for client-server communication that results in a modular and type-safe architecture. It is informed and motivated by the software engineering practice of developing server backends with a database layer and a frontend, all of which communicate with a notion of request/response. I make use of dependent types to ensure the request/response relation matches and show how this idea fits in the broader context of containers and their morphisms. Using the category of containers and their monoidal products, I define monads on containers that mimic their functional programming counterparts, and using the Kleene star, I describe stateful protocols in the same system.

Container Morphisms for Composable Interactive Systems

TL;DR

This paper develops a formal, dependently typed framework for composing multi-tier interactive systems by modeling interfaces as containers and translations between them as container morphisms, enabling modular assembly of client, server, and storage layers. It introduces a session model via the Kleene star on containers and a monadic perspective through , along with context-, state-, and costate-based execution to run composed API transformers with effects using and . The approach is mechanised in Idris2 and demonstrated with a To-do application and a filesystem-like example to illustrate correct-by-construction behavior across surfaces and underlying APIs. Overall, the work offers a principled, reusable methodology for building end-to-end systems that span different protocols, while providing formal guarantees about composition and effect management.

Abstract

This paper provides a mathematical framework for client-server communication that results in a modular and type-safe architecture. It is informed and motivated by the software engineering practice of developing server backends with a database layer and a frontend, all of which communicate with a notion of request/response. I make use of dependent types to ensure the request/response relation matches and show how this idea fits in the broader context of containers and their morphisms. Using the category of containers and their monoidal products, I define monads on containers that mimic their functional programming counterparts, and using the Kleene star, I describe stateful protocols in the same system.
Paper Structure (5 sections, 2 figures)

This paper contains 5 sections, 2 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related Work
  4. Containers & APIs
  5. The category of containers

Figures (2)

  • Figure 1: A binary client-server model, events read clockwise.
  • Figure 2: An illustration of my revised compositional client-server view. Each color represents a different piece of software, each boundary between colors represents a protocol with messages and responses. The lifecycle of a single interaction can be read clockwise starting from the $UI$.

Theorems & Definitions (2)

  • definition thmcounterdefinition: \formalisationURL#line23
  • definition thmcounterdefinition: \formalisationURL#line30