What's the usual approach to bidirectional type checking for applications of lambdas without annotations? Synthesize func type A -> B containing a metavar, check arg type against A, have checking unify and return substitutions that you apply to B?
Conversation
The "traditional" bidirectional approach is to give up, and expect annotations at bare beta-redexes.
You can do a little better by adopting the "Let Arguments Go First" approach [1], but I'm pretty sure anything more would require HM.
[1]
4
8
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Does this mean bidirectional elaboration is good but from there everything is explicitly typed?
1
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
This Tweet is from a suspended account. Learn more
The only issue with explicitly typed core is if you are too eager about annotation then you can end up with lots of needless duplication and so you need to do some sorts of CSE/let-floating type optimizations in the elaboration. But otherwise it doesn't make much sense to me.
2
1
Yeah, for example I was running into this here: twitter.com/brendanzab/sta - link to where McBride talks about this is in a tweet in that thread. Andras Korvacs and have a neat approach where you 'remember' the original neutrals, letting you readback into unbloated terms.
Quote Tweet
So, in some detective work going back into my prior state of mind, it seems like this thread is where I got scared off from using readback in my elaborator, which actually seems quite similar to what McBride is talking about in the above quote: twitter.com/brendanzab/sta
Show this thread