by Andre Videla
Today marks the official release of the Stellar series of libraries for Idris2, a library based on Containers1 demonstrating the power of API-programming. A new programming paradigm focused on manipulating program interfaces, rather than program objects.
This blog post is not about Stellar itself, but about the nature of containers as a tool to model multi-agent interaction, and how it relates to the work we have been doing at Glaive. You can learn more about stellar on its main page.
While developing the technology on Tactics, we stumbled upon a curiously unsolved problem: How do we make sure agents, whether human or machine, can only communicate appropriately with a third party? In our case we were attempting to constrain the kinds of messages an editor can send to the compiler, but this question has much broader applications. Indeed, the editor-compiler interface is a specific instance of a bipartite protocol. The challenge in that communication is the ability to control the protocol depending on the previous states of the system. In other words, how can we accurately describe how one system talks to another?
Stellar offers the perfect solution to that problem. We are faced with an interface (the compiler) and we would like to match it to another interface: well-typed tactics. In turn, this interface of well-typed tactics needs to be usable by a model such that the model only ever communicate in ways that make sense in the current proof context.
This approach is synergistic in at least three ways. First with Stellar, we employ Containers to describe programming API. For our purposes, it turns out this compiler API can be neatly encapsulated by LSP, the Language Server Protocol, exposing common programming actions from an editor to a compiler. Second, we combine our interpretation of Tactics as Containers in the same picture. The object we manipulate to connect our compiler to our interpretation of tactics are one and the same. Finally, the object interacting with the compiler, today a language model, generates objects eerily familiar to Containers.
With the rise of Large Language Models as general purpose assistants we have seen attempts at combining the existing programmatic world with the world of tokens. This interface is extremely challenging to implement because tokens are, by their very nature, highly unstructured. A series of word fragments can only match a programming interface by fortunate coincidence, a coincidence that harnesses and training data work very hard to make happen. But what if we didn’t have to rely on statistical improbabilities and instead build the structure within the model such that stepping outside the expected structure is impossible?
This is what we are exploring.
The idea that containers model interaction occurred many times across history 2 3 4 5 6. What we did is test this idea against the real world by implementing Stellar, a library to build programs where the unit of program manipulation is not a function, but a lens. In turn those lenses explain how to translate from interacting with HTTP to a database or other microservices. All this work is based on containers as interaction descriptions.
We define an interaction as a pair of a message and a response indexed by that original message. This structure is exactly a Container, its morphisms define exactly dependent lenses and APIs such as HTTP endpoints are merely the co-product of multiple simple containers defining a single request/response pair.
We can see this relationship in the code of stellar:
-- An API is a pair of a message and a response for that message.
record API where
constructor (!>)
-- The type of messages we send to the system.
message : Type
-- The type of responses we expect for each message we send.
response : message -> Type
The morphisms of API, called API-transformers in Stellar, are the lenses between containers:
record (=&>) (a, b : API) where
constructor (!!)
continuation : (x : a.message) -> Σ b.message (\y => b.response y -> a.response x)
What’s different with stellar is where we take those basic building blocks, and how they are going to help us produce correct-by-construction interactions.
Stellar makes clear the difference between a direct API call and one going through a substrate. We call substrate the hardware protocol that is not related to the program’s API but sits in the space between programs. For example, a browser and a server communicate with a shared API, the messages sent from the browser must match the messages expected by the server exactly. However, because the client and the server are different machines, those messages are run through a common substrate: HTTP. Indeed, each message needs to be serialised into an HTTP request, and the browser will make use of the facilities of the operating system on which it is running to send that HTTP request. On the other side, the server will also use the facilities of its own operating system to decode the request and deserialise it into data the program can understand.
So while there must be a direct match between client and server, there is a detour to take via a common substrate to handle the fact that those machines are separated by many layers of abstraction.
Sometimes the common substrate is used out of convenience, rather than necessity. The Language Server Protocol is a communication protocol over the HTTP substrate, even though, in the common case, the client and the server are hosted on the same machine.
The benefits of this approach is the abstraction afforded by HTTP over the details of the editor and its runtime, and the compiler and its runtime. The operating system provides all the tools to jump over this hurdle by making it easy to send and receive HTTP requests locally. Of course, nothing comes for free, and the cost here comes in the form of performance overhead. Instead of a shared library and a function call we need to serialise data in a request, run it through the network stack, catch it on the other side, and deserialise and run all the usual checks that the data has been preserved. Stellar provides a mathematical explanation to this choice, and also brings up alternatives: HTTP is but one substrate, could we pick another, more efficient, one?
Today, the convention to let a language model interact with structured software is though MCP. To make progress toward verified machine interactions we implemented MCP as an interaction pattern for apps written using Stellar. This is not going to suddently make MCP interacton verified. But it is the first step toward stating what can even be formalised, and how it can be improved.
MCP is communication
protocol that wraps around JSON RPC interface. For stellar, it means it’s a
lens with JSONRPC as its domain. But to instantiate an MCP server, one must
pick one of two substrates: HTTP or CLI. This is a very routine operation in
Stellar we can represent as a string diagram:
In principle there is nothing stopping stellar from proposing another substrate than HTTP or CLI to communicate with any other API, for example we could imagine:
.Net, one could imagine connecting the client and server via a simple
library call.To connect our compiler to our model, driven by tactics, we developed an MCP library using Stellar. This library provides a couple of insights related to MCP and communication protocols in general.
MCP
communicates with JSONRPC messages and responses, it is, at its
core, a lens JSONRPC =&> AsMCP A where A is the API of the application we
are modifying to support MCP. As you can see, the codomain is wrapped in a
functor AsMCP, this functor is actually a functor on APIs and its role is
to add to A the additional endpoints that MCP requires to run correctly.
The proper implementation of AsMCP is relatively straight-forward:
AsMCP : API -> API
AsMCP a = a + (MCPINIT + End)
It adds the choice of two endpoints, MCPINIT handles the initialisation
handshake returning server capabilities. End represents built-in features
that stellar can implement for you, we can better see what is going on with a
string diagram:
MCPINIT and End, and secondly, generate a lens that will route JSON RPC messages to either the existing API or one of the two new messages.Given an existing app handling an API A we can modify the API A via AsMCP
to handle MCPINIT messages as well as the built-in messages Stellar can do
without help (notification/initialized and tool/list). Because AsMCP is
merely adding constants via +, it’s a functor by virtue of partially applying
+ as a bifunctor.
This work is not hypothetical. It has been tried and tested on a live server. You can point your
favourite LLM to the url https://stellar-mcp-todo-app.fly.dev/mcp and it will be
capable to use the interface of a basic todo app built with Stellar and stellar-mcp.
This application is compliant with the official spec, tested with the official MCP tooling.
Our progress on structured generation has encouraged the acceleration of this research programme by demonstrating that models, by learning structure, can internalise notions of interaction previously handled by the harness. Where before, a model has no choice but generate tokens, we can now provably ensure that only well-formed structures are generated. As of today, those structures take the form of a sigma-type. Indeed, in our internal prototype we can learn structures based on a type that informs the shape of the upcoming data, and then the data, appropriately indexed by the shape given.
This representation by design follows the structure of a container, and as such not only it can represent well-formed data structure, it can generate well formed patterns of interaction by first advertising what kind of interaction it means to use, and then generating the data for that interaction method.
Our experiments are currently only limited by the amount of man-hours available every day, but we have concrete plans to take this further. There is a myriad of research avenues that we are exploring, including AD wrt to communication protocols, fixpoints of containers for protocols, typically to represent the kleene star of a communication pattern, and introducing some bespoke interaction patterns for compiler interaction in a structurally sound way.
Michael Abbott, Thorsten Altenkirch, Neil Ghani & Conor McBride : Derivatives of Containers ↩
Andreas Blass: Questions and answers – a category arising in linear logic, complexity theory, and set theory ↩
Mihai Budiu, Joel Galenson & Gordon D. Plotkin The Compiler Forest ↩
Jules Hedges Morphisms of open games ↩
Peter Hancock & Anton Setzer: Interactive Programs in Dependent Type Theory ↩
Andre Videla: Container Morphisms for Composable Interactive Systems ↩