Comment by winwang
17 hours ago
Hmm. I had an issue once with numpy shape mismatch errors appearing after 18+ hours of computation. Frustrating, because it could be caught at compile time.
Later, I learned some typelevel programming (in Scala), and by encoding a digital (binary) adder and multiplier at the type level, I showed -- at least to myself -- it was possible to compute and check linear algebra shapes at compile time (without a compiler plugin). It was rather magical and funny to think that I just embedded basic digital logic in such a higher-abstraction world.
It was slow for the inputs I cared about, so I added some optimizations, like an if-statement at the type level, for example, so that it bit-shift for multiplying powers of 2 (multiplication for tensor products). The compile time difference being palpable was a testament to how "some 'ideas' are surprisingly close to others" (err, 'ideas' ~ 'numbers' in this case). There is a connection to the p-adic numbers here, courtesy of dyadics, and some connection to the more-natural "last-mile" problem.
It's not REST, maybe. But I felt it was magical.
I agree that solving logic puzzles is very fun. I even pointed at things such as Advent of Code in my original reply. Computer programming can be very fun and satisfying to do. It is the reason why I became a software developer.
But it is not the same sort activity as writing a short story, or composing a a symphony, or painting a still-life. Those are done with different purposes. Art is something done with the purpose of exploring emotions, aesthetic beauty, question societal norms, etc.
The closest programming gets to that is if you are writing a jingle for advertisement, or drawing a signpost, or writing a technical article.
I disagree. It's not just a logic puzzle. If I haven't communicated that to you, that's also my failure. I've written stories short and long as well. It's a different kind of art.
"Art is something done with the purpose of exploring emotions, aesthetic beauty, question societal norms, etc." I apologize if my emotions and aesthetics are not communicated, but I can only say that they were there. As for societal norms, I doubt that "embedding digital logic in types" is a "norm" of the programming society.
And though it's an appeal to patterns, I will have to bring up the general repeated failure of humanity to recognize art.
I apologize if I don't have the same sort of emotional response to embedding linear algebra validation at the compilation step as I do when I watched Mononoke Hime, or when I read The Picture of Dorian Grey.
While your tale sounded pretty interesting, it is the same sort of interesting as solving a math puzzle. I enjoy math puzzles.
3 replies →