Shouldn't the elaborated lambda abstractions be annotated with their parameter type?

[atennapel]

In 03-holes the lambda abstractions in the well-typed core terms Tm have no parameter type. How can it be well-typed in that case, since we cannot typecheck a lambda abstractions without a domain type.

[AndrasKovacs]

Thanks for the question!

There are a bunch of trade-offs in annotating terms with types. The amount of annotations depend on what we want to do with elaboration output.

The main question is: do we want to re-check elaboration output? The motivation for re-checking is usually validation; for example in Coq we re-check core terms generated by tactics to make sure that they make sense, because tactics are not guaranteed to output well-formed terms. Another example is GHC Haskell, where we have a core linter, which checks elaboration output with a simpler algorithm than elaboration itself. Then, passing the core linter gives some evidence for the correctness of optimization passes, for instance.

In elaboration-zoo, the only thing we do with elaboration output is evaluation, for the purpose of conversion checking and normalization, and lambda annotations are superfluous for this purpose. We also just trust that the elaborator produces well-typed output. Hence, we don't ever re-check core terms.

You're right that in a production-strength system, we'd probably annotate lambdas. In 03-holes, it's not hard and probably a good exercise to add lambda annotations.

[atennapel]

Thanks for the detailed answer! Yes for my purposes I need to re-check and I was just wondering why you left it out. So I will attempt to do the exercise :)