# Archives

Here you can find all my previous posts:
• A quickie: Boundaries in Cubical Agda August 29, 2022

Wonderfully vague title, yes? As some of you might know, I’m now maintaining the implementation of Cubical Agda. Undoubtedly, if you know, it’s because I’ve been talking your ear off about it: I’m sorry. The “little kid with new toy” energy will continue until morale improves.

• 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 $G$, 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.

• Cubical Type Theory March 7, 2021

Hello, everyone! It’s been a while, hasn’t it? Somehow, after every post, I manage to convince myself that I’m gonna be better and not let a whole season go by between posts, but it never happens. For the last two posts I’ve been going on at length about fancy type theories, and this post, as the title implies, is no exception. In fact, two posts ago I mentioned, offhand, cubical type theory as a possibility for realising HoTT in a constructive way, but 128 days ago I did not understand cubical type theory in the slightest.

• On Induction January 15, 2021

Last time on this… thing… I update very occasionally, I talked about possible choices for representing equality in type theory. Equality is very important, since many properties of programs and mathematical operators are stated as equalities (e.g., in the definition of a group). However, expressing properties is useless if we can’t prove them, and this is where inductive types come in.

• Reflections on Equality October 30, 2020

When shopping for a dependent type theory, many factors should be taken into consideration: how inductive data is represented (inductive schemas vs W-types), how inductive data computes (eliminators vs case trees), how types of types are represented (universes à la Tarski vs à la Russell). However, the most important is their treatment of equality.

• The Semantics of Evaluation & Continuations July 12, 2020

Continuations are a criminally underappreciated language feature. Very few languages (off the top of my head: most Scheme dialects, some Standard ML implementations, and Ruby) support the—already very expressive—undelimited continuations—the kind introduced by call/cc—and even fewer implement the more expressive delimited continuations. Continuations (and tail recursion) can, in a first-class, functional way, express all local and non-local control features, and are an integral part of efficient implementations of algebraic effects systems, both as language features and (most importantly) as libraries.

• The G-machine In Detail, or How Lazy Evaluation Works January 31, 2020

With Haskell now more popular than ever, a great deal of programmers deal with lazy evaluation in their daily lives. They’re aware of the pitfalls of lazy I/O, know not to use foldl, and are masters at introducing bang patterns in the right place. But very few programmers know the magic behind lazy evaluation—graph reduction.

• A Quickie: A Use Case for Impredicative Polymorphism October 19, 2019

Amulet now (as of the 18th of October) has support for impredicative polymorphism based on Quick Look impredicativity, an algorithm first proposed for GHC that treats inference of applications as a two-step process to enable inferring impredicative types.

• Typed Type-Level Computation in Amulet October 4, 2019

Amulet, as a programming language, has a focus on strong static typing. This has led us to adopt many features inspired by dependently-typed languages, the most prominent of which being typed holes and GADTs, the latter being an imitation of indexed families.

• Interactive amc-prove September 29, 2019

Following my last post announcing amc-prove, I decided I’d make it more accessible to people who wouldn’t like to spend almost 10 minutes compiling Haskell code just to play with a fiddly prover.

• Announcement: amc-prove September 25, 2019

amc-prove is a smallish tool to automatically prove (some) sentences of constructive quantifier-free first-order logic using the Amulet compiler’s capability to suggest replacements for typed holes.

• A Quickie: Manipulating Records in Amulet September 22, 2019

Amulet, unlike some other languages, has records figured out. Much like in ML (and PureScript), they are their own, first-class entities in the language as opposed to being syntax sugar for defining a product constructor and projection functions.

• Compositional Typing for ML January 28, 2019

Compositional type-checking is a neat technique that I first saw in a paper by Olaf Chitil. He introduces a system of principal typings, as opposed to a system of principal types, as a way to address the bad type errors that many functional programming languages with type systems based on Hindley-Milner suffer from.

• Amulet updates August 11, 2018

Jesus, it’s been a while. Though my last post was almost 6 months ago (give or take a few), I’ve been busy working on Amulet, which continues to grow, almost an eldritch abomination you try desperately, but fail, to kill.

• GADTs and Amulet March 27, 2018

Dependent types are a very useful feature - the gold standard of enforcing invariants at compile time. However, they are still very much not practical, especially considering inference for unrestricted dependent types is equivalent to higher-order unification, which was proven to be undecidable.

• Amulet and Language Safety March 14, 2018

Ever since its inception, Amulet has strived to be a language that guarantees safety, to some extent, with its strong, static, inferred type system. Through polymorphism we gain the concept of parametricity, as explained in Philip Wadler’s Theorems for Free: a function’s behaviour does not depend on the instantiations you perform.

• Amulet's New Type Checker February 18, 2018

In the last post about Amulet I wrote about rewriting the type checking code. And, to everybody’s surprise (including myself), I actually did it.

Like all good programming languages, Amulet has a strong, static type system. What most other languages do not have, however, is (mostly) full type inference: programs are still type-checked despite (mostly) having no type annotations.

• The Amulet Programming Language January 18, 2018

As you might have noticed, I like designing and implementing programming languages. This is another of these projects. Amulet is a strictly-evaluated, statically typed impure roughly functional programming language with support for parametric data types and rank-1 polymorphism à la Hindley-Milner (but no let-generalization), along with row-polymorphic records. While syntactically inspired by the ML family, it’s a disservice to those languages to group Amulet with them, mostly because of the (present) lack of modules.

• Dependent Types September 8, 2017

Dependent types are pretty cool, yo. This post is a semi-structured ramble about dtt, a small dependently-typed “programming language” inspired by Thierry Coquand’s Calculus of (inductive) Constructions (though, note that the induction part is still lacking: There is support for defining inductive data types, and destructuring them by pattern matching, but since there’s no totality checker, recursion is disallowed).

• Multimethods in Urn August 15, 2017

multimethod, noun. A procedure which decides runtime behaviour based on the types of its arguments.

• Optimisation through Constraint Propagation August 6, 2017

Constraint propagation is a new optimisation proposed for implementation in the Urn compiler. It is a variation on the idea of flow-sensitive typing in that it is not applied to increasing program safety, rather being used to improve speed.

• The Urn Pattern Matching Library August 2, 2017

Efficient compilation of pattern matching is not exactly an open problem in computer science in the same way that implementing say, type systems, might be, but it’s still definitely possible to see a lot of mysticism surrounding it.

• Delimited Continuations, Urn and Lua August 1, 2017

As some of you might know, Urn is my current pet project. This means that any potential upcoming blag posts are going to involve it in some way or another, and that includes this one. For the uninitiated, Urn is a programming language which compiles to Lua, in the Lisp tradition, with no clear ascendance: We take inspiration from several Lisps, most notably Common Lisp and Scheme.

• Monadic Parsing with User State August 26, 2016

In this post I propose an extension to the monadic parser framework introduced in a previous post, You could have invented Parsec, that extends the parser to also support embedded user state in your parsing.

This could be used, for example, for parsing a language with user-extensible operators: The precedences and fixidities of operators would be kept in a hashmap threaded along the bind chain.

• Dependent types in Haskell - Sort of August 23, 2016

Warning: An intermediate level of type-fu is necessary for understanding *this post.

The glorious Glasgow Haskell Compilation system, since around version 6.10 has had support for indexed type familes, which let us represent functional relationships between types. Since around version 7, it has also supported datatype-kind promotion, which lifts arbitrary data declarations to types. Since version 8, it has supported an extension called TypeInType, which unifies the kind and type level.

• You could have invented Parsec August 17, 2016

As most of us should know, Parsec is a relatively fast, lightweight monadic parser combinator library.

In this post I aim to show that monadic parsing is not only useful, but a simple concept to grok.