2
$\begingroup$

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?

Improve this question
$\endgroup$
7
  • $\begingroup$ Just to be sure: you really mean type inference and not type checking? $\endgroup$
    – Andrej Bauer
    Commented Mar 14, 2021 at 17:18
  • $\begingroup$ 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)$. $\endgroup$
    – Andrej Bauer
    Commented Mar 14, 2021 at 17:20
  • $\begingroup$ @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. $\endgroup$
    – user61651
    Commented Mar 14, 2021 at 18:04
  • $\begingroup$ 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$. $\endgroup$
    – Andrej Bauer
    Commented Mar 14, 2021 at 18:12
  • $\begingroup$ 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. $\endgroup$
    – user61651
    Commented Mar 14, 2021 at 18:19

1 Answer 1

Reset to default
3
$\begingroup$

Type inference for dependent type theory is undecidable in general, so what you're asking for is impossible. However, it is possible to separate the syntax into inferrable terms and checkable terms, and implement inference for the inferrable fragment. This is the approach taken by bidirectional typechecking. The paper on LambdaPi by Andres Löh, Conor McBride and Wouter Swierstra describes a tutorial implementation of a dependent typechecker in this style. More advanced typecheckers for dependently typed languages typically rely on higher-order unification to infer the types for more expressions, a good example is the paper on Higher-order Dynamic Pattern Unification by Andreas Abel and Brigitte Pientka.

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, ...

Improve this answer
$\endgroup$
3
  • $\begingroup$ I thought type inference is decidable in the empty context for intensional Martin-Löf type theory. Is that not true? $\endgroup$
    – user61651
    Commented Mar 14, 2021 at 16:33
  • $\begingroup$ Nobody aasked for computable type inference... $\endgroup$
    – Andrej Bauer
    Commented Mar 14, 2021 at 17:17
  • $\begingroup$ > I thought type inference is decidable in the empty context for intensional Martin-Löf type theory. Is that not true? I don't know of any result like that. $\endgroup$
    – Jesper
    Commented Mar 15, 2021 at 8:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.