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
I remember working through /A tutorial implementation of a dependently typed programming language/ and being like whoa this is tiny and simple! and then tried to write a program in it and ran headlong into the lack of implicits and was like ohhhhhhhhhhh
1
2
Brendan Zabarauskas
@brendanzab
Yeah definitely. You end up like Dhall 😂 I'm hopeful the Andras' implicit function elaboration helps me to understand this stuff more - it's just too much of a challenge to try to look at all the papers then 'draw the rest of the elaborator'
Quote Tweet
Brendan Zabarauskas
@brendanzab
·
I'm hoping to read “Elaboration with First-Class Implicit Function Types” by Andras Korvacs at some stage - seems like it might be a good starting point at least? And it has an implementation, which is super helpful: • dl.acm.org/doi/10.1145/34 • github.com/AndrasKovacs/i
Show this thread
2
5