@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.
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)
I have spent literally 2 hours recompiling agda over and over because of this goddamn library
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
SIMD Advent of Code
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 😠
Type Theory/Category Theory
I like proof assistants and make them too!
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.