# Typing inference as a map on abstract syntax trees

Is there a reference that explains typing inference for Martin-Löf type theory as a computable map from abstract syntax trees of terms to abstract syntax trees of types? I don't want to identify non-identical judgmentally equal things.

The terms and the types are all defined in the empty context and we also include annotations for the variable types in lambda abstractions.

If there is such a map then is it true if a type is not in beta normal form then it has no terms in beta normal form map to it?

• Just to be sure: you really mean type inference and not type checking? Mar 14, 2021 at 17:18
• The answer to the question about normal forms is obviously negative, $\mathrm{refl}(0)$ is normal inhabitant of the non-normal type $\mathrm{Id}(\mathbb{N}, 0, (\lambda x . x) 0)$. Mar 14, 2021 at 17:20
• @AndrejBauer the question is imprecise but I want a more unique typing where terms have a type not only unique to to judgmental equality but rather unique up to isomorphism of abstract syntax trees. I will try to make it more precise.
– user61651
Mar 14, 2021 at 18:04
• That sounds very restrictive. Why would you want that? Normally one instead has uniqueness of typing: if $\Gamma \vdash t : A$ and $\Gamma \vdash t : B$ then $\Gamma \vdash A \equiv B$. Mar 14, 2021 at 18:12
• Just from a homotopy perspective we can think of terms as points of spaces and equalities as paths so I wondered if we could rigidify typing.
– user61651
Mar 14, 2021 at 18:19

Regarding your second question, this claim is false: the conversion rule of dependent type theory says that a type is inhabited if and only if its normal form is inhabited. So a type such as (\(X:Type). x) Nat is not in beta normal form but is inhabited by the normal forms zero, suc zero, ...