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