xeval
is a small and not particularly useful program that arose from an important thought process.
This post the result of exploring that thought process—trying to articulate it to myself—but without writing too much on the topic.
Agda's sized types are inconsistent.
This post is about why I care and how I've worked around it.
A lot of Nix projects end up with their own binary cache (also known as a “substituter”).
Nix can be quite slow when it’s configured to use many project-specific substituters,
because it queries them all when checking if it needs to build a derivation. In a specific
project, most of the other substituters Nix knows about are irrelevant, and querying them
is wasted effort. My solution is to only enable https://cache.nixos.org globally, and
to selectively enable other substituters while I’m working on a project that needs them.
Here’s how I do it.
Recently I’ve been tweaking the appearance of my desktop environment,
which consists of XMonad and Taffybar,
with LightDM as the display manager,
all tied together using NixOS and home-manager.
Reflections on 2023's hobby projects.
My experience playing the original Diablo for the first time.
Developing a variable binding library for Rust, based on the
theory of nominal sets.
The proofs for my Nominal Sets article.
Over the past few years I’ve become wary of a certain feeling related to my artistic hobbies
like drawing and music production: the sense of excitement and “motivation” after I’ve acquired
some new art-related material. It’s very easy to spend hours doodling with a new marker, writing
in a fresh journal, or twiddling with a synth I’ve just bought. The next day, though, the new tool
is a little less exciting, and so on, until it’s as normal as everything else.
I’ve just finished migrating this site from Jekyll to
Hakyll. The only noticeable changes are: slightly prettier page URLs, MathML support, and
tweaks to syntax highlighting to compensate for using Pandoc. I paid
special attention to preserving the Atom feed identifiers so that feed readers aren’t
impacted.
In
this
conversation,
Sam Harris and Cal Newport talked about
how we use the world wide web, how it has become extremely centralised around a few social media
platforms, and the role of recommendation algorithms in this system. Parts of this conversation are
starting to influence the way I use the web.
Reflections this year's hobby projects.
Dream.In.Code was a
programming help forum that ran from 2001 to the beginning of 2022. It was recently shut
down
due to hosting costs. My participation in Dream.In.Code, starting from 2009 and ending somewhere in
2013, represents the beginning of my life as a programmer. Over the past 10 or so years, programming
has become a huge part of my life. I’d like to acknowledge the role this forum played in my development.
I’ve recently been working on web a graphics project
where I played a Canvas API implementation
against a WebGL implementation. When running the app in Firefox on Linux, I was surprised to find that the WebGL version was 10-30% slower
(in frames per second) than the Canvas version.
I’m an experienced Haskell programmer, and I’ve been writing a lot of Rust lately.
I recently ran into a little trouble when porting a simple function from Haskell to
Rust. This article is a short description of my journey.
I’ve Googled this one too many times, so I’m writing it here for future reference.
Memory-sensitive languages like C++ and Rust use compile-time information to calculate
sizes of datatypes. These sizes are used to inform alignment, allocation, and calling conventions in ways
that improve runtime performance. Modern languages in this setting support generic types, but so far
these languages only allow parameterisation over types, not type constructors. In this article I describe
how to enable parameterisation over arbitrary type constructs, while still retaining compile-time calculation
of datatype sizes.
I was first clued into this a while ago by
a comment on Bob Harper’s blog that “exponentials are coinductive”, but it only really clicked for me today. Let’s get into it.
I’ve been using Agda on NixOS for a while (mostly via agda-mode
in Emacs), but I remember it was a bit
difficult to get going the very first time. Hopefully this becomes a searchable reference
to getting it all set up quickly.
In this Twitter thread,
Eugenia Cheng talks about how she presented at a conference for women in STEM, and was
confronted by a white guy who felt ‘called out’ by some of her anecdotes. Apparently, she
described interactions with obnoxious individuals in a professional setting, and noted that
they were all white guys. Ironically, the guy raised the issue in such a way that he was added
to the list of anecdotes.
I remember when I first learned about computer programming, around 2008 or 2009.
I wanted to make games, and asked a search engine. Apparently computer graphics
was way too hard, so I decided I wanted to create browser-based static HTML
games and text-based roguelikes. Having learned that PHP and MySQL exist, I sat
down and brainstormed a setting, classes and roles for characters, and all the
other things that come with fantasy RPGs.
I think writing can help us think better.
In his propositions as types
talk, Philip Wadler contrasts
programming languages that have been ‘invented’ with those that have been
‘discovered’. “And you can tell!” he exclaims, receiving giggles from the
audience. Regardless of
how you feel about mathematical
platonism,
I think Phil is pointing at a meaningful difference in the way certain ideas
arise.
I love bound - it makes De
Bruijn indices mindlessly easy. I also love
Plated
for all sorts of whole-program transformations. I think they’re two
indispensible tools for working with programming languages.
Unfortunately, they’re not compatible.
A certain algorithmic puzzle website has a problem that goes like this…
It’s difficult to learn functional programming without hearing about continuations. Often they’re mentioned while talking about boosting the performance of pure functional code, sometimes there’s talk of control flow, and occasionally with ‘time-travel’ thrown in there to make it all seem more obscure. It’s all true, but let’s start from the beginning.
NixOS is a Linux distribution with declarative
configuration management. Your system configuration is specified in a
set of files, and can run a command to update your system to the current
specification. A consequence of this is that your entire system
configuration can be versioned.
Unification is a vital process in the implementation of Hindley-Damas-Milner
type inference. In the original paper
it is mentioned in passing as assumed knowledge, so here is an explanation of
unification in with a little help from the HM type theory.
LINQ is a system that provides a flexible query interface for .NET languages.
It allows a user to write queries over arbitrary data using an in-built
SQL-like syntax. This syntactic sugar is mapped to method calls at compile time,
so any data structure that implements the correct methods can be used with LINQ.
Last semester I had to write a static website by hand with no templating
resulting in a lot of duplicated code across multiple pages. I had already
finished most of the project when I realised that the main page of the
project should be named index.html
instead of home.html
. I renamed the
file, but that left me with countless references to “home.html” that needed
to be changed, and I wanted to change them all at once. Enter sed
.
With so many programming languages and frameworks at our disposal, it is
too easy to believe that knowledge of many tools is the defining characteristic
of a good programmer. However, many experienced programmers will assert that
it isn’t the languages you know, but your ability to solve problems that
defines you as a programmer.
Monad transformers combine the functionality of two monads into one. They are often used
as a way to “flatten” nested monads, but are also used to enable interactions between
monads that, when used seperately, would be incredibly difficult to implement.