optics and servers · theory: applied category theory

Hi there, I've been informed that people here might be interested in this presentation that I gave yesterday about a project of mine, relating the implementation of server and their API all while using lenses to describe and extend both implementation and API https://www.youtube.com/watch?v=4xpbYPa1lTc

Henry Story (Jul 03 2021 at 04:39):

Watching this I thought to myself "Mhh, lenses look very much like coalgebras", and that would fit the discussion we were having on the web-cats channel recently. So I thought I'd catch up a bit on lenses and watched Bartosz Milewski's course on lenses and indeed they are. At the end of the talk he even says: "a lens is a comonad coalgebra" (perhaps limited to the Store Comonad?), something to add to the discussion about Comonads that @Eric Neumann started.

Henry Story (Jul 03 2021 at 08:20):

(The second part of that talk goes into a more composeable version of Lenses, still related to the above though by the Yoneda Lemma)

Henry Story (Jul 04 2021 at 05:53):

I was just looking at this course from 2019 again Comonads by Example by Chris Penner, who really does a very good job of building up intutions very clearly. (I am not sure yet about his idea that there is something comonadic about

a \to f b

in monads...).
The second video looks at the Store comonad.
That made me think: A Web Server is a store of States comonad. The index into the Store are URLs and the values are states, which can be changed. Or perhaps better the values are coalgebras with various methods to observe and change the state?

Henry Story (Jul 04 2021 at 06:15):

experiment :: Functor f => (s -> f s) -> w a -> f a

as I provide a function from a URL to a set of of URLs which are all the access control rules linked to from the first. That function would need to be given the store itself, in order to (1) be able to fetch the first access control rule and then (2) collect for each rule the imported access control rules. So experiment above would be very inefficient way of doing that: one really wants to traverse the store....

Henry Story (Jul 04 2021 at 06:19):

What falls out from that experiment and the hyper-textual and hyper-data nature of the web, is that as soon as you start following links, you don't as a client at least (but client/server is just a role distinction not an ontologically fundamental one - See issue on peer to peer web ), ... so you don't consider one web server alone, but you must look at the whole web itself.
So you need a Web Store, that gives you the state of all the resources possible. That would then have to be in non-verified handwavy scala notation

type Web = Store[URL,Option[ResourceState]]

Henry Story (Jul 04 2021 at 06:42):

But that is not quite right, because we never get back states on the web (a web server may), which we can interact with. Instead we send messages to those resources, which respond by telling us if they exist (200) or don't (40x if lucky, or by never responding if the server is not up or does not exist.)

Henry Story (Jul 04 2021 at 07:09):

In that video there is a quick overview of how to represent Conway's Game of Life using the Store comonad. He points out that the default implementation is very slow, but that this can be fixed using representable functors. I wonder if those can be used for caching on the web too! :thinking: - I need that!

Matteo Capucci (he/him) (Jul 04 2021 at 09:28):

This reminds me of a recent talk by @André Videla on RESTful APIs as parametrised lenses. If you consider that (monomorphic) lenses are coalgebras of Store, this is even a more compelling link.

Henry Story (Jul 04 2021 at 09:32):

heh. yes, indeed that is what I started watching a few days ago. Lenses reminded me of coalgebras, and a talk by Bartosz showed that indeed "lenses are exactly the coalgebras for the costate comonad", and so I wanted to get a better feel for the costate comonad = the store comonad. I should perhaps finish watching the Optics talk now that I have covered Store. Then I can provide some feedback.

Henry Story (Jul 04 2021 at 11:24):

@André Videla's starts looking at Lenses as a topic at minute 19 of the talk.
At around minute 22 he looks at how GET and POST on a resource would map to functions, except of course that the state change method requires state to be around (in an FP language). And so that is what is addressed at minute 25. The point there is that from the point of view of the client the lens is enough, it does not need to take account of the state, but the server does. And so just before minute 26 he looks at State Management. And so he moves from

GET: User -> List Todo
PUT: User -> List -> ()

GET: User -> State -> List Todo
PUT: User -> State -> List -> State

Which is what I was thinking about the need for a Store URL ((GET x PUT) coalgebra)
(Note that on a well built web server the client should get an ETag header, which should be a name for the state).

Henry Story (Jul 04 2021 at 12:04):

Because the web is built on message passing, It may be that actor frameworks built around that concept such as Akka are better suited to build web servers. There actors are named by URLs and a responsible for some state. So in the web server I built on that, all messages in the system have URLs attached to them, so that they can know where to go. The server routes the messages to the right actor. I had been thinking of implementing those as state monads communicating with the "external world" including other actors.... But an actor could also be a particular location in a Store Comonad (the location given by URL naming the actor), which would allow it to communicate with its neighbours.

I was thinking perhaps the extend method could be more appropriate for authorization than the "experiment" method I mentioned above.

class Functor w => Comonad w where
    extract :: w a -> a
    duplicate :: w a -> w (w a)
    extend :: (w a -> b) -> w a -> w b

The first function given to extend w a -> b could be the function that takes a Web Actor (w a) and because it is able to follow links around, can fetch all the needed data to determin access, returning a boolean b (by a stroke of luck the variable names all work).

Henry Story (Jul 05 2021 at 15:53):

So in short it seems like @André Videla's talk (above) confirms the intutions we were having on the web-cats channel and especially those expressed by @Eric Neumann about the importance of Comonads for the Web, once we know that Optics are coalgebras for the Store comonad.

Henry Story (Jul 09 2021 at 18:41):

It turns out that there is also an algebraic description of lenses, along with the coalgebraic one mentioned above.
"the category of lenses for a fixed "view" V is, up to isomorphism, the category of algebras for a particular monad on Set/V. "
that is taken from the 2012 article from Jeremy Gibbons, Michael Johnson where they explains in detail how they are equivalent for "very well behaved lenses" which follow three laws
Relating Algebraic and Coalgebraic Descriptions of Lenses.

Henry Story (Jul 09 2021 at 19:44):

The coalgebra for the store comonad is defined as:

l = \langle p, g \rangle: S \to S^V \times V

where p is the change of state function (PUT) and g is the request to observe a value (GET).
The coalgebra is easier to see if we have defined the store monad functor

D(A) = A^V \times V

then l is the coalgebra

l : S \to DS

(I think I had somehow been associating the lens with the Store, but the image below shows clearly how it is the coalgebra on that store!)
This is the picture from the article that is really helpful.
Lenses are the coalgebras for the costate comonad

Henry Story (Jul 09 2021 at 20:15):

We can actually understand better what part of the web can be modelled by (these types of) lenses by looking at the laws.
The first one is the get-put law

\epsilon \circ \langle p, g \rangle = 1_S

which states that if you GET the value and PUT it back then you are in the same state. That is because the store has

\epsilon (f, v) = f(v)

That does seem to match HTTP.
Note that in @André Videla 's presentation above there seems to be a problem with the choice of POST as the verb to change a resource instead of PUT. POST creates a new resource, it is a speech/document act, which is unique - so probably where linear logic is needed? a POST can be used to buy something, send a text message, ... POSTing the same form twice, could end up buying two items...
One problem I see for the moment is that I don't see a place for POST in the coalgebras. Especially if S here is the state of one resource, because then it could not create a new one... Is that where the other optics come in?

Henry Story (Jul 09 2021 at 21:02):

the second law known as put-get is that if you PUT then GET you should get what you had last PUT.
That will work if you are the actor in charge of the resource. If you are a client, then it is quite possible that someone else altered the state of the resource in the mean-time. (As an actor it is also possible that someone edited the file while the server was running, something that it is difficult to exclude).

And thirdly there is the Put-put law which says that if you PUT P and then PUT Q then you could have skipped put of P. True the last PUT wins. Again this is different from POST: with POST the intermediate creations of resources continue to exist.

Henry Story (Jul 09 2021 at 21:04):

(The article argues all three laws fall out from this being the coalgebra for the store comonad).

Henry Story (Jul 09 2021 at 21:06):

Henry Story (Jul 10 2021 at 16:23):

I wrote up some code using the Scala Monocle library to simulate a POST. It uses the modify method that is defined on the Setter trait, and available on a Lens.

def POST(slug: String, text: String): Container => Container =
    contents.modify(oldMap =>
        oldMap + (slug -> TextResource(text))
     )

> val p1 = Server.POST("blog1","My first blog. Testing")
> val newRoot = p1(Server.root)
val newRoot: monocle.Container = Container(Map(blog1 -> TextResource(My first blog. Testing,2021-07-10T14:31:41.680411Z)),2021-07-10T14:31:41.640292Z

Henry Story (Jul 10 2021 at 19:35):

So where I differ from @André Videla in the way I conceive of a Web Server, is that I think of a web server as essentially perhaps requiring nothing more than the colagebra on the Store comonad, and perhaps the concept of a Container and a Resource as in

sealed trait Resource[T] {
    def content: T
    def created: Instant
}
case class Container( content: Map[String, Resource[_]] = Map(),
         created: Instant = now) extends Resource[Map[String, Resource[_]]]
case class TextResource(content: String, created: Instant = now) extends Resource[String]

The String attributes in the Map constitutes a path segment giving us the path to the resource. Containers can contain Containers, giving us the URL Path such as </people/tim> .
The resource itself could just be a bytestring with metadata such as a mime type to be interpreted by the client, or a creation date.

It is the clients that create the resources, that get described with metadata. A Client can create an image, some css, some html, a film, some javascript, on a server and link them altogether so that they form a nice blog page. Then it can add some RDF to describe the data in an RSS feed.

It is really up to a read/write client to POST new content, edit it with PUT if needed, and GET it to display it. That is what the LDP protocol essentially describes.
So the way to see it is perhaps that Lenses explain why we have this simple universal API with which to interact with any such server.

These require more of the server, as they require it to interpret the data on its store and keep indexes for example.

Henry Story (Jul 10 2021 at 19:51):

Say that lenses as such actually help give us a nice model of a web server (without access control). Is there a category where I could take the idea of a Lens which would better fit the actor model, such as implemented by Erlang or akka)

Henry Story (Jul 11 2021 at 08:29):

I think one can actually see why the actor model is advantageous over the model presented in Andre's video above.

The model of the web server given by Andre is an immutable model. That is the advantage of optics: it gives you a way to change the state of one component inside a much larger structure. So you are to imagine the whole web server in one immutable data structure.
A PUT on </foo/bar/baz> changes the object at that location and returns a new root web server object. The risk here is that one then has to sequentialise updates, or deal with problems of merging a number of web server objects resulting from parallel update requests. Having an sequence of update events for the whole web server could be useful for keeping a full history of it perhaps. But given that a web server has pages linked to the whole web, and that keeping a full history of the whole web is impossible and even undersireable (due to privacy reasons for example), it is not clear that this is really that useful. The state of the server will have to be written to disk, so it may be better there to have a versioned file system. In any case the versioning was not the part put forward in the talk, and it creates a lot of other problems as we saw, potentially sequentialising all updates: someone wants to upload a 500MB video of a cute duck swimming in a pond, and everyone else using your web server will have to wait for that to complete before they can do the next update.

The actor model on the other had limits state transformations to the smallest state needed. So if a new video is POSTed to /2021/07/11/ then only one actor for that resource needs to be synchronise the state of that resource. Edits can occur simultaneously on any number of other resources too.

Henry Story (Jul 13 2021 at 07:27):

Even though I don't see Lenses as a good way to implement a web server, it does at least seem to do one thing right: it captures the laws a client relies on when fetching, puting or creating a resource (at least in an ldp:BasicContainer). The laws seem to tell us that a client that makes such requests, can know that it is not responsible for any other changes to the server. Any other changes must be due to other agents.
To re-iterate the problem: an implementation of a web server as a Lens would force all changes to by synchronised by the server as it coalgebraically steps from one state to the next - this requires too much synchronisation.
But the laws seem to be right.

So we seem to have structure describing a contract. Does that make any categorical sense?

Category Theory
Zulip Server
Archive

Stream: theory: applied category theory

Topic: optics and servers

André Videla (Jul 02 2021 at 18:01):