Aaron Eline

NJPLS 2026 Trip Report

Aaron Eline

•

May 26, 2026

Last Friday I attended NJPLS 2026 and wanted to write up some of the cool talks that I saw. I love NJPLS, the informal atmosphere and talks on work that is still in progress make for a great time. Many thanks to the organizers at Penn.

Principal Gradual Type Inference

David Van Horn talked about his work on Gradual Type Inference. If you’re not familiar with gradual typing, it’s the idea that you can intermix dynamic and static type checking in the same language. The pitch is often that you can start your project in the nice, loose, low-mental overhead world of dynamic types, and then as your project matures you can move things to static types piece by piece. The most popular gradually typed language is almost certainly TypeScript, which adds gradual typing to JavaScript.

Here’s an example: 

function foo(x : number): string {
    if (x === 0) {
        return "test";
    } else {
        return (x.toFixed()).toString();
    }
}

function bar(x) {
    return foo(x);
}

console.log(bar("test"));

The function foo is statically typed, but the function bar and the toplevel call to log are not. Interactions between the untyped code and typed code still necessitate runtime type checking, as there may be type errors. In fact, there is a type error in the above code! We pass "test" to foo despite it not being a number. The interesting wrinkle is where this type error is reported (or, who is “blamed”). If we run this code we get: 

TypeError: x.toFixed is not a function. (In 'x.toFixed()', 'x.toFixed' is undefined)

With a line number pointing to foo . This is somewhat unsatisfying, as it’s not really foo ’s fault. foo declared statically that it takes a number, and bar broke that contract.

An alternative formulation of gradual types is so-called “sound gradual typing”, where these kinds of blame problems are properly resolved. Typed Racket is an example. Here’s the same program, rendered in Typed and untyped Racket: Module 1 

#lang typed/racket
(provide foo)

(: foo (-> Integer String))
(define (foo x)
  (if (zero? x)
      "test"
      "beef"))

Module 2 

#lang racket
(require "mod1.rkt")

(define (bar x) (foo x))

Running module 2 gives us this error: 

foo: contract violation
  expected: exact-integer?
  given: "test"
  in: the 1st argument of
      (-> exact-integer? any)
  contract from: /private/tmp/mod1.rkt
  blaming: /private/tmp/mod2.rkt

Note that the error here places the blame on the untyped module.

This was all setup for DVH’s talk, which raised an interesting point. As someone who lives mostly in the fully statically typed world, I’m used to thinking about types as being erased. They are a compile-time fiction we use to reason about the program. Types are used to describe a program’s meaning, but they do not affect a program’s meaning.

But in the gradually typed world this just isn’t true! Consider: 

(define (foo x)
  (if (zero? x) (add1 x) 32))

(define (bar) (foo "test"))
(bar)

Here’s one type I could give foo: (-> Int Int) , but this changes the meaning of my program! Running this program used to give 32 , now it errors! The talk went into the ramifications of this fact, and how we might start to think about gradual type inference such that it is always behavior preserving.

Morphosyntactic Programming: Case, Mood, and Type-Directed Disambiguation for Turkish-Like Syntax

Joomy gave a great talk on a personal project of his: implementing a language that incorporates some of the grammatical features of Turkish into a programming language. The language is called Kip and there is an online implementation: https://kip-dili.github.io.

Now, I do not speak or read Turkish, so forgive me if I’ve got the details wrong, but here goes: In Kip, aspects of the program’s type are determined by certain grammatical structures in Turkish. For example, in Haskell, you mark effectful computations by explicitly stating it in the type: 

helloWorld :: IO ()

In Kip, you can do this implicitly by using the infinitive form of nouns. Kip also uses Turkish’s “case” grammatical construct to allow you to supply arguments to a function in any order.

Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean

Apparently, IEEE is creating a new floating point standard! Tung-Che Chang gave this talk on IEEE P3109, a new standard that defines low precision floats, like float16, float8. These formats have become useful within machine learning workloads. The previous standard (IEEE 754) defined two float formats: float32 and float64. This one is different, it defines the float format parametrically, allowing you to pick any precision you want and still have a standard to work from. It also introduces new rounding and saturation modes. This talk walked through the format, which was interesting in and of itself, but also walked through a new project to formalize the format in Lean.

Incr: Faster Re-execution via Bolt-on Incrementalization

Maybe my favorite talk of the day. Vagos Lamprou gave a talk about a tool built on top of a unix primitive they have developed called Ef, which lets you execute a unix command in a new virtualization they call a “semi-isolate”. Semi-isolates isolate all the side effects of a command, but start from the same system state they are run in. Instead of being applied to your host system, these effects (such as file reads/writes) now pile up in a new environment, which can either be applied to your host system or passed to future semi-isolates to run on top of. This talk builds a tool called “incr” that uses semi-isolates to automatically incrementalize a bash script. This lets you run a script once, edit it, run it again, and re-use all work that still applies. It does this by examining the resulting environment of each command to see which commands depend on each other. As an example, imagine this script: 

wget <my-dataset>
awk | sed | grep < dataset.csv > output.csv
python script.py < output.csv

You run this, and realize that script.py has a bug, so you fix it, re-run the script, and incr transparently re-uses the work from lines 1 and 2, saving you from re-doing that computation.

Pointers in OxCaml

Finally, there was a cool talk from Ryan Tjoa on implementing Interior Pointers in OxCaml (Jane Street’s performance oriented fork of Ocaml). Interior pointers are common in systems programming data structures, such as: 

struct foo {
  int len;
  int *ptr;
  // Other data
}

Where ptr might point in the middle of some other arbitrary data structure. This is a challenging pattern to implement in many languages with a garbage collector, as most garbage collectors are free to move heap data around to avoid memory fragmentation. This breaks interior pointers, as you need some way to update them, or else they will point to invalid data. Additionally, the garbage collector needs to be able to understand what objects interior pointers are referring to so that it can track liveness of heap objects and correctly avoid use-after-free issues. This is solved in OxCaml using a two-word field, where the first word tracks the base object, and the second word is an offset into the object. These are also set up using the type system so that they compose nicely, say you have two types like this: 

type b = {
     length : int;
     inner : int array;
}
type a = {
     data : b array;
}

Now if I have a pointer to ints offset by b , and a pointer to a b offset by a , I can combine these to get a pointer to ints offset by a .