Relation between Meta/C++ typecheckers

Stream: lean4

[Wojciech Nawrocki]

What is the relation between the Lean.Meta typechecking functionality, and the corresponding code in the kernel? For example, there is isExprDefEq and is_def_eq which seem to be totally separate. Can we expect them to do exactly the same thing?

[Arthur Paulino]

cc @Gabriel Barreto

[Leonardo de Moura]

Wojciech Nawrocki said:

What is the relation between the Lean.Meta typechecking functionality, and the corresponding code in the kernel? For example, there is isExprDefEq and is_def_eq which seem to be totally separate. Can we expect them to do exactly the same thing?

There is one big difference: the kernel has no support for metavariables. It expects that all of them have been eliminated by the frontend.

[Leonardo de Moura]

The Lean.Meta version also supports features that are not relevant in the kernel. Example: smart unfolding.

[Leonardo de Moura]

The heuristics are also slightly different, and the kernel does not take attributes such as [reducible] into account.

[Arthur Paulino]

Which are the contexts of use for each of them?

[Leonardo de Moura]

The kernel is used to type-check fully elaborated declarations. We say it is part of the "trusted code base". Suppose one implements a buggy tactic that produces an invalid proof. The kernel will catch the mistake during type checking.
Lean.Meta is used in to implement the frontend: tactics, type inference, type class resolution, etc. The whole elaborator is based on Lean.Meta.

[Wojciech Nawrocki]

Thank you! Then the one worry I would have about discrepancies is if there were terms (that can go into the kernel, so metavariable-less, etc) which the Meta version accepts but the kernel rejects, or alternatively ones which Meta complains about but the kernel would be happy with.

[Siddharth Bhat]

@Leonardo de Moura if I may, I have a follow up question: what is the type checking algorithm used by the kernel? is it normalization-by-evaluation flavoured? If it is not NbE, what is the algorithm?

[Leonardo de Moura]

Wojciech Nawrocki said:

Thank you! Then the one worry I would have about discrepancies is if there were terms (that can go into the kernel, so metavariable-less, etc) which the Meta version accepts but the kernel rejects, or alternatively ones which Meta complains about but the kernel would be happy with.

This is a valid concern. If the kernel does not accept something created by Meta, we treat it as a bug. The other direction is harder to observe, at least, as a regular user.

[Leonardo de Moura]

Siddharth Bhat said:

Leonardo de Moura if I may, I have a follow up question: what is the type checking algorithm used by the kernel? is it normalization-by-evaluation flavoured? If it is not NbE, what is the algorithm?

The kernel type checker is very simple. There isn't any fancy algorithm there. It unfolds things lazily and uses a cache. That being said, we want to implement an efficient term normalizer in the future. The goal is to provide better support for proofs by reflection.

[Mac]

Wojciech Nawrocki said:

terms (that can go into the kernel, so metavariable-less, etc) which the Meta version accepts but the kernel rejects

If you ever see an error message that begins with (kernel), this is what has happened. And, as Leo mentioned, it should ideally be reported as a bug.