Conversation

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

· Oct 15, 2020

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:59 AM · Oct 16, 2020Twitter Web App

Replying to

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

GitHub - AndrasKovacs/implicit-fun-elaboration: Implementation for ICFP 2020 paper

Implementation for ICFP 2020 paper. Contribute to AndrasKovacs/implicit-fun-elaboration development by creating an account on GitHub.

Replying to

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!

Brendan Zabarauskas

@brendanzab

Oct 16, 2020

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?' 😰

Show replies