Recent content on Daniel's Blog
Humid air swirls with colorful spirits. They trace its invisible currents in spirals through open spaces, cling to branches, drip down stone faces and, awakened by the first beams of the rising sun, ooze newly out of trees like sap. Lulls of wind leave them gliding gently downward to be picked up again. From a distance, eddies of the spirits’ malleable confetti travel along plains. With…
In the previous post in this series , I wrote about a little utility I created for detecting underlined words in a book and creating vocabulary study material for them. Like I mentioned earlier, this was one of my earliest experiences with LLM-driven development, and I think it shaped my outlook on the technology quite a bit. For me, the bottom line is this: with LLMs, I was able to rapidly solve…
TL;DR : I, with the help of ChatGPT, wrote a program that helps me extract vocabulary words from PDFs. Scroll just a bit further down to see what it looks like. Sometime in 2020 or 2021, during the COVID-19 pandemic, I overheard from some source that Albert Camus, in his book La Peste (The Plague), had quite accurately described the experience that many of us were going through at the time. Having…
Whenever I stay still, I feel the spiders weave their webs around me. Their tiny legs entangle me in silk, traverse my body as they seem to proudly inspect their work and into darkness sink. There're times I see the spiders' threads on others, They shimmer gently in the purple dusk, Or sway with zephyrs in the hair of lovers, stuck. To listen to the webs is to hear echoes of social butterflies…
I work at HPE on the Chapel Programming Language . Recently, another HPE person asked me: So, you work on the programming language. What’s next for you? This caught me off-guard because I hadn’t even conceived of moving on. I don’t want to move on, because I love the field of programming languages . In addition, I have come to think there is something in PL for everyone, from…
One day, when I was in graduate school, the Programming Languages research group was in a pub for a little gathering. Amidst beers, fries, and overpriced sandwiches, the professor and I were talking about dependent types . Speaking loosely and imprecisely, these are types that are somehow constructed from values in a language, like numbers. For example, in C++, std::array is a dependent type. An…
In the previous post, we put together a number of powerful pieces of machinery to construct a sign analysis. However, we still haven’t verified that this analysis produces correct results. For the most part, we already have the tools required to demonstrate correctness; the most important one is the validity of our CFGs relative to the semantics of the little language . High-Level Algorithm…
In the previous post, I showed that the Control Flow graphs we built of our programs match how they are really executed. This means that we can rely on these graphs to compute program information. In this post, we finally get to compute that information. Here’s a quick bit paraphrasing from last time that provides a summary of our approach: We will construct a finite-height lattice. Every…
In the previous two posts, I covered two ways of looking at programs in my little toy language: In part 5 , I covered the formal semantics of the programming language. These are precise rules that describe how programs are executed. These serve as the source of truth for what each statement and expression does. Because they are the source of truth, they capture all information about how programs…
In the previous section, I’ve given a formal definition of the programming language that I’ve been trying to analyze. This formal definition serves as the “ground truth” for how our little imperative programs are executed; however, program analyses (especially in practice) seldom take the formal semantics as input. Instead, they focus on more pragmatic program…
In the previous several posts, I’ve formalized the notion of lattices, which are an essential ingredient to formalizing the analyses in Anders Møller’s lecture notes. However, there can be no program analysis without a program to analyze! In this post, I will define the (very simple) language that we will be analyzing. An essential aspect of the language is its semantics , which simply…
In the preivous post we looked at lattices of finite height, which are a crucial ingredient to our static analyses. In this post, I will describe the specific algorithm that makes use of these lattices; this algorithm will be at the core of this series. Lattice-based static analyses tend to operate by iteratively combining facts from the program into new ones. For instance, when analyzing y = 1 +…
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. As a first example, natural numbers form a lattice , but they are not a finite-height lattice ; the following chain can be made infinitely long: $$ 0 < 1 < 2 < ... $$ There isn’t a “biggest natural number”! On the other…
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). One instance of the…
I’m losing my edge to the art-school Brooklynites in little jackets and borrowed nostalgia for the unremembered Eighties The Everpresent Void was first discovered at a children’s birthday party. Among the laughter and alluring warbling of an arcade, a party was preparing to take their seats at a worn table. The food was french fries, mediocre cheese pizza, and hamburgers; the sort of…
This is the first post in a series on static program analysis in Agda . See the introduction for a little bit more context. The goal of this post is to motivate the algebraic structure called a lattice . Lattices have broad applications [note: See, for instance, Lars Hupel's excellent introduction to CRDTs which uses lattices for Conflict-Free Replicated Data Types. CRDTs can be used to implement…
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. The group didn’t end up reading the lecture notes, but I did. As I was going through them, I noticed that they were quite rigorous: the first several chapters cover a little bit of lattice theory , and the subsequent analyses…
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. Hillel’s premise was that language designers tend to focus on the first two; however, because the convenience…
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.List.Properties ; they just give the code from a particular Agda file, but make every identifier clickable. Then, if you see some variable or function that you don’t know, you can just click it and jump right to it! It makes exploring the documentation a lot…
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. Recently, I came up with a little trick to help simplify some of my proofs, and it seems like this trick might have broader applications. In my head, I call this trick ‘Deeply Embedded Expressions’. Before I introduce it, let me explain…
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. The first question to get out of the way is “what on earth is an inference rule?”. The answer is simple: an inference rule is just a way of writing “if … then …”. When writing an inference rule, we…
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. However, it feels like the pattern is relatively unknown, so I thought I’d show it off, and some of its applications in the Chapel compiler . I’ve slightly tweaked a…
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. However, the languages are sufficiently different to leave room for useful design patterns in Agda that can’t be brought over from Haskell, because they don’t exist there. One such pattern will be the focus…
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. The code is “mine” in the sense that I was debugging changes I was making, and perhaps also in the sense that I was working with it. I work as a compiler developer on the Chapel team. Recently, while…
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. However, one particular insight I gleaned from the paper merits additional discussion and demonstration. I’m going to…
Have you encountered Haskell’s foldr function? Did you know that you can use it to express any function on a list? What’s more, there’s a way to derive similar functions for a large class of data types in Haskell. [note: Specifically, this is the class of inductive types . ] This is precisely the focus of this post. Before we get into the details, it’s good to review the…
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™. [note: The results of the PCR test are pending at the time of writing. ] In seeming correspondence with the progression of my cold, a thought occurred in the back of my mind: “ Your blog deployment is kind…
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. “Pick a number” , he said, “And I’ll teach you how to draw a pattern from it.” The procedure was rather simple: Pick a number between 2 and 8 (inclusive). Start generating…
I wanted to briefly introduce a project that I’ve been working on in my spare time over the past couple of months. It’s called Matrix Highlight , though this is a working title. However, it does exactly what the title claims: this little project is a browser extension to annotate the web, using Matrix as a communication and storage protocol. My goal with this project is a…
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. Though I’m quite happy with how that turned out, my article was missing something that’s present on the original Dawn page – an evaluator. In this article, I’ll define an evaluator function 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. The core calculus is called the untyped concatenative calculus , or UCC. The definitions in the semantics seemed so clean and straightforward that I wanted to try my hand at translating them into machine-checked code. I am most…
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. Today, I’m going to share a little trick I’ve discovered which allows me to do something that I suspect would normally require dependent types . The Problem Suppose you want to…
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. In particular, I wanted to display links to the files I’m referring to, in three different cases: when I’m referring to an entire code file, to an entire raw (non-highlighted) file, or to a portion of a…
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. I’ve since improved on this some more, so I thought I’d share what I created with others. Including…
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. Day 7 got close, but not close enough to inspire me to create a formalization. Day 8, on the other hand, is quite interesting, [note: Especially to someone like me who's interested in programming languages! ] and took quite some time to…
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!” At first, I wanted to formalize and prove the correctness of the two-pointer solution . However, I didn’t have the time to mess around with the various properties of sorted lists and their traversals. So, I settled for the brute…
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. The language consisted of very few constructs, and was very much a “toy”. On the expression side of things, it had three registers ( A , B , and R ), numbers, addition, comparison using “less than”,…
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. Now is the time to do that. In particular, I identified four things that could be improved or cleaned up: Error handling . We need to stop using throw 0 and start using assert . We can…
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. Some had been pretty standard: “What’s the difference between concurrency and parallelism?” – a reasonable question given that Go was the company’s language of choice. “What’s the…
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 . In these posts, I described a hypothetical way of ’typechecking’ an expression data type Expr into a typesafe form SafeExpr . A SafeExpr can be evaluated without any code to handle type errors, since it’s by…
I recently got to use a very curious Haskell technique in production: [note: As production as research code gets, anyway! ] time traveling. I say this with the utmost seriousness. This technique worked like magic for the problem I was trying to solve, and so I thought I’d share what I learned. In addition to the technique and its workings, I will also explain how time traveling can be…
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. However, sometimes, ripples from these areas make their way into my life, and this is one such instance. Let me tell you a story [note: I originally wrote about this in a thread on DELL's support website . Some of this post is going to be adapted…
Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris . The gist of the post was as follows: Programming Language Fundamentals students were surprised that, despite having run their expression through (object language) typechecking, they still had to have a Maybe type in their evaluation functions. This was due to the fact that the (meta language) type system was not…
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. It was, in some way, enlightening. The things that I used to take for granted with a ‘powerful’ machine now became a rare luxury: StackOverflow, and other relatively static websites, took upwards of ten seconds to finish…
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. I’ve been mentioning let/in and lambda expressions for a while now. The former will let us create names for expressions that are limited to a certain scope (without having to create global variable bindings), while the latter will…
As I’ve described in my previous post , the process for compiling a Crystal project with Nix is a fairly straightforward one. As is standard within the Nix ecosystem, the project’s dependencies, as specified by the source language’s build system (shards, in Crystal’s case), are converted into a Nix expression ( shards.nix ). These dependencies are then used in a derivation,…
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 . This means that we cannot construct data structures that can contain arbitrary types. While we can define and use a list of integers, if we want to…
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. Suppose we didn’t want to add a special if/else expression into our language. Thanks to lazy evaluation, we can express it using a function: defn if c t e…
Since I first started working on my website at age fourteen, the site has gone through many revisions, and hopefully changed for the better. This blog was originally dynamically served using a Python/Flask backend, having a custom login system and post “editor” (just an input box). One of the more strange things about my website, though, was how I displayed content. It was clear to me,…
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: Recursion/loops, . . . [and] . . . Procedures/functions with arguments (or some other abstraction mechanism) A while-loop makes enough sense. The most straightforward way to…