romance languages imply the existence of bromance languages
Remote
rntz
@rntz@recurse.social
Michael Arntzenius irl. PL design, math, calligraphy, &c.
Postdoc at UC Berkeley working on incremental computation, DB ⋈ FP, etc.
698
Followers
306
Following
26
Posts
Joined November 18, 2022
Web:
Twitter:
cohost:
rntz
email:
daekharel@gmail.com
Posts
Replying to
@okennedy@discuss.systems
@okennedy@discuss.systems here's a concrete example:
O(g1, g2) G(g1, e1) G(g2, e2) E(e1, v) E(e2, v)
FDs:
G(g, e): g determines e uniquely
E(e, v): e determines v uniquely
so there are at most |O| results for this query.
But, if my database is:
E(e_1, v) ... E(e_n, v)
G(g, e_1) ... G(g, e_n)
and no O() facts at all
there are no query results but a WCOJ can do n^2 > |O| work with variable order v, e1, e2, g1, g2:
v <- {v : ∃e. E(e,v)}
e1 <- {e : E(e,v) and ∃g. G(g,e)}
e2 <- {e : E(e,v) and ∃g. G(g,e)}
...
Replying to
@rntz@recurse.social
@okennedy@discuss.systems do you know anything about this by chance?
Is there standard literature on how to do worst-case optimal queries in the presence of functional dependencies/foreign keys? There are cases where you can use FDs to get asymptotic speedups but I'm having trouble figuring out the right general approach rather than looking at individual queries and saying "oh, obviously you index it this way and then it's fast".
Replying to
@rntz@recurse.social
Deus Ex (2000), a favorite game of my early life. For me, it expanded what a video game could be *about*. How big, conceptually, it could be. What questions it could ask about the world, or choices it could ask of the player. Nostalgia is definitely a factor, and its uniqueness has been diminished by its influence, but I did have a tradition of replaying it every year or two for about a decade, and it held up.
Replying to
@rntz@recurse.social
Outer Wilds. In Outer Wilds, exploration, puzzle-solving, and story are inseparable in a way only possible in a video game. You explore to find puzzles; solve puzzles to explore; solving puzzles tells the story; the story helps you solve puzzles. Feels like nothing could be added to or removed from it without loss. And yet, somehow, the DLC does improve it - although mostly by creating an isolated world-within-a-world. But this itself gives a different perspective on the events of the main game.
Replying to
@rntz@recurse.social
Hollow Knight: Silksong. I just finished this (113 hours!) and it's the first game I think I've ever 100%ed, and maybe the only game that's ever made me want to work hard to get good. The movement mechanics are an absolute masterpiece. Felt a bit like doing a PhD: constantly getting stuck and getting unstuck, requiring determination and continuous self-improvement. (Hades is similar but more frantic and less meditative, lacks exploration, and I couldn't "feel" my own improvement as clearly.)
VIDEO GAMES I STILL THINK ABOUT, A THREAD
If I had to identify running themes in video games I like, I'd say: exploration; puzzles; unique or fitting art direction; and telling a story in a way only a videogame could. But unlike happy families, every good video game is good in its own way, so here are a few of the ones I've liked most.
[inspired by @chrisamaphone@hci.social's great thread: @chrisamaphone@hci.social@recurse.social]
Replying to
@rntz@recurse.social
The video of my FLOPS 2026 talk on Finite Functional Programming is now up on youtube! https://www.youtube.com/watch?v=Ji2FF4mDhDE
It's 24 minutes long and probably the clearest explanation of my current thinking about how to design a higher-order functional query language besides the paper itself. If you read the slides and were confused about something, it might be explained in here. (The slides & paper are linked up-thread.)
Replying to
@jonmsterling@mathstodon.xyz
@jonmsterling@mathstodon.xyz I think “maintain two grammars” is better for the ecosystem than the tacit expectation that we trust the codebase as soon as we want to check a proof. This is getting into “wish list” rather than “reasonable expectation” territory, but given the rise of supply chain attacks I’d like to see more sandboxing / safety guarantees from new languages, not less, especially when it comes to things like theorem provers that might in principle be used to verify untrusted code.
Replying to
@mevenlennonbertrand@lipn.info
@mevenlennonbertrand@lipn.info indeed, but what if I don't have negation :P
(I am less-than-half-joking. If you squint, miniKanren's search strategy implements parallel or. But miniKanren very definitely does not have arbitrary negation. I have heard that Andorra Prolog has something like "parallel and" but I have not investigated further.)
Replying to
@rntz@recurse.social
Likewise, mathlib being 7G compiled is not *that* ridiculous given it's a formalisation of substantial parts of modern math (as someone pointed out to me on twitter).
And, yeah, many modern languages do per-project dependency management to avoid versioning difficulties.
there is like, no individual part of this that is indefensible. but the combination of everything just results in something that is... not great as a first experience.
Replying to
@rntz@recurse.social
looks like "no syntax highlighting without trust" is specific to Lean, not VSCode, because Lean has strong syntactic metaprogramming (hey, I like mixfix and syntax extensions!) but this means you have to run Lean code to parse Lean (eh, okay...) and Lean is also a general-purpose programming language (useful...) which can access your filesystem in arbitrary ways (uh oh) and it doesn't come with a sandbox so...
yeah, you have to trust the project to syntax highlight it iiuc. argh.
Replying to
@rntz@recurse.social
looks like the origin of parallel-or might be Plotkin 1977, "LCF Considered as a Programming Language" (https://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf) I should probably just read it (31 pages single column) but it looks a mite intimidating.
I've heard of "parallel or", (x por y), which terminates with true iff either x or y does, unlike "x or y" which diverges if x does. What about "parallel and":
false and x = false
x and false = false
true and x = x
x and true = x
Is there a canonical or useful reference for either of these?
Replying to
@rntz@recurse.social
checking out a tutorial project and I need to "trust" the project folder - which AFAICT allows arbitrary code exec on my machine by whoever authored the repo - in order to interact with Lean code in any way, even syntax highlighting, it seems? What the actual fuck? Who thought the correct options were (a) things just don't work at all, (b) arbitrary code exec, and NOTHING IN BETWEEN?
modern development baffles me.
I followed the instructions from https://lean-lang.org/install/ to install lean via VSCode and create a first project with mathlib, and then I ran
$ du -hs first-project/
7.0G first-project
SEVEN GIGABYTES
what the fuck is going on here? who the fuck thought this was an acceptable outcome?
Replying to
@rntz@recurse.social
The slides for my FLOPS 2026 talk on "Finite Functional Programming" are now available! https://www.rntz.net/files/flops-2026-finite-fp-slides.pdf
These are similar to, but I think more intuitive & accessible than, my HOPE'25 presentation (https://recurse.social/@rntz/115364255843280509) In particular I managed to avoid diving into typing rules. So I recommend reading these first and reading the paper or the HOPE slides if you want more detail.
"Loft" is a measure of how much down feathers "puff up" and so how much insulation they provide. Martins are a variety of bird. If I filled a sleeping bag with martin down and measured its puffiness, would that be... Per-Martin Loft?
The miniKanren and Relational Programming workshop is accepting submissions until June 5th! You (yes you!) should submit! We accept short or long papers, about miniKanren or relational programming more widely - and, this year especially, about relating the two, and what relational/logic/constraint/etc programmers can learn from one another! :)
https://icfp26.sigplan.org/home/minikanren-2026#Call-for-Papers
mastodon continues to be a great place to talk about wild maths ideas; all the replies I got to this were fantastic and illuminating
Replying to
@sliminality@types.pl
@sliminality@types.pl other: I still don't know it, because it is false in the contexts I care about (partial orders).
counterexample: in sets ordered by inclusion, not {1} <= {2} but also not {1} > {2}.
(For real though, I picked "show results" because I honestly don't remember when/how I learned this.)
Replying to
@rntz@recurse.social
I have lots of future work in mind here: I hope to implement this with indexed streams (https://arxiv.org/abs/2507.06456) / fairly seekable iterators (https://arxiv.org/abs/2510.26016v1) and to generalize from finiteness to other degree constraints (https://arxiv.org/pdf/2504.02770) eg functional dependencies and cardinality constraints, cf https://recurse.social/@rntz/116529665044883799
I have a new paper with @mwillsey@discuss.systems!
"Finite Functional Programming" (https://arxiv.org/abs/2604.26161) combines functional programming with relational/tensor algebra using functions of finite support: Datalog relations are finite boolean functions; tensors are finite real-valued funs. We ensure finite support of λ-terms using graded effects to check grounding, and relevance types (the "use at least once" cousin of linearity) to check relational/tensor operations preserve "absence" appropriately.
Replying to
@jcreed@mastodon.social
@jcreed I don't think I understand the notation here. What is ΣA₁? I know what (Σ(x:X) P x) is. But I don't know what (ΣA) is when A is just a type.
Replying to
@rajeesh@typo.social
@rajeesh@typo.social wrote my own site-specific generator in Python + Makefiles, been maintaining it since 2008. uses some boringly old tech (Mako https://www.makotemplates.org/ sass https://sass-lang.com/ yaml, markdown) and has some weird hacks (to make builds faster I worked around python's startup time by implementing a little python job server and a little C client that connects to it via unix sockets).
unfortunately it's too deeply entangled with the site's content for me to put it on github or similar.