3 Jun 2024
Chorex is a brand-new Elixir library for choreographic programming [3]: Chorex provides a macro-based DSL that lets you describe how processes communicate to perform a computation. This top-down description of interacting processes is called a choreography. From this choreography, Chorex creates modules for each process that handle all the message-passing in the system. The interactions performed by the generated code will never deadlock by construction because the choreographic DSL ensures that no processes will be waiting on each other at the same time.
...
30 Oct 2023
Something I’ve wondered about for a little while: why don’t more languages have a call/cc operator? Having first-class continuations in your programming language gives your programmers a powerful construct. So why do only a handful of languages have it?
The short answer is: it’s tricky to implement efficiently. One way to get call/cc is to convert your code into continuation-passing style. Then, call/cc simply takes the continuation in that representation and binds it to a variable. Most languages don’t seem to go through a continuation-passing style conversion pass though, so there’s no continuation to grab.
...
2 Oct 2023
Or: Approaching the Y Combinator
These are some of my class notes. Learning to derive the Y Combinator from first principles is something I’ve always wanted to do. This isn’t quite the Y Combinator, but it’s very close and it still gets you recursion without relying on recursive structures to begin with.
In the beginning, we write a recursive function to compute the length of a list:
(let* ([len (λ (lst)
(if (null? lst)
0
(+ 1 (len (cdr lst)))))])
(len '(1 2 3)))
The let* syntax allows us to create local variable bindings that can reference themselves. But let’s suppose we don’t have let*—what do we do?
...
14 Aug 2023
There’s a neat paper Type Systems as Macros by Chang, Knauth, and Greenman [1] that describes how to implement a typed language using an untyped host language and macro expansion. The paper is neat, but I found the code hard to follow—the paper uses a compact notation that’s convenient for print, but not so much for reproducing on one’s own. This post is my attempt to implement and explain in more accessible terms what’s presented in the paper.
...
5 Aug 2023
I started my PhD program about a year ago. In my first year I have:
- Taken 4 “normal” 3-credit-hour classes
- Participated in 3 seminars
- Switched advisors
- Attended 2 conferences (PLDI @ FCRC, JuliaCon)
- Presented my work at JuliaCon
It’s been a lot of work, and there’s been a lot of stress. I’m in a much better place now than when I started, and over all I’m happy where I’m at and where I’m headed.
...
19 May 2023
There are a bunch of different ways of writing a macro in Racket. There are also some tricky things around phases to keep in mind. This is to help me keep them all straight.
...
11 May 2023
I believe computer science plays as integral of a part to a well-rounded liberal arts education as does mathematics and linguistics. Why? A liberal arts education is designed to help you think in new and better ways. Computer science teaches novel ways of thinking, reasoning, and approaching problems that are hard to get anywhere else.
I took a class on pedagogy when I encountered this puzzle. I answered the question easily, and I caught myself using reasoning patterns from work in programming coming to the forefront.
...
23 Jan 2023
Background
#
This is a question I’ve been wrestling with for a little bit. My first experience with a type system was with Java, and I didn’t like it. It just felt like an annoying constraint on the kinds of programs I could write. I was coming from Perl, which sports weak dynamic typing, so Java’s rigidity came as a bit of a shock.
After Java I learned some C, which too has types. C’s types are different from Java’s in a big way: in C they’re really just directives to the compiler on how to interpret some bytes. “Everything is just void *” is kind of true. In C, bytes can be interpreted however you wish.
...
27 Jul 2022
This is an experimental type checker/inferer for a simple lambda calculus. All the source for this may be found on my Codeberg repository.
...
2 Mar 2022
I have a hard time keeping these terms straight:
- liveness vs. safety
- soundness vs. completeness
This is intended as a short guide for myself; maybe someone else will find it useful too! Note that this is all to the best of my knowledge and understanding at the present time; if there be faults, they be the faults of myself. I welcome correction and clarification if I am wrong.
Liveness vs. Safety
#
Liveness and safety deal with properties of a system. Contrast that with soundness and completion, which are adjectives about analyses.
...