# Typechecking

(* $Date: 2013-01-16 22:29:57 -0500 (Wed, 16 Jan 2013) $ *)

Require Export Stlc.

The has_type relation of the STLC defines what it means for a
term to belong to a type (in some context). But it doesn't, by
itself, tell us how to
Fortunately, the rules defining has_type are

*check*whether or not a term is well typed.*syntax directed*— they exactly follow the shape of the term. This makes it straightforward to translate the typing rules into clauses of a typechecking*function*that takes a term and a context and either returns the term's type or else signals that the term is not typable.Module STLCChecker.

Import STLC.

Fixpoint beq_ty (T

_{1}T

_{2}:ty) : bool :=

match T

_{1},T

_{2}with

| TBool, TBool =>

true

| TArrow T

_{11}T

_{12}, TArrow T21 T22 =>

andb (beq_ty T

_{11}T21) (beq_ty T

_{12}T22)

| _,_ =>

false

end.

... and we need to establish the usual two-way connection between
the boolean result returned by beq_ty and the logical
proposition that its inputs are equal.

Lemma beq_ty_refl : ∀T

_{1},

beq_ty T

_{1}T

_{1}= true.

Proof.

intros T

_{1}. induction T

_{1}; simpl.

reflexivity.

rewrite IHT1_1. rewrite IHT1_2. reflexivity. Qed.

Lemma beq_ty__eq : ∀T

_{1}T

_{2},

beq_ty T

_{1}T

_{2}= true → T

_{1}= T

_{2}.

Proof with auto.

intros T

_{1}. induction T

_{1}; intros T

_{2}Hbeq; destruct T

_{2}; inversion Hbeq.

Case "T

_{1}=TBool".

reflexivity.

Case "T

_{1}=TArrow T1_1 T1_2".

apply andb_true in H0. inversion H0 as [Hbeq1 Hbeq2].

apply IHT1_1 in Hbeq1. apply IHT1_2 in Hbeq2. subst... Qed.

## The Typechecker

_{11}T

_{12}for some T

_{1}and T

_{2}).

Fixpoint type_check (Γ:context) (t:tm) : option ty :=

match t with

| tvar x => Γ x

| tabs x T

_{11}t

_{12}=> match type_check (extend Γ x T

_{11}) t

_{12}with

| Some T

_{12}=> Some (TArrow T

_{11}T

_{12})

| _ => None

end

| tapp t

_{1}t

_{2}=> match type_check Γ t

_{1}, type_check Γ t

_{2}with

| Some (TArrow T

_{11}T

_{12}),Some T

_{2}=>

if beq_ty T

_{11}T

_{2}then Some T

_{12}else None

| _,_ => None

end

| ttrue => Some TBool

| tfalse => Some TBool

| tif x t f => match type_check Γ x with

| Some TBool =>

match type_check Γ t, type_check Γ f with

| Some T

_{1}, Some T

_{2}=>

if beq_ty T

_{1}T

_{2}then Some T

_{1}else None

| _,_ => None

end

| _ => None

end

end.

## Properties

*sound*and

*complete*for the original has_type relation — that is, type_check and has_type define the same partial function.

Theorem type_checking_sound : ∀Γ t T,

type_check Γ t = Some T → has_type Γ t T.

Proof with eauto.

intros Γ t. generalize dependent Γ.

t_cases (induction t) Case; intros Γ T Htc; inversion Htc.

Case "tvar"...

Case "tapp".

remember (type_check Γ t

_{1}) as TO1.

remember (type_check Γ t

_{2}) as TO2.

destruct TO1 as [T

_{1}|]; try solve by inversion;

destruct T

_{1}as [|T

_{11}T

_{12}]; try solve by inversion.

destruct TO2 as [T

_{2}|]; try solve by inversion.

remember (beq_ty T

_{11}T

_{2}) as b.

destruct b; try solve by inversion.

symmetry in Heqb. apply beq_ty__eq in Heqb.

inversion H0; subst...

Case "tabs".

rename i into y. rename t into T

_{1}.

remember (extend Γ y T

_{1}) as G'.

remember (type_check G' t0) as TO2.

destruct TO2; try solve by inversion.

inversion H0; subst...

Case "ttrue"...

Case "tfalse"...

Case "tif".

remember (type_check Γ t

_{1}) as TOc.

remember (type_check Γ t

_{2}) as TO1.

remember (type_check Γ t

_{3}) as TO2.

destruct TOc as [Tc|]; try solve by inversion.

destruct Tc; try solve by inversion.

destruct TO1 as [T

_{1}|]; try solve by inversion.

destruct TO2 as [T

_{2}|]; try solve by inversion.

remember (beq_ty T

_{1}T

_{2}) as b.

destruct b; try solve by inversion.

symmetry in Heqb. apply beq_ty__eq in Heqb.

inversion H0. subst. subst...

Qed.

Theorem type_checking_complete : ∀Γ t T,

has_type Γ t T → type_check Γ t = Some T.

Proof with auto.

intros Γ t T Hty.

has_type_cases (induction Hty) Case; simpl.

Case "T_Var"...

Case "T_Abs". rewrite IHHty...

Case "T_App".

rewrite IHHty1. rewrite IHHty2.

rewrite (beq_ty_refl T

_{11})...

Case "T_True"...

Case "T_False"...

Case "T_If". rewrite IHHty1. rewrite IHHty2.

rewrite IHHty3. rewrite (beq_ty_refl T)...

Qed.

End STLCChecker.