Idiomdrottning’s homepage

Azorius vs Simic at the compiler

All the kids today with their dependent types and their provable correctness… I’m more of a hack hack, explore, evolve, iterative incremental improvement, big ball of mud, foot gun, intuitive programmer. Leaning into emotions and heuristics and hammock time and smells and refactoring. Hacking on the right side of the brain?

In the Pie language from The Little Typer:

(claim Odd
       (-> Nat U))
(define Odd
  (lambda (n)
    (Sigma ((half Nat))
           (= Nat n (double half)))))

We can formally prove that 42 is odd.

I don’t wanna parade-rain on this stuff. It’s cool that people are trying new things. I’m… just hanging back to see where things are going.

Update

left_adjoint wrote a really good follow-up post:

A lot of dependently typed programming languages that have text editor integration will fill in the skeleton of what the program must be by the induction principle of the type, giving you a bunch of “holes” to fill in for your code. You can fill in those holes piecemeal and even be working on defining your theorems and properties about your code simultaneously.

About a year ago I saw a demo of someone using Elm (the web framework, not the mail app) in a similar way. For me, that still seem like it’d be a major leap in how I work with code. It’s great that it does the boiler plate for me, and I really, really appreciate that it does, but… when it’s not done yet?

How easy is it to refactor stuff, mold stuff around? Lisp to me is more like a, uh, a moldable clay, while Elm came across as programming with a super enhanced bionic exoskeleton on. Each keystroke inferring mountains. As you can see, my ignorance is showing here. I don’t have that much experience with a good typed language (outside of Haskell, which inspired brev, though I based my polymorphic multimethods on arbitrary (and arbitrarily composable) preds rather than on a type hierarchy) and am still reeling from Java and C++ back in the day. That’s why I’m being careful to try to not parade-rain.

It’s a process that I find very symbiotic, really, and less antagonistic than the typical “write code => does it work => aww fuck” loop.

This symbiotic, exploratory processes sounds very appealing. I love REPL-driven programming, making something, refactoring it, extracting, inlining, renaming stuff until it’s awesome.

One thing that does not sound great is the name, “Agda”, in a Swedish-speaking context. I know, I know, I’m getting tedious with my constant wish for a new name for GIMP and Apache but… “Agda” (because of the song it intentionally references) is my least favorite of all those.

Type City

I feel like there are three reasons for types.

Performance

Which, yes. Very appealing. Run-time chex are slooow.

Super-auto-completing super-powered coding

Which… isn’t the compiler auto-doing things that you ideally wouldn’t even have to do? Like, take the classic & well-known awk program '!x[$0]++' which removes duplicate (including non-consecutive) lines. It doesn’t need to generate code for all record types, it just… works on all types right away. And the entire program is just seven chars♥

Similarly I made as-list so that list operators could work on many other types, not just lists.

Provably error-free

This is the part that I think is sus. As the “42 is odd” example above implies. To sell me on dependent type stuff, lean into the performance and the super-powered coding, just like left_adjoint did♥