I’ve long been obsessed with minimalistic languages that still manage to have expressive power. My usual approach: start with a bare-bones combinato

rohlang3: (an attempt at) a point-free, homoiconic, and dependently typed SK calculus

submited by

Style Pass

2025-01-03 01:30:04

I’ve long been obsessed with minimalistic languages that still manage to have expressive power. My usual approach: start with a bare-bones combinator calculus (like SK), then keep adding “one more extension” until it looks suspiciously like a full-blown typed language. rohlang3 is exactly that experiment. It’s a small language built in Rust that tries to be point-free, homoiconic, and (somewhat) dependently typed, all on top of an SK-like foundation—plus reflection, partial evaluation, and a weird environment reordering system.

I also have no formal education in these fields so I could have some fundamentally misunderstanding about any of these topics.

But that alone wasn’t enough for me. I piled on new combinators for reflection (q and e), partial evaluation (z), environment reordering (i, E, D), and a Pi/Sigma-style dependent type system (p, g). It definitely breaks “pure minimalism,” but it’s also what makes rohlang3 interesting to hack on.

I wanted some notion of dependent types so I could treat the language as if it were a mini proof system (even though that’s kind of precarious). We have a single universe u. You can do (p u u) for a Pi type or (g u u) for a Sigma type—both reflect a simplified (read: incomplete) approach to higher-level type theory. It’s enough to write small examples like (pu(ku))(p u (k u)) or (gu(i))(g u (i)).