RIP to Bill Lawvere, right as I'm teaching my categorical logic/type theory class, a field he invented.

@apostolis @amy As far as the Haskell pretty printer libraries go, they seem to have basically all adopted semantic annotations, and the idea is now standard. It's in both prettyprint and pretty, which are the standard-bearers for each of the major styles.

As far as interactive errors go, I'm not aware of the idea spreading, at least not from my Idris work. The rise of LSP has imposed both a floor and a ceiling on our UI ambitions, and while it's had lots of good effects on getting decent interfaces for lots of languages, its limited set of verbs and datatypes also limits what we can build.

Any of my POPL peeps want to grab dinner

This is just to say

I have painted
the shed
that was housing

and whose
colour you
probably
liked a bit

Forgive me
this feature proposal
the language syntax

Where does the myth that Univalent Foundations = Constrictive Foundations come from, and how is it so persistent????

Every day my hatred for PG&E only grows stronger

Paper Accepted

Happy to announce my paper with Dan Licata "A Formal Logic for Formal Category Theory" has been accepted to FoSSaCS 2023. Preprint available on arxiv for now but we'll be doing some updates for the final version (arxiv.org/abs/2210.08663)

Think I finally have a good strategy for elaborating ordered linear type theories; it's surprisingly tricky!

Cofibrations are one of the 3 classes of maps appearing in Quillen's definition of model structure and one of the key links between homotopy theory and type theory.

The 1Lab has had to resort to using Bop It! as a source of lemma names.

I have spent literally 2 hours recompiling agda over and over because of this goddamn library

libicu is my mortal enemy. Every time I need to build agda it seems to break in new and awful ways. For some reason the source files you can get all have windows line endings. Absolutely livid lol

Delighted to release the third edition of Programming Languages: Application and Interpretation (PLAI). A complete rewrite based on many years of research and experience. Because that research is still ramping up, this is just the start of many changes.
plai.org/

"Oh, I'll use representability so I can work with the category of Sets wont that be nice"

Meanwhile happly is sitting around the corner just waiting to bonk me with the "all your arguments are in the wrong order" hammer

Cubical Agda would be so much nicer without happly and funext.

My kingdom for a way to make case-split introduce as many variables as there are pis after a copattern split

caveat brain-emptor-no-thoughts

Dr. Bronners 7-in-1 trees

Day 4 done! The parsing is starting to get trickier; luckily each line fits inside of a 128-bit wide vector. The real frustration this time was the lack of non-strict comparison operators; you don't get _mm_cmple_epi32_mask until AVX-512 😠