in Code


Justin Le

Welcome! My name is Justin Le. I’m an Applied Math/Computational Science PhD with a background with physics, previously at Chapman University, SimSpace, Google, and currently at Anduril. This is just my weblog covering my various adventures in programming and explorations in the vast worlds of computation, physics, engineering, mathematics, and knowledge. Expect a healthy curiosity and an only slightly unhealthy obsession for finding new ways to marvel, wonder, and create. Join me if you wish!

Check out some of my most popular articles: First-Class Statements, “IO Monad” Considered Harmful, and Purely Functional Typed Models!

Recent Entries

  • Advent of Code 2025: Haskell Solution Reflections for all 12 Days

    Merry Christmas all! This is my annual Advent of Code post! Advent of Code is a series of (this year) 12 daily Christmas-themed programming puzzles that are meant to be fun diversions from your daily life, help you find a bit of whimsy in your world, give you a chance to explore new ideas and program together with your friends. I always enjoy discussing creative ways to solve these puzzles every day, and it’s become a bit of an annual highlight for me and a lot of others. My favorite part about these puzzles is that they are open ended enough that there are usually many different interesting ways to solve them — it’s not like a stressful interview question where you have to recite the obscure incantation to pass the test. In the past I’ve leveraged group theory, galilean transformations and linear algebra, and more group theory.

    Haskell is especially fun for these because if you set up your abstractions in just the right way, the puzzles seem to solve themselves. It’s a good opportunity every year to get exposed to different parts of the Haskell ecosystem! Last year, I moved almost all of my Haskell code to an Advent of Code Megarepo, and I also write up my favorite ways to solve each one in the megarepo wiki.

    All of this year’s 12 puzzles are here, but I’ve also included links to each individual one in this post. I’m also considering expanding some of these into full on blog posts, so be on the look out, or let me know if there are any that you might want fully expanded! And if you haven’t, why not try these out yourself? Be sure to drop by the libera-chat ##advent-of-code channel to discuss any fun ways you solve them, or any questions! Thanks again to Eric for a great new fresh take on the event this year!

    Read more … Comments

  • The Baby Paradox in Haskell

    Everybody Loves My Baby is a Jazz Standard from 1924 with the famous lyric:

    Everybody loves my baby, but my baby don’t love nobody but me.

    Which is often formalized as:

    \[ \begin{align} \text{Axiom}_1 . & \forall x. \text{Loves}(x, \text{Baby}) \\ \text{Axiom}_2 . \forall x. & \text{Loves}(\text{Baby}, x) \implies x = me \end{align} \]

    Let’s prove in Haskell (in one line) that these two statements, taken together, imply that I am my own baby.

    Read more … Comments

  • Faking ADTs and GADTs in Languages That Shouldn't Have Them

    Haskell is the world’s best programming language1, but let’s face the harsh reality that a lot of times in life you’ll have to write in other programming languages. But alas you have been fully Haskell-brained and lost all ability to program unless it is type-directed, you don’t even know how to start writing a program without imagining its shape as a type first.

    Well, fear not. The foundational theory behind Algebraic Data Types and Generalized Algebraic Data Types (ADTs and GADTs) are so fundamental that they’ll fit (somewhat) seamlessly into whatever language you’re forced to write. After all, if they can fit profunctor optics in Microsoft’s Java code, the sky’s the limit!

    This is an “April Fools” joke in the tradition of my previous one in some of these ways that we are going to twist these other languages might seem unconventional or possibly ill-advised… but also the title is definitely a lie: these languages definitely should have them! :D


    1. I bet you thought there was going be some sort of caveat in this footnote, didn’t you?↩︎

    Read more … Comments

  • Sum Types and Subtypes and Unions

    There’s yet again been a bit of functional programming-adjacent twitter drama recently, but it’s actually sort of touched into some subtleties about sum types that I am asked about (and think about) a lot nowadays. So, I’d like to take this opportunity to talk a bit about the “why” and nature of sum types and how to use them effectively, and how they contrast with other related concepts in programming and software development and when even cases where sum types aren’t the best option.

    Read more … Comments

  • Advent of Code 2024: Haskell Solution Reflections for all 25 Days

    Admittedly a bit late, buuuuuut Merry belated Christmas and Happy New Years to all!

    This past December I again participated in Eric Wastl’s Advent of Code, a series of 25 daily Christmas-themed puzzles. Each puzzle comes with a cute story about saving Christmas, and the puzzles increase in difficulty as the stakes get higher and higher. Every night at midnight EST, my friends and I (including the good people of libera chat’s ##advent-of-code channel) discuss the latest puzzle and creative ways to solve and optimize it. But, the main goal isn’t to solve it quickly, it’s always to see creative ways to approach the puzzle and share different insights. The puzzles are bite-sized enough that there are often multiple ways to approach it, and in the past I’ve leveraged group theory, galilean transformations and linear algebra, and more group theory. This year was also the special 10 year anniversary event, with callbacks to fun story elements of all the previous years!

    Most of the puzzles are also pretty nice to solve in Haskell! Lots of DFS’s that melt away as simple recursion or recursion schemes, and even the BFS’s that expose you to different data structures and encodings.

    This year I’ve moved almost all of my Haskell code to an Advent of Code Megarepo. I also like to post write-ups on Haskelly ways to approach the problems, and they are auto-compiled on the megarepo wiki.

    I try my best every year, but sometimes I am able to complete write-ups for all 25 puzzles before the new year catches up. The last time was 2020, and I’m proud to announce that 2024 is now also 100% complete!

    You can find all of them here, but here are links to each individual one. Hopefully you can find them helpful. And if you haven’t yet, why not try Advent of Code yourself? :) And drop by the libera chat ##advent-of-code channel, we’d love to say hi and chat, or help out! Thanks all for reading, and also thanks to Eric for a great event this year, as always!

    Read more … Comments

  • Functors to Monads: A Story of Shapes

    For many years now I’ve been using a mental model and intuition that has guided me well for understanding and teaching and using functors, applicatives, monads, and other related Haskell abstractions, as well as for approaching learning new ones. Sometimes when teaching Haskell I talk about this concept and assume everyone already has heard it, but I realize that it’s something universal yet easy to miss depending on how you’re learning it. So, here it is: how I understand the Functor and other related abstractions and free constructions in Haskell.

    The crux is this: instead of thinking about what fmap changes, ask: what does fmap keep constant?

    This isn’t a rigorous understanding and isn’t going to explain every aspect about every Functor, and will probably only be useful if you already know a little bit about Functors in Haskell. But it’s a nice intuition trick that has yet to majorly mislead me.

    Read more … Comments

  • Seven Levels of Type Safety in Haskell: Lists

    One thing I always appreciate about Haskell is that you can often choose the level of type-safety you want to work at. Haskell offers tools to be able to work at both extremes, whereas most languages only offer some limited part of the spectrum. Picking the right level often comes down to being consciously aware of the benefits/drawbacks/unique advantages to each.

    So, here is a rundown of seven “levels” of type safety that you can operate at when working with the ubiquitous linked list data type, and how to use them! I genuinely believe all of these are useful (or useless) in their own different circumstances, even though the “extremes” at both ends are definitely pushing the limits of the language.

    This post is written for an intermediate Haskeller, who is already familiar with ADTs and defining their own custom list type like data List a = Nil | Cons a (List a). But, be advised that most of the techniques discussed in this post (especially at both extremes) are considered esoteric at best and harmful at worst for most actual real-world applications. The point of this post is more to inspire the imagination and demonstrate principles that could be useful to apply in actual code, and not to present actual useful data structures.

    All of the code here is available online here, and if you check out the repo and run nix develop you should be able to load them all in ghci as well:

    $ cd code-samples/type-levels
    $ nix develop
    $ ghci
    ghci> :load Level1.hs

    Read more … Comments