We describe how the technology developed for open games can be repurposed to build web servers in a compositional way.
This paper is basically a companion to the Idris2 library André wrote, Recombine: gitlab.com/avidela/recomb…
Although it doesn't strictly follow the 'categorical cybernetics' tao, it's still a very neat approach to correct-by-construction servers
The FP folk has known lenses & optics are a neat abstraction for a long time, here we show parametric lenses deserve attention too. They allow *parametric data access*, such as that of a client requesting resources to a web server.
So in the paper you'll find a 'practical' walkthrough of the abstractions employed in the library (lenses, dependent lenses, parametric dependent lenses), and their use in server development; followed by a walkthrough of Recombine itself.
here's the deal: proofs are mainly artifacts (usually text, but figures count too!) mathematicians produce to convince other mathematicians of some fact about their *shared* imaginary world. without the *shared* part, they'd mean nothing. 1/n
specifically there is no such thing as a 'correct proof', there is only a consensus about which proofs are correct. correctness it's not an objective fact. 2/n
And now a very interesting concept/observation: some emergent effects have intrinsic significance since they feed back in the components of the system which gave rise to the them:
Hence this classification of emergence (paraphrasing Cruthfield below): 1. 'something new appears' 2. 1 + observer identifies a pattern 3. 2 + the observer is part of the system itself (strong 2nd order cybernetics vibes from this one)
@math3ma just gave a very interesting talk about this paper, with wonderful intuitions
My understanding of the situation is the following (and I hope she'll correct me if I'm wrong). At a first approximation, a lang model (LM) learns a Markov kernel π:X->X where X is a set of strings.
The question is, what structure shall we expect this kernel to have?
The idea of π is that given a string x:X, π(-|x) is the probability measuring the likelihood of a given string y:X to follow x. Hence π(y|x) is π(xy) up to normalization.
Idea: the structure of scientific revolutions identified by Kuhn is an instance of the more general features of evolutive/inferential dynamics. Available evidence provides the selective pressure for scientific theories.
For instance, lack of selective pressure produce adaptive radiation in evolution. en.wikipedia.org/wiki/Adaptive_…
This is analogous to the pre-paradigmatic phase of a science, where lack of evidence produces a plethora of alternative theories and models.
A 'revolution' would correspond to speciation/extinction, i.e. the strong selection of a few successful traits (revolution/crisis). Then for a long time these traits don't vary (paradigmatic periods), giving rise to punctuated equilibria. en.wikipedia.org/wiki/Punctuate…
David Spivak delivered one of the best motivational talks about ACT I've ever seen:
It's a replica of his NIST talk from last week, here's a few key points I personally vibed with 👇🧵
First: ACT is about better communication and better language *for SMEs* (Subject Matter Experts).
The corollary (this is me not David) is you shouldn't exact applications from applied category theorists.
It's not our job!
We provide the fishing cane, not the fish.
Second: mathematics as account systems. It's all in the slide. The example is great because is so easy to disregard $s as 'just numbers'.
Mathematicians (but CTists are somehow more sensible to this) know they must be parsimonious with structure.
👉🏼 Fibred categories are like woven fabric and doing a Grothendieck construction is a like weaving on a loom: a... thread about textile intuitions for fibrations 🧵👇🏼
The threads of woven fabric, when you look up close, are entertwined in a distinctive pattern: some of them run vertically (that's the *weft* or *woof*), and some run horizontally (that's the *warp*). The *bias* is the 'diagonal' direction, along which fabric is easy to stretch
Likewise, when a category E is fibred there is a factorization system that tells you how to decompose each morphism into a 'warp' part and a 'weft' part.
If we forget about the weft, we can project down our fabric on the selvedge. This projection is the fibration!