# Daniel's Blog

## Posts

On this page you can see every article on this blog in reverse chronological order. If you like pretty colors and patterns, you can also see a visualization of all the articles and links between them on the content graph page. If you have something specific in mind, you can also try using the search page.

• Implementing and Verifying "Static Program Analysis" in Agda, Part 3: Lattices of Finite Height

In the previous post, I introduced the class of finite-height lattices: lattices where chains made from elements and the less-than operator < can only be so long. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 2: Combining Lattices

In the previous post, I wrote about how lattices arise when tracking, comparing and combining static information about programs. I then showed two simple lattices: the natural numbers, and the (parameterized) “above-below” lattice, which modified an arbitrary set with “bottom” and “top” elements ($\bot$ and $\top$ respectively). ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 1: Lattices

This is the first post in a series on static program analysis in Agda. See the introduction for a little bit more context. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 0: Intro

Some years ago, when the Programming Languages research group at Oregon State University was discussing what to read, the Static Program Analysis lecture notes came up. ...

• Microfeatures I Love in Blogs and Personal Websites

Some time ago, Hillel Wayne published an article titled Microfeatures I’d like to see in more languages . In this article, he described three kinds of features in programming languages: fundamental features, deeply engrained features, and nice-to-have convenience features. ...

• Integrating Agda's HTML Output with Hugo

One of my favorite things about Agda are its clickable HTML pages. If you don’t know what they are, that’s pages like Data. ...

• The "Deeply Embedded Expression" Trick in Agda

I’ve been working on a relatively large Agda project for a few months now, and I’d like to think that I’ve become quite proficient. ...

• Bergamot: Exploring Programming Language Inference Rules

Inference Rules and the Study of Programming Languages In this post, I will talk about inference rules, particularly in the field of programming language theory. ...

• My Favorite C++ Pattern: X Macros

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

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

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

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

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

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

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

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

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

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

• Type-Safe Event Emitter in TypeScript

I’ve been playing around with TypeScript recently, and enjoying it too. Nearly all of my compile-time type safety desires have been accomodated by the language, and in a rather intuitive and clean way. ...

• Approximating Custom Functions in Hugo

This will be an uncharacteristically short post. Recently, I wrote about my experience with including code from local files. After I wrote that post, I decided to expand upon my setup. ...

• Pleasant Code Includes with Hugo

Ever since I started the compiler series, I began to include more and more fragments of code into my blog. I didn’t want to be copy-pasting my code between my project and my Markdown files, so I quickly wrote up a Hugo shortcode to pull in other files in the local directory. ...

• Advent of Code in Coq - Day 8

Huh? We’re on day 8? What happened to days 2 through 7? Well, for the most part, I didn’t think they were that interesting from the Coq point of view. ...

• Advent of Code in Coq - Day 1

The first puzzle of this year’s Advent of Code was quite simple, which gave me a thought: “Hey, this feels within reach for me to formally verify! ...

• A Typesafe Representation of an Imperative Language

A recent homework assignment for my university’s programming languages course was to encode the abstract syntax for a small imperative language into Haskell data types. ...

• Compiling a Functional Language Using C++, Part 13 - Cleanup

In part 12, we added let/in and lambda expressions to our compiler. At the end of that post, I mentioned that before we move on to bigger and better things, I wanted to take a step back and clean up the compiler. ...

• How Many Values Does a Boolean Have?

A friend of mine recently had an interview for a software engineering position. They later recounted to me the content of the technical questions that they had been asked. ...

• Meaningfully Typechecking a Language in Idris, With Tuples

Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. I then followed it up with Meaningfully Typechecking a Language in Idris, Revisited. ...

• Time Traveling In Haskell: How It Works And How To Use It

I recently got to use a very curious Haskell technique in production: [note: As production as research code gets, anyway! ] time traveling. ...

• DELL Is A Horrible Company And You Should Avoid Them At All Costs

I really do not want this to be a consumer electronics blog. Such things aren’t interesting to me, and nor do I have much knowledge about them. ...

• Meaningfully Typechecking a Language in Idris, Revisited

Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. The gist of the post was as follows: ...

• Rendering Mathematics On The Back End

Due to something of a streak of bad luck when it came to computers, I spent a significant amount of time using a Linux-based Chromebook, and then a Pinebook Pro. ...

• Compiling a Functional Language Using C++, Part 12 - Let/In and Lambdas

Now that our language’s type system is more fleshed out and pleasant to use, it’s time to shift our focus to the ergonomics of the language itself. ...

• Building a Crystal Project with Nix, Revisited

As I’ve described in my previous post, the process for compiling a Crystal project with Nix is a fairly straightforward one. ...

• Compiling a Functional Language Using C++, Part 11 - Polymorphic Data Types

In part 10, we managed to get our compiler to accept functions that were polymorphically typed. However, a piece of the puzzle is still missing: while our functions can handle values of different types, the same cannot be said for our data types. ...

• Compiling a Functional Language Using C++, Part 10 - Polymorphism

In part 8, we wrote some pretty interesting programs in our little language. We successfully expressed arithmetic and recursion. But there’s one thing that we cannot express in our language without further changes: an if statement. ...

• Math Rendering is Wrong

Since I first started working on my website at age fourteen, the site has gone through many revisions, and hopefully changed for the better. ...

• Creating Recursive Functions in a Stack Based Language

In CS 381, Programming Language Fundamentals, many students chose to implement a stack based language. Such languages are very neat, but two of the requirements for such languages may, at first, seem somewhat hard to satisfy: ...

• Meaningfully Typechecking a Language in Idris

This term, I’m a TA for Oregon State University’s Programming Languages course. The students in the course are tasked with using Haskell to implement a programming language of their own design. ...

• Building a Basic Crystal Project with Nix

I really like the idea of Nix: you can have reproducible builds, written more or less declaratively. I also really like the programming language Crystal , which is a compiled Ruby derivative. ...

• Compiling a Functional Language Using C++, Part 9 - Garbage Collection

“When will you learn? When will you learn that your actions have consequences?” So far, we’ve entirely ignored the problem of memory management. ...

• Using GHC IDE for Haskell Error Checking and Autocompletion

Last year, when I took Oregon State University’s CS 381 class, I ended up setting up my editor with the Haskell IDE engine. ...

• A Language for an Assignment - Homework 3

It rained in Sunriver on New Year’s Eve, and it continued to rain for the next couple of days. So, instead of going skiing as planned, to the dismay of my family and friends, I spent the majority of those days working on the third language for homework 3. ...

• A Language for an Assignment - Homework 2

After the madness of the language for homework 1, the solution to the second homework offers a moment of respite. Let’s get right into the problems, shall we? ...

• A Language for an Assignment - Homework 1

On a rainy Oregon day, I was walking between classes with a group of friends. We were discussing the various ways to obfuscate solutions to the weekly homework assignments in our Algorithms course: replace every if with a ternary expression, use single variable names, put everything on one line. ...

• JavaScript-Free Sidenotes in Hugo

A friend recently showed me a website, the design of which I really liked: Gwern Branwen’s personal website . In particular, I found that sidenotes were a feature that I didn’t even know I needed. ...

• Compiling a Functional Language Using C++, Part 8 - LLVM

We don’t want a compiler that can only generate code for a single platform. Our language should work on macOS, Windows, and Linux, on x86_64, ARM, and maybe some other architectures. ...

• Thoughts on Better Explanations

How do you explain how to write a program? Instructional material is becoming more and more popular on the web, with thousands of programming tutorials for languages, frameworks, and technologies created on YouTube, Medium, and peole’s personal sites. ...

• Compiling a Functional Language Using C++, Part 7 - Runtime

Wikipedia has the following definition for a runtime: A [runtime] primarily implements portions of an execution model. We know what our execution model is! ...

• Compiling a Functional Language Using C++, Part 6 - Compilation

In the previous post, we defined a machine for graph reduction, called a G-machine. However, this machine is still not particularly connected to our language. ...

• Compiling a Functional Language Using C++, Part 5 - Execution

We now have trees representing valid programs in our language, and it’s time to think about how to compile them into machine code, to be executed on hardware. ...

• Compiling a Functional Language Using C++, Part 4 - Small Improvements

We’ve done quite a big push in the previous post. We defined type rules for our language, implemented unification, and then implemented unification to enforce these rules for our program. ...

• Compiling a Functional Language Using C++, Part 3 - Type Checking

I think tokenizing and parsing are boring. The thing is, looking at syntax is a pretty shallow measure of how interesting a language is. ...

• Switching to a Static Site Generator

A long time ago, I decided to try out Jekyll for my website. However, it all felt too convoluted: the ruby gems I needed to install, the configuration options for the site, the theming. ...

• Compiling a Functional Language Using C++, Part 2 - Parsing

In the previous post, we covered tokenizing. We learned how to convert an input string into logical segments, and even wrote up a tokenizer to do it according to the rules of our language. ...

• Compiling a Functional Language Using C++, Part 1 - Tokenizing

It makes sense to build a compiler bit by bit, following the stages we outlined in the first post of the series. ...

• Compiling a Functional Language Using C++, Part 0 - Intro

During my last academic term, I was enrolled in a compilers course. We had a final project - develop a compiler for a basic Python subset, using LLVM. ...

• Local Development Environment for JOS and CS 444

Working with the instructor’s dotfiles on the server is great and all, but there’s a few things you can do loccally that you can’t do on the school server: ...

• Lambda Calculus and Church Encoded Integers

You always hear the words “turning complete” thrown around in various contexts. Powerpoint is Turing complete, CSS is Turing complete. Turing completeness effectively describes a property of a language of system to perform any computation that can be performed on a computer (or by a human with a piece of paper). ...

• Proof of Inductive Palindrome Definition in Coq

Going through the Software Foundations textbook, I found an exercise which I really enjoyed solving. This exercise was to define an inductive property that holds iff a list is a palindrome. ...

• Setting Up Crystal on ARM

Having found myself using a Chromebook with Arch Linux, I acutely felt the lack of official Crystal builds for ARM. After spending an hour or so looking online for a comprehensive guide to getting a working compiler on ARM, I think I now know the general idea. ...

• Haskell Error Checking and Autocompletion With LSP

For Oregon State University’s CS 381, Programming Language Fundamentals, Haskell is the language of choice. While it has an excellent REPL, and an excellent compiler, a piece of the puzzle is missing when writing Haskell code: on-the-fly error checking. ...

• A Look Into Starbound's File Formats

After playing a few hours of Starbound, I decided that I wanted to mess around with its file format, perhaps make a save manager/swapper, or something. ...

• New Look, New Features!

I’ve recently taken the time to redesign my website from scratch, on both the back-end and the front-end! On the back-end, this means the addition of tags, which allow me to categorize the not-so-plentiful content on the site. ...

• Learning Emulation, Part 2.5 - Implementation

This is the third post in a series I’m writing about Chip-8 emulation. If you want to see the first one, head here. ...

• Learning Emulation, Part 2