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
your bike

and whose
colour you
liked a bit

Forgive me
this feature proposal
had changes to
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 (

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

This is the start of a series of threads about cofibrations.

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

Show thread

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.

"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

Show thread

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

SIMD Advent of Code 

Day 5 done:

This one was pretty annoying because things kept not /quite/ fitting in various vectors. I could definitely optimize further, but it only takes 15 microseconds so I cannot be bothered.

SIMD Advent of Code 

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 😠


Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.