Archives

Translating mathematics into code that a proof assistant can understand is a process that involves a fair bit of friction. There’s quite a big difference between what humans are willing to suspend disbelief about, and what a type checker will actually accept without proof. Reducing this friction is the primary task of the authors of a proof assistant — but, of course, it would be infeasible to modify the proof assistant itself to cover a new problem domain every time one comes up. To this end, we provide users with various mechanisms for automation, through which users can encode their domain-specific knowledge.

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.

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:

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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 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.

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.

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.

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.

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.

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 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).

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

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.

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.

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.

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.

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.

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.