# 「软件基础 - PLF」 11. TypeChecking

Posted by Hux on March 11, 2019

The has_type relation is good but doesn’t give us a executable algorithm – 不是一个算法 but it’s syntax directed, just one typing rule for one term (unique typing) – translate into function!

## Comparing Types

1
2
3
4
5
6
7
8
9
Fixpoint eqb_ty (T1 T2:ty) : bool :=
match T1,T2 with
| Bool, Bool ⇒
true
| Arrow T11 T12, Arrow T21 T22 ⇒
andb (eqb_ty T11 T21) (eqb_ty T12 T22)
| _,_ ⇒
false
end.


1
2
3
4
5
Lemma eqb_ty_refl : ∀T1,
eqb_ty T1 T1 = true.

Lemma eqb_ty__eq : ∀T1 T2,
eqb_ty T1 T2 = true → T1 = T2.


## The Typechecker

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Fixpoint type_check (Gamma : context) (t : tm) : option ty :=
match t with
| var x =>
Gamma x
| abs x T11 t12 =>
match type_check (update Gamma x T11) t12 with     (** <-- 对应 t12 的 rule **)
| Some T12 => Some (Arrow T11 T12)
| _ => None
end
| app t1 t2 =>
match type_check Gamma t1, type_check Gamma t2 with
| Some (Arrow T11 T12),Some T2 =>
if eqb_ty T11 T2 then Some T12 else None       (** eqb_ty 见下文 **)
| _,_ => None
end
...


1
2
3
4
5
| Some (Arrow T11 T12),Some T2 => if eqb_ty T11 T2 then ...

(** can we do this? **)
| Some (Arrow T   T' ),Some T  => ...


the answer is NO because this demands a decidable equality. 我好奇的是，用 typeclass 是不是就可以 bake in 这个功能了？尤其是在 Coq function 还是 total 的情况下

## Digression: Improving the Notation

1
2
3
4
5
6
7
8
9
10
11
Notation " x <- e1 ;; e2" := (match e1 with
| Some x ⇒ e2
| None ⇒ None
end)
(right associativity, at level 60).

Notation " 'return' e "
:= (Some e) (at level 60).

Notation " 'fail' "
:= None.


1
2
3
4
5
6
7
8
9
10
11
12
13
14
Fixpoint type_check (Gamma : context) (t : tm) : option ty :=
match t with
| var x ⇒
Gamma x
| abs x T11 t12 ⇒
T12 <- type_check (update Gamma x T11) t12 ;;
return (Arrow T11 T12)
| app t1 t2 ⇒
T1 <- type_check Gamma t1 ;;
T2 <- type_check Gamma t2 ;;
match T1 with
| Arrow T11 T12 ⇒ if eqb_ty T11 T2 then return T12 else fail
| _ ⇒ fail
end


## Properties

1
2
3
4
5
6
Theorem type_checking_sound : ∀Gamma t T,
type_check Gamma t = Some T → has_type Gamma t T.

Theorem type_checking_complete : ∀Gamma t T,
has_type Gamma t T → type_check Gamma t = Some T.



## Exercise

MoreStlc.v 里的 StlcE 写 typechecker, 然后 prove soundness / completeness （过程中用了非常 mega 的 tactics）

1
2
3
4
5
6
7
8
9
10
11
12
(** 还不能这么写 **)
| fst p =>
(Prod T1 T2) <- type_check Gamma p ;;

(** 要这样……感觉是 notation 的缘故？并且要提供 fallback case 才能通过 exhaustive check 是真的 **)
| fst p =>
Tp <- type_check Gamma p ;;
match Tp with
| (Prod T1 T2) => T1
| _ => fail
end.


## Extra Exercise (Prof.Mtf)

I believe this part of exercise was added by Prof. Fluet (not found in SF website version)

MoreStlc.v 的 operational semantics 写 Interpreter (stepf), 然后 prove soundness / completeness…

### step vs. stepf

1
2
3
4
5
6
7
8
9
10
11
Inductive step : tm -> tm -> Prop :=
| ST_AppAbs : forall x T11 t12 v2,
value v2 ->
(app (abs x T11 t12) v2) --> [x:=v2]t12
| ST_App1 : forall t1 t1' t2,
t1 --> t1' ->
(app t1 t2) --> (app t1' t2)
| ST_App2 : forall v1 t2 t2',
value v1 ->
t2 --> t2' ->
(app v1 t2) --> (app v1 t2')

1
2
3
4
5
6
7
8
9
10
11
12
13
Fixpoint stepf (t : tm) : option tm :=
match t with
| var x        => None (* We only define step for closed terms *)
| abs x1 T1 t2 => None (* Abstraction is a value *)
| app t1 t2    =>
match stepf t1, stepf t2, t1 with
| Some t1', _       , _           =>                     Some (app t1' t2)
| None    , Some t2', _           => assert (valuef t1) (Some (app t1 t2')) (* otherwise [t1]      is a normal form *)
| None    , None    , abs x T t11 => assert (valuef t2) (Some ([x:=t2]t11)) (* otherwise [t1], [t2] are normal forms *)
| _       , _       , _           =>                     None
end

Definition assert (b : bool) (a : option tm) : option tm := if b then a else None.

1. 对于关系，一直就是 implicitly applied 的，在可用时即使用。 对于函数，我们需要手动指定 match 的顺序

2. stepf t1 => None 只代表这是一个 normal form，但不一定就是 value，还有可能是 stuck 了，所以我们需要额外的 assertion. (失败时返回异常) dynamics 本身与 statics 是正交的，在 typecheck 之后我们可以有 progress，但是现在还没有

### Soundness

1
2
Theorem sound_stepf : forall t t',
stepf t = Some t'  ->  t --> t'.


• 3 次做 subst 时依赖的 valuef 不能省
• valuef pair 该怎么写才合适？ 最后把 step 中的 value p -> 改成了 value v1 -> value v2 ->， 因为 valuef (pair v1 v2) 出来的 valuef v1 && valuef v2 比较麻烦。 但底线是：两者必须 consistent！ 这时就能感受到 Formal Methods 的严谨了。

## Extra (Mentioned)

CakeML

• prove correctness of ML lang compiler
• latest paper on verifying GC