Michael Arntzenius irl. PL design, math, calligraphy, &c. ✉️ daekharel@gmail.com 🐘 @rntz@recurse.social 🟦 bsky.app/profile/rntz.net
Joined June 2009
- Tweets 6,677
- Following 337
- Followers 1,893
- Likes 8,184
rntz retweeted
FP friends -- please encourage recently completed PhD students to publish their dissertation abstracts in the Journal of Functional Programming: simple process, no refereeing, open access, 200+ published to date, deadline 30th November 2025. Please share! tinyurl.com/jfp-phd-abstract…
today I thought "hm, maybe I should reread the Count of Monte Cristo". but you know what they say: vita brevis, ars longa.
anyone have a good mnemonic for "pushout = quotiented/glued sum; pullback = subset of product"? I have trouble remembering pushout ~ sum ~ colimit and pullback ~ product ~ limit. (Bonus points if it helps me remember pushouts glue and pullbacks subset.)
Slides for my miniKanren 2025 talk, "Fair intersection of seekable iterators", about an efficient, compositional way to implement relational joins on sorted data structures, and how it (sorta) requires "fairness": rntz.net/files/minikanren-20…
how can we find time to explain things?
good talks are so good, so valuable.
(... can we review them like we review papers?)
do we give talks to communicate ideas?
we publish in conferences: places where talks happen.
but w/ so many papers, conf talks are short & can't explain–only advertize.
so workshop talks are miles better.
how perverse! our strongest, peer-reviewed results–the worst explained!
I've joked re all SIGPLAN confs being ~the same before. But now I'm at icfpoopsla, picking which talks to see, I'm ~50/50 on ICFP talks vs workshop talks; but almost entirely preferring workshops to OOPSLA talks. Convergence? Not yet!
Slides for my HOPE 2025 presentation, "Finite Functional Programming via Graded Effects & Relevance Types": rntz.net/files/hope-2025-fin…
why am I calling my secret project "Finite Functional Programming"
when I could be calling it "Lambda: the Ultimate Relation"
why is writing (anything) so much like squeezing water from a stone?
approximately the most important thing in my profession. I have done it repeatedly. I wrote a whole thesis. it is no easier now than ever. perhaps harder. ughhhh
i go halfway around the world for a conference in a famous tourist city and first day what do I do?
go to a bookstore
rntz retweeted
To prove you're human, break the law
No serious LLM company will release a model that happily torrents videos or tortures kittens
This creates the most hilarious kind of CAPTCHA ever
rntz retweeted
Excited to announce that my paper, Typing Strictness, with @alpha_convert, Benjamin Pierce and @fancytypes has been conditionally accepted to POPL 2026.
Check out the preprint: sainati.pl/typing-strictness…
Analytically, we differentiate via limits/epsilon-delta. Synthetically, we use infinitesimals - artificial infinitely small quantities.
Analytically, we handle dirac deltas with distribution theory. What's the synthetic account? Is it artificial infinitely big quantities?
We are the ones who wonder why
strings that sing the sweetest lie
divisible in common parts─
proportion, queen of all the arts!
and yet the square's diagonal
cannot to its sides compare:
nature's ugliness so laid bare
we kill't him who uncover'd it
productivity of co(inductive)-programs
fairness of concurrent scheduling
completeness of search strategies
these three seem deeply related to me, but I can't yet precisely articulate how. Is there existing work on connections between them?