Archives

Here you can find all my previous posts:

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

  Today’s note is about what is perhaps the most confusing rule of Groupoid Martin-Löf’s dependent type theory, the J eliminator. For starters, its name means basically nothing: as far as I can tell its name comes from the fact that Identity is another word for equality and J is the letter that comes after I.

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

  ---

  1. Technically, amc-prove “supports” the entire Amulet type system, which includes things like type-classes and rank-N types (it’s equal in expressive power to System F). However, the hole-filling logic is meant to aid the programmer while she codes, not exhaustively search for a solution, so it was written to fail early and fail fast instead of spending unbounded time searching for a solution that might not be there.↩︎

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

  ---

  1. Olaf Chitil. 2001. Compositional explanation of types and algorithmic debugging of type errors. In Proceedings of the sixth ACM SIGPLAN international conference on Functional programming (ICFP ’01). ACM, New York, NY, USA, 193-204. DOI.↩︎

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

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

  ---

  1. The relevant merge request can be found here.↩︎

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

  ---

  1. Though this might come off as a weird decision to some, there is a logical reason behind it: Urn was initially meant to be used in the ComputerCraft mod for Minecraft, which uses the Lua programming language, though the language has outgrown it by now. For example, the experimental readline support is being implemented with the LuaJIT foreign function interface.↩︎

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

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

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

• You could have invented Parsec August 17, 2016

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