Brendan Zabarauskas on Twitter: "@jonmsterling @anormalform @alpha_convert @typer_uma Are you ok with having coercive subtyping? Saw that in some of Luo's papers, and it seemed handy!" / Twitter

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?

2

8

Joe Cutler

@alpha_convert

Apr 4, 2021

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]