Daniel's Blog

Hello!

Welcome to my blog. Here, I write about various subjects, including (but not limited to) functional programming, compiler development, programming language theory, and occasionally video games. I hope you find something useful here!

• My Favorite C++ Pattern: X Macros

  4166 words, about 20 minutes to read.

  When I first joined the Chapel team, one pattern used in its C++-based compiler made a strong impression on me. Since then, I’ve used the pattern many more times, and have been very satisfied with how it turned out. . . .

• The "Is Something" Pattern in Agda

  1772 words, about 9 minutes to read.

  Agda is a functional programming language with a relatively Haskell-like syntax and feature set, so coming into it, I relied on my past experiences with Haskell to get things done. . . .

• Proving My Compiler Code Incorrect With Alloy

  6773 words, about 32 minutes to read.

  Disclaimer: though “my compiler code” makes for a fun title, I do not claim exclusive credit for any of the C++ code in the Chapel compiler that I mention in this post. . . .

• Search as a Polynomial

  3732 words, about 18 minutes to read.

  I read a really neat paper some time ago, and I’ve been wanting to write about it ever since. The paper is called Algebras for Weighted Search, and it is a tad too deep to dive into in a blog article – readers of ICFP are rarely the target audience on this site. . . .

• Generalizing Folds in Haskell

  3338 words, about 16 minutes to read.

  Have you encountered Haskell’s foldr function? Did you know that you can use it to express any function on a list? . . .

• Declaratively Deploying Multiple Blog Versions with NixOS and Flakes

  3560 words, about 17 minutes to read.

  Prologue You can skip this section if you’d like. For the last few days, I’ve been stuck inside of my room due to some kind of cold or flu, which or may or may not be COVID™. . . .

• Digit Sum Patterns and Modular Arithmetic

  6083 words, about 29 minutes to read.

  When I was in elementary school, our class was briefly visited by our school’s headmaster. He was there for a demonstration, probably intended to get us to practice our multiplication tables. . . .

• Introducing Matrix Highlight

  1069 words, about 6 minutes to read.

  I wanted to briefly introduce a project that I’ve been working on in my spare time over the past couple of months. . . .

• A Verified Evaluator for the Untyped Concatenative Calculus

  6793 words, about 32 minutes to read.

  Earlier, I wrote an article in which I used Coq to encode the formal semantics of Dawn’s Untyped Concatenative Calculus, and to prove a few things about the mini-language. . . .

• Formalizing Dawn in Coq

  4345 words, about 21 minutes to read.

  The Foundations of Dawn article came up on Lobsters recently. In this article, the author of Dawn defines a core calculus for the language, and provides its semantics. . . .