Reed Mullanix @totbwf@types.pl

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.

This is just to say

I have painted
the shed
that was housing
your bike

and whose
colour you
probably
liked a bit

Forgive me
this feature proposal
had changes to
the language syntax

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 (https://arxiv.org/abs/2210.08663)

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.

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.
https://www.plai.org/

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