Matteo Capucci Profile picture
Mar 30, 2022 5 tweets 2 min read Read on X
Out today 👇 'Lenses for compsable servers', jww @andre_videla
arxiv.org/abs/2203.15633

We describe how the technology developed for open games can be repurposed to build web servers in a compositional way. Image
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 Image
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.

Enjoy!

• • •

Missing some Tweet in this thread? You can try to force a refresh
 

Keep Current with Matteo Capucci

Matteo Capucci Profile picture

Stay in touch and get notified when new unrolls are available from this author!

Read all threads

This Thread may be Removed Anytime!

PDF

Twitter may remove this content at anytime! Save it as PDF for later use!

Try unrolling a thread yourself!

how to unroll video
  1. Follow @ThreadReaderApp to mention us!

  2. From a Twitter thread mention us with a keyword "unroll"
@threadreaderapp unroll

Practice here first or read more on our help page!

More from @mattecapu

Dec 14, 2024
soooo why are proofs cultural objects? here's a quick thread 🧵
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
Read 22 tweets
Feb 6, 2023
Two of the most lucid paragraphs on the subject (emergence) I've read recently csc.ucdavis.edu/~cmg/papers/Ca…
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)
Read 4 tweets
Dec 12, 2022
@math3ma just gave a very interesting talk about this paper, with wonderful intuitions AN ENRICHED CATEGORY THEORY...
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.
Read 17 tweets
Nov 17, 2022
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…
Read 4 tweets
Nov 15, 2022
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. I'm here to help improve co...
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. Mathematical fields as acco...
Read 12 tweets
Jun 28, 2022
👉🏼 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 From https://www.thesprucecrafts.com/warp-and-weft-1177681
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!
Read 10 tweets

Did Thread Reader help you today?

Support us! We are indie developers!


This site is made by just two indie developers on a laptop doing marketing, support and development! Read more about the story.

Become a Premium Member ($3/month or $30/year) and get exclusive features!

Become Premium

Don't want to be a Premium member but still want to support us?

Make a small donation by buying us coffee ($5) or help with server cost ($10)

Donate via Paypal

Or Donate anonymously using crypto!

Ethereum

0xfe58350B80634f60Fa6Dc149a72b4DFbc17D341E copy

Bitcoin

3ATGMxNzCUFzxpMCHL5sWSt4DVtS8UqXpi copy

Thank you for your support!

Follow Us!

:(