Gabriella Gonzalez@GabriellaG439·Mar 7Is there a type-checking analog of normalization-by-evaluation where one reuses the host language's type checker to produce inferred types and error messages?7221
Brendan Zabarauskas@brendanzab·Mar 7Are you talking about HOAS? I thought that was orthogonal to NbE?21
Brendan Zabarauskas@brendanzabReplying to @brendanzab and @GabriellaG439(Interesting question though!)3:38 AM · Mar 7, 2022·Twitter Web App