Home

Hi!

profile picture I'm Amélia, a non-binary (they/them) mathematician & programmer. This blog is where I write about programming languages: their implementation, their semantics, etc.

cube In addition to this blog, I maintain the 1Lab, a formalised, cross-linked reference resource for Homotopy Type Theory, done in Cubical Agda.

amulet My most significant project other than this blog and the 1lab is Amulet, a functional programming language in the ML tradition with support for advanced type-level programming.

Posts

Here are the lastest 5 posts from the blog:

  • The Adjoint Functor Theorem in Everyday Life March 13, 2022

    Here’s a mathematical situation that comes up a lot more often than is reasonable. Suppose we have some mathematical object GG, generally defined as some structure on a set: a group, a ring, a topological space. These all have natural categorical structures, so we can - in a uniform way - talk about their subobjects:

  • The Complete History of isoToEquiv December 17, 2021

    It’s a standard fact in (higher) category theory and homotopy theory that any equivalence of categories (homotopy equivalence) can be improved to an adjoint equivalence of categories (strong homotopy equivalence). Adjoint equivalences (and strong homotopy equivalences) are “more structured” notions in the sense that the data of an adjoint equivalence is contractible if inhabited.

  • Parsing Layout, or: Haskell's Syntax is a Mess September 3, 2021

    Hello! Today we’re going to talk about something I’m actually good at, for a change: writing compilers. Specifically, I’m going to demonstrate how to wrangle Alex and Happy to implement a parser for a simple language with the same indentation sensitive parsing behaviour as Haskell, the layout rule.

  • Cubical Sets June 21, 2021

    In which I try to write about semantics. This is not gonna go well, but I’m gonna try my best. I’ve heard it on good authority that the best way to learn something is to explain it to someone else, so in this post I’m going to use you, dear reader, as my rubber duck while I try to understand cubical sets. These are important (to me) because they provide a semantic model of cubical type theory (which I have written about previously), and since we have a semantic model, that theory is (semantically) consistent.

  • A quickie: Axiom J June 7, 2021

    Hey y’all, it’s been three months since my last blog post! You know what that means.. or should mean, at least. Yes, I’d quite like to have another long blog post done, but… Life is kinda trash right now, no motivation for writing, whatever. So over the coming week(s) or so, as a coping mechanism for the chaos that is the end of the semester, I’m gonna write a couple of really short posts (like this one) that might not even be coherent at all—this sentence sure isn’t.

…or you can find more in the archives.