5
$\begingroup$

type checking

I was preparing examples of type checking in simply typed $\lambda$-calculus. I wanted to explain it to my audience in the way of implementation. And I found a bit tricky point in the typing rule of application, which is as follows.

$$ \frac {\Gamma \vdash t_1:T_{11}\rightarrow T_{12} \quad \Gamma \vdash t_2:T_{11}} {\Gamma \vdash t_1 \, t_2 :T_{12} } $$

$$ \frac {\Gamma, x:T_1 \vdash t_2 :T_2} {\Gamma \vdash \lambda x:T_1.t_2 : T_1 \rightarrow T_2} $$

Typing rules for booleans are:

$$ \frac {} {\Gamma \vdash \texttt{true}: bool } $$

$$ \frac {} {\Gamma \vdash \texttt{false}: bool } $$

My question

As far as I know, we do not need unification for type checking in the typed $\lambda$-calculus, we need unification in type inference. However, the following type checking example seems that we need something like unification, also it seems that type checking is leading to type construction.

$$ \frac { \vdash \lambda x:bool.x: T \rightarrow bool \quad \vdash \text{true}: T} { \vdash (\lambda x:bool.x) \text{ true}: bool } $$ Here, $T$ is unknown type variable. It is easy to saying that $T$ is $bool$ because of the boolean typing rules, so we can continue the left branch of the above type checking as follows.

$$ \frac {x:bool \vdash x:bool} { \vdash \lambda x:bool.x: bool \rightarrow bool } $$

The premise is true, so the type checking is successful.

But how do we know the value of $T$ in an implementation? It should take matching $ true:bool$ to $true: \text{T}$ to know $T$ is $bool$. But this seems unification to me.

Also, finding $T$ for $\Gamma \vdash t: T$ is a type inference problem. So, the above type checking is leading to type inference. Am I correct?

Does type checking of the simply typed $\lambda$-calculus need unification?

Does type inference appear when doing type checking?

Please correct me if I am wrong at any point and explain.

Other info

Type checking of ${ \vdash (\lambda x:bool.x) \text{ true}: bool }$ is given as an example in the book "types and programming languages", page 103. However, it did not specify how $T$ is obtained. Its derivation concluded $T$ is $bool$ when using the typing rule of application, as shown below.

$$ \frac { \vdash \lambda x:bool.x: bool \rightarrow bool \quad \vdash \text{true}: bool} { \vdash (\lambda x:bool.x) \text{ true}: bool } $$

I believe these details are ignored in the book.

Improve this question
$\endgroup$
6
  • $\begingroup$ Why do you think we don't need unification (or something morally equivalent) for type checking? Even if it isn't necessary, why avoid it seeing that many implementations do use it? $\endgroup$
    – Derek Elkins left SE
    Feb 7, 2018 at 10:24
  • $\begingroup$ I assume it is a typo, but type inference would be more like finding a (usually "most general" in some sense) $T$ given $t$ and $\Gamma$ such that $\Gamma\vdash t:T$. Bidirectional type checking does split type checking into synthesis and checking phases, but while the synthesis phase is similar to type inference, there is no requirement that every type be synthesizable. That is, we can restrict synthesis to only the "easy" cases. $\endgroup$
    – Derek Elkins left SE
    Feb 7, 2018 at 10:32
  • $\begingroup$ @DerekElkins "That is, we can restrict synthesis to only the "easy" cases.", what you mean is that we can restrict the case such that $T$ can be obtained by not unification but a simply matching? It would be great if you could explain in an answer using above example. "I assume it is a typo,", which one you are referring to? $\endgroup$
    – alim
    Feb 7, 2018 at 10:47
  • $\begingroup$ I'm referring to where you state "finding $t$ for $\Gamma\vdash t:T$ is a type inference problem". I'm intentionally being vague by what "easy" means but I am definitely not intending the avoidance of unification. Unification isn't "hard", at least not first-order unification. Bidirectional type checking is often applied where the type inference problem is undecidable, while synthesis in these systems is restricted to be decidable. $\endgroup$
    – Derek Elkins left SE
    Feb 7, 2018 at 11:05
  • $\begingroup$ At any rate, if you want to describe type checking in terms of an implementation, then you need to have an actual implementation in mind. If you want an implementation that doesn't use unification, you should explicitly ask for one, and not just whether it's possible for one to exist. $\endgroup$
    – Derek Elkins left SE
    Feb 7, 2018 at 11:05

1 Answer 1

Reset to default
6
$\begingroup$

Your example is poorly chosen. In $(\lambda x : \mathsf{bool} . x) \, \mathsf{true}$ you can obviously read off the type from the $\lambda$-abstraction because it tells you that $x$ should have type $\mathsf{bool}$. A more relevant example is $$ ((\lambda f : \mathsf{bool} \to \mathsf{bool} . f) (\lambda x : \mathsf{bool} . x)) \, \mathsf{true} : \mathsf{bool} $$ Now we are faced with determining $T$ by looking at $(\lambda f : \mathsf{bool} \to \mathsf{bool} . f) (\lambda x : \mathsf{bool} . x)$.

The usual algorithm to be used for this sort of thing is bidirectional typechecking: some terms have their types checked but others have their types inferred. No unification is required, because all types are inferred immediately. (Unification happens when we postpone decisions until a later time.)

Improve this answer
$\endgroup$
2

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.