Owen Lynch

Cracking myself up over my morning oatmeal imagining if the proof assistant currently known as Rocq had instead been renamed "Le Chicken".

I think one reason why a lot of the academic literature on parsing and grammars is so disconnected from what language implementations use in practice is that what matters is not having a declarative spec for what an instance of the grammar is, what matters is following an algorithm whose failure conditions are understandable. When you implement recursive descent, at the point of a failure you know more or less what is going on.

A full declarative specification of what the parser should do in these error cases is not that much shorter than just writing the darn recursive descent algorithm out.

I feel like this is a general phenomenon, there are wide classes of programs where the spec is essentially the algorithm, and thus verification is kind of meaningless, it's more of a question of "does the algorithm do a reasonable and mostly predictable thing in practice"?

And this is why I like category theory for computer science, it works at so much higher of a level that it's orthogonal to a lot of practical questions. If category theory were lower level, I'd rather just scrap it and write code. But precisely because it forgets so much, it actually makes it easier to think about some questions. The "awkward middle" between math and programming where a lot of CS sits is often neither practically relevant nor conceptually simplifying.

Just picked up from "Logical Relations as Types" the practice of not saying the words "beta rule" and "eta rule" and instead saying "computation rule" and "uniqueness rule".

I feel like I would have been much happier if people had used this terminology when I originally learned type theory, and I'm definitely going to use it next time I teach someone.

While I'm on that subject... I like thinking about the four rules as answers to the four questions.

How can I make an element of this type?
How can I use an element of this type?
What happens when I use an element of this type?
Are there any other sneaky elements of this type? (No!)

You can find slides for the TYPES2026 talk I just gave on my website: https://owenlynch.org/archive/2026-types/1.html.

These slides include hippogriff (https://tangled.org/owenlynch.tngl.sh/hippogriff/) compiled to WASM, so you can edit the code snippets and run them with ctrl-enter to see what happens.

The observation that I can get trapped by almost any site with an algorithmic feed (YouTube, Twitter, Reddit, hell even Facebook), no matter how asinine the content it gives me, is very humbling to any pretensions of taste that I have...

To escape these, the solution has never been to block the relevant domain in ublock, because I inevitably end up wanting to look at some link that someone has sent, and then I unblock it, and then it's off to the races. The solution is also not self control. Maybe that works for some people. The solution is to figure out how to make the site dumber. For Twitter, it was locking my account. For YouTube it was disabling having a YouTube history, so that my home page was blank of recommendations. Facebook is dumb enough that I mostly manage to stay off it organically, thankfully. And for Reddit, I switched to Old Reddit and unsubscribed to all subreddits so my homepage is blank.

I still have the muscle memory for all of these things, even though I've been off Twitter for over a year, my fingers will still sometimes type twitter.com into a freshly opened tab.

I really think the algorithmic feed is one of the worst intentions of the 21st century. I don't think it's a good idea to ban it, but I think that there should always be a way (like I've found with YouTube and Reddit) of disabling the feed while keeping access to other material on the site.

When people complain about using category theory for PL, I think about this quote from Cryptonomicon (delivered by the fictional Alan Turing)

"Shut up about Leibniz for a moment, Rudy, because look here: You--Rudy--and I are on a train, as it were, sitting in the dining car, having a nice conversation, and that train is being pulled along at a terrific clip by certain locomotives named The Bertrand Russell and Riemann and Euler and others. And our friend Lawrence is running alongside the train, trying to keep up with us--it's not that we're smarter than he is, necessarily, but that he's a farmer who didn't get a ticket. And I, Rudy, am simply reaching out through the open window here, trying to pull him onto the fucking train with us so that the three of us can have a nice little chat about mathematics without having to listen to him panting and gasping for breath the whole way."

Swap out "The Bertrand Russell" for "The Alexander Grothendieck" and swap out "panting and gasping for breath" with "100-case syntactic arguments"...

In theory, a theoretical problem does not necessarily imply a practical problem, but in practice it almost always does.

@MartinEscardo@mathstodon.xyz A couple things.

1. I'd need concrete performance data that my handwritten parser was a performance bottleneck in the overall compilation pipeline before I would ever take on the maintenance burden of keeping two implementations in sync.

2. I would design the grammar in the first place for predictable and understandable errors, which concretely means: LL(1) with respect to whatever my tokenizer is doing. In this situation, I would expect that a parser generator wouldn't be that much faster than handwritten recursive descent, and quite possibly slower.

3. There are techniques in recursive descent like Pratt parsing which handle infix precedence or even fancier stuff like custom mixfix operators which are annoying to encode into a traditional BNF grammar; you can write an ambiguous grammar and then add precedences, but it's not so clear when you've done this that it's still LL(1), and I'd rather not bother.

4. I would expect that bigger performance gains would be around cache usage. E.g., use a sum of struct of arrays for your AST with 32 bit IDs instead of pointers, put token tags into single bytes in a byte array and store the associated spans elsewhere, use SIMD instructions in lexing, etc. These are the kind of things that production compilers do in order to really optimize performance. Again, I don't really care about performance for my parsers right now because it's not a bottleneck, but this is what I would do if I did care.

Whenever I do something fancy with normalization by evaluation I have an urge to shout "Yes closures! Dance for me! Dance! Dance!"

Is there a left adjoint to Nakano's later modality? It would be nice to handle it MTT style as a positive modality, rather than just have it as an applicative functor.

Perhaps it needs linearity in order to work though, because it's not a monad...

@danielgratzer@mathstodon.xyz @bentnib@types.pl

@MartinEscardo@mathstodon.xyz

1. Edward Kmett once told me that the reason he uses Haskell is that the pipeline to correct software of "write something highly reusable and then get a bunch of bug reports from the community" is much faster than "formally verify" and moreover you get not just bug reports but also patches that increase performance, add more features, etc. In this vein, I follow the philosophy of https://parentheticallyspeaking.org/articles/bicameral-not-homoiconic/ in writing a parser for a fairly generic notation once and then use it for all my projects, and then other people use it too, and the end result is a quite pleasant tool! (https://github.com/ToposInstitute/fnotation also ported to Haskell https://hackage.haskell.org/package/fnotation)

My video on teaching @thosgood@mathstodon.xyz how to elaborate the simply typed lambda calculus is up! https://www.youtube.com/watch?v=uBjuFDs-shw&list=PLhgq-BqyZ7i5C6ZnaYiGDhiGZuvvtLh5o&index=9

Modal type theory people:

Given a judgmental proposition P (that is, not necessarily a type, a meta-level proposition), there is an open modality associated to it which looks like (P -> A), this is right adjoint to adding a proof of P to the context. So far, so good.

I want to now instead have a context formation operator which acts like (P -> Γ). My intuition here is that (P -> Γ) "locks" the context Γ, and Γ,P "unlocks" the context. This seems to make sense because (P -> Γ,P) = (P -> Γ), (locking something unlocked is the same as locking the original thing) and (P -> Γ),P = Γ,P (unlocking something that has been locked is the same as unlocking the original thing).

Now, I don't expect (P -> Γ) to have a further right adjoint (I'm using it for a different purpose). But is this a kind of context operation that people have looked at?

I'm stopping by Utrecht Science Park for the next couple hours; if there are any type theorists who want to chat DM me!

@eigil@mathstodon.xyz yo welcome back to civilization

What's the minimal way of getting the yo hiragana in LaTeX without fussing too much with fonts, which will work on the arXiv?

@constantine

primitive modality, which cannot be done with SOGATs

OK good, I still have some tricks you haven't figured out 😜