Is 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?
Conversation
Replying to
Are you talking about HOAS? I thought that was orthogonal to NbE?
Replying to
It's a vague and open-ended question inspired by attempting type inference by translating code to an SMT solver. When the solver started failing with type errors I was like "Why not reuse the solver's type system?" and then "Why not reuse the host language's type system?"
1
4
I guess you'll be constrained to things the host type system can express, while working around the things you don't want it to do. But maybe those statements are too simple to be worth much.
2