GitHubAbout me
I am a 4th year PhD student at Stanford University researching programming languages and compilers. My advisor is Alex Aiken. I have a bachelor's in CS and math from UC Berkeley.
My favorite programming language is Rust. My favorite dependently typed programming language (proof assistant) is Agda.
Research
High performance functional programming
Human RAM is limited. Hence, programmers must be able to reason compositionally about the correctness and performance of their code. To that end, we build abstractions. Interpreted liberally, the relevant quote is by Grothendieck:
The unknown thing to be known appeared to me as some stretch of earth or hard marl, resisting penetration… the sea advances insensibly in silence, nothing seems to happen, nothing moves, the water is so far off you hardly hear it.. yet it finally surrounds the resistant substance.
My primary research project the past few years has been the Morphic programming language. Morphic turns pure, functional programming constructs into zero-cost abstractions.
- Morphic's lambda set specialization makes lambdas unboxed and statically dispatched, and allows calls to lambdas to be inlined. See the paper or talk for details.
- Morphic uses a borrow-based reference counting scheme which is able to eliminate almost all reference count increments and decrements for a large class of programs. A paper on the topic was accepted subject to minor revision, as usual, and should be published in a few months.
- Morphic's mutation optimization transforms updates to logically-immutable data structures into in-place mutations when doing so does not affect semantics.
A central tenet of Morphic is that optimizations should be resilient and scalable. Traditional interprocedural analyses do not scale because they become arbitrarily imprecise as the size of a code base increases. A caller affects its callees and that, in turn, affects other callers. This is called poisoning. All of Morphic's optimizations are specializing (think C++ or Rust generics) and, therefore, non-poisoning. For example, a function's reference counting scheme might depend on its caller because it might or might not be responsible for decrementing the reference counts of its arguments. But, in Morphic, adding a new caller will never degrade performance. Instead, the compiler is free to generate multiple copies of the function featuring different schemes.
Dependent type theory
I am also doing some type theory work, though I don't yet have as much to say about that. In short, equality in type theory is tricky. One can adopt a path equality satisfying univalence, i.e., such that equivalent types are equal. Essentially, with an extensionality principle on the universe of types—a useful tool for defining objects best understood "up to isomorphism." Alternatively, one can adopt a strict equality such that any two witnesses to the same equality are equal. Strict equalities are easier to work with than path equalities. They are also necessary to correctly define important notions, such as infinitely-coherent monoids. Of course, it is desirable to support both notions of equality—the right tool for the right task. To prevent elimination of the path equality into the strict equality, which would be unsound, one must then introduce a strict universe Ω of propositions, separate from the universe of types U.
I am interested in formulating a type theory with a "nice" Ω supporting ways to escape back into U. E.g., unlike Coq/Rocq, we should have unique choice:
{A B R} ((a : A) → ∃! b , R a b) → ∃! f , R a (f a)