patternMinor
Some points about type checking of simply typed $\lambda$-calculus?
Viewed 0 times
calculuspointscheckingtypetypedsomeaboutsimplylambda
Problem
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)
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)
Solution
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.)
$$
((\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.)
Context
StackExchange Computer Science Q#87801, answer score: 6
Revisions (0)
No revisions yet.