What’s the context of this quote?
Conversation
Bob .. Harper .. giving a lecture .. on Homotopy Type Theory?
1
Sorry, I was vague. I meant in John Leo’s talk; in what context was he invoking the Harper quote?
1
Oh, just talking up dependent type theory. Y'know, future so bright kinda stuff.
(I don't quite agree or disagree enough to state an opinion either way, but Harper both cracks me up and makes me swoon a little when speaking that way..)
1
2
Researching so far outside of current practicalities does require an optimism that borders on megalomania — so yes, thus both the cracking up and the swooning.
(I should really properly understand dependent type theory one of these days.)
1
At some level it's like "ok so you can encode vec of length N" and at another level it's like "ok you can encode literally any theorem in all of mathematics as a type" and tbqh it's a bit of an abrupt leap between the two.
(The chapter in Coq'Art is aptly titled "Pandora's Box")
1
Yeah, that tweet just about summarizes my understanding. In the vaguest sense, I get that it’s what happens if you follow the Curry-Howard correspondence to its natural conclusions, but that’s about it.
1
I think it's more like .. the way you fall off the turing-completeness cliff if you foolishly happen to add backwards branches to coded instructions. If you foolishly happen to name the bound _value_ in a type abstraction, the whole universe gets sucked into the resulting vortex.
2
2
Like you really don't have to go very far to find the natural conclusion. I think pretty much just here: math.andrej.com/2012/11/08/how
2
5
I struggled with it for a _long_ time because I couldn't wrap my head around how runtime values travelled backwards in time across the phase distinction, but they don't; all reasoning is still at compile time, it's just over _normalized symbolic expressions_ from all universes.
1
1
5
Yup, I found the best way to understand it was to implement it. Makes things much clearer.