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
Brendan Zabarauskas
@brendanzab
Replying to
@brendanzab
and
@rob_rix
I'm hopeful that the more of us show an interest outside of academia, the easier it will become for the next folks who want to give it a go. Thankfully I'm seeing more people than ever interested in implementing dependent type systems, which is a positive sign.
1
András Kovács
@andrasKovacs6
I'm doing a weekly seminar on elaboration. We're going though elaboration-zoo and I'm revising it quite significantly each week. The seminar's on MS Teams, I can send invites if you want. It's 10-12 am UTC Friday, if that's not good you can still get the recordings.
6
14
Show replies