Does dependent type checkers need to store lambda parameter type in their core language?

Question

"Core language" refers to the exported well-typed terms that can be evaluated (or reduced).

In the core language of MiniAgda, a dependently-typed language, the parameter type of a lambda is not stored anywhere. So does in Mini-TT and Agda.

However, Idris does store lambda parameter type in its core language.

I wonder do we need/needn't to store parameter type (or, under what condition do we need/needn't to store it)? Because according the surface syntax of all these languages, they don't have lambdas with their parameters explicitly-annotated. For Idris here's a link showing that Idris does not have lambda with type annotation.

Answer 1

In general, type inference for dependent types is undecidable. This means that when checking a function, we need some way to know what type its argument has.

In the case of Idris, they simply annotate lambdas with parameter types. This is very common in type theory, since it makes your type system syntax directed in a very simple way. When you do this, you can usually view the typing judgment as having the type as an output parameter (i.e. given the input term, you can determine its type).

I don't know what MiniAgda does in particular, but the other main way is to treat the type as an input to the checking judgment. So in this case, you don't need to store the type of the function in the AST, but when typechecking, you will use the context in some way to get the type of the function (i.e. from an annotation).

Generally this is done using bidirectional typechecking. This paper and this post both give excellent overviews of how this can be done in practice.

Answer 2

In Bob Harper's logical framework papers, there is the notion of canonical forms and quasi-canonical forms. The lambda abstractions in the type theory do store binder types (which they call "type labels"), and therefore canonical forms do, but they specifically introduced quasi-canonical forms as canonical forms without binders, and these are sufficient for approximating the version that does have them.

Quoting from On Equivalence and Canonical Forms in the LF Type Theory https://www.cs.cmu.edu/~rwh/papers/lf-theory/lf-theory.pdf:

We show that quasi-canonical forms of a given type are sufficient to determine the meaning of an object, since the type labels can be reconstructed (up to definitional equality) from the classifying type.