Conversation

Brendan Zabarauskas
@brendanzab
In the past I've struggled to navigate the research around inferring 'missing stuff' when elaborating dependently typed languages. This thread by
@rob_rix
would have been helpful back then for understand what they were all talking about wrt. "higher order unification", etc!
Quote Tweet
Rob Rix‎
@rob_rix
·
pattern unification works by carefully constructing a diff between two types with holes for the information missing on either side, and then rifling madly through the context to see what you’ve got lying around that it can cram into the holes, possibly by turning or hitting them.
Show this thread
2
12
Rob Rix‎
@rob_rix
tbh it would’ve been helpful for me too. It’s not even clear at the outset *what it’s for* from most of the literature!
1
3
Brendan Zabarauskas
@brendanzab
yeah I just ended up at 'higher order unification' and logic programming stuff and got very confused 😳 and then in trying to tell people about it folks are like 'isn't higher order unification undecidable?' 😰
2
2
Rob Rix‎
@rob_rix
Replying to
@brendanzab
Right? I mean, I definitely respect the sheer audacity of looking at like “oh, this is an algorithm that, if it works, can test and generate equal programs” and not just shutting off the computer and going for a walk but actually making it happen.
1
Rob Rix‎
@rob_rix
But so much is communicated by the boundaries of hard problems and their solutions that too often goes unspoken. What is it useful for, what is it not? What are the frictions? Where/when does undecidability occur? Why? Etc.
1
Show replies