Swimming out past intuition
26 Jul 2020 ⇐ Notes archive(This is an entry in my technical notebook. There will likely be typos, mistakes, or wider logical leaps — the intent here is to “let others look over my shoulder while I figure things out.”)
After a recent note on Binding[dynamicMember:], I’ve jokingly started a Twitter thread with the type’s affordances — à la Rob Rix’s “it type checks, but what does it mean?”
So far I’ve got Binding.zip and .flatMap (or alternatively, join paired with the dynamic member subscript).
Type checking drove the implementations since I don’t grok them yet. What does it mean to flatMap on Bindings? Is that something we’d even want to do?
The compiler signaled the “reachability” of these functions, even if my understanding wasn’t there. And this is why proof assistants like Lean and community efforts behind them (the Xena project) excite me. If mathematics can be formalized to a point where assistants can guide our work in the same way a compiler does for engineering, we can swim past our present intuitions.
It’ll take a while for our collective knowledge to catch up to a lengthened line of sight, but we also needed telescopes before we could physically explore space.