Not explicity, but I was trying out the imperative-ish do syntax, and I believe that uses partial functions when desugared. For example:

private def infiniteLoop: Nat := Id.run do
let mut n: Nat := 0
while true do
n := n + 1
n

I would love a chiller version of AOC where all the problems are first-week level of difficulty.

Nice! I'm really thrown by Lean's imperative syntax in do blocks - for loops, while loops, mutation. I need to read up on what's going on!

"Falling in love" and "thinking it sucks" are both limiting perspectives on TypeScript. It's a remarkable piece of pragmatic programming language tech that bolts some sanity on top of JS and its ecosystem - but all the warts of JS are all still there. The Web should aspire to better.

What does a partial def do?

github.com/mdr/aoc-2024...

I stole and ported this "diagonals" function for today's puzzle. It might be interesting to prove some properties about it, e.g. that the elements of `join (diagonals grid)` are the same (ignoring order) as the elements of `join grid`.

It would work, but the extra wrappers would make me sad:

[ShapeCircle (Circle 3.0), ShapeSquare (Square 4.0)]

How do you find it compared to the proprietary models?

Are you thinking along the lines of:

data Circle = Circle { radius :: Double }
data Square = Square { side :: Double }

data Shape where
CircleShape :: Circle -> Shape
SquareShape :: Square -> Shape

filterCircles :: [Shape] -> [Circle]

PostHog is a top tier name for (amongst other things) a session replay tool!

I hadn't come across Dave Farley before, but he talks a lot of sense!

Me too! I did Unison last year, and Idris the year before. I suspect I might only get through a dozen puzzles or so, but I like the excuse to tinker with something new.