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.
...
17 Nov 2022
I had a friend ask me what continuations are, and why they're useful.
There's a ton of literature about continuations; this is just a simple example meant to showcase something small and hopefully grokkable.
You will need to understand a little bit of Racket, but if you know any Scheme, that should be good enough. If you just want a quick primer, check out Learn X in Y minutes for Racket.
#lang racket
;;; Export these symbols
(provide fail pick non-deterministic-factor)
;;; Global stack of choices (only visible to this module)
(define *choices* '())
;;; Pop a value off of the alternate choices stack
(define (fail)
(if (null? *choices*)
#f
(let ([next-choice (car *choices*)])
(set! *choices* (cdr *choices*))
(next-choice))))
This next function pick is where we capture the continuation. I've named it
return-from-pick to illustrate that when you call this function, it
will jump back to the point in the code where pick returns.
However, this works even if you use the continuation after the
thing the called pick itself has returned.
...
27 Jul 2022
All the source for this may be found on my Codeberg repository.
Synopsis
#
Experimental type checker/inferer for a simple lambda calculus
Description
#
This is a type inference system for a little language. (Described below.) It uses a fusion of type inference algorithms from PLAI, ESP, and μKanren. (See Resources)
Broadly speaking, our type inference engine works by:
- generating typing constraints from the program
- solving those constraints
We’ll describe each of those in more detail.
...
4 Jul 2022
μKanren (“micro-Kanren”) is a tiny, embeddable logic programming language. It’s easy to understand and implement in almost any language. It’s a great case study of an embedded language: unlike other common “embedded” languages like SQL or regex, which normally are represented as just plain-old strings, μKanren takes more advantage of the host language’s features.
I recommend reading the original paper: it’s short, well-written, and easy to understand.
I did a write-up which you can read on Codeberg. The README is my set of notes that I made while walking through the implementation of the paper, and the repository contains an implementation in Racket. I’ve included some fun use cases like a type checker/inference engine that takes up only 37 lines of code!
...
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.
...
24 Oct 2021
Last week I was studying outside of a lecture hall where someone was teaching an introductory course on computer programming. There was a lot that I overheard that I disagreed with; this essay is an attempt to help me crystallize what exactly I disagreed with.
...
4 Aug 2020
I’ve been thinking about programming languages a lot recently. A question I asked myself was: why do we work on, refine, and create new programming languages?
I thought of several reasons, but they seemed to boil down into two broader reasons:
-
Better abstractions and more automation: some languages automate and ease some tedious tasks like memory management, concurrency, or type annotations. Almost all languages give you some ways of creating abstractions that let you reason with concepts in your problem domain, but different languages do this in different ways.
...
15 Jun 2020
An analogy occurred to me this evening as I was thinking about programming language design:
Choosing good keywords and function names is like picking a good font; the ideas conveyed may be the same, but a change can drastically impact legibility and enjoyment of use.
PHP does a spectacular job of providing a bad example. It’s like the Comic Sans of programming languages. Now there are many reasons why PHP is not a good language—I’d like to investigate this particular aspect of its design here briefly.
...