「SF-PLF」11. TypeChecking

Programming Language Foundations - A Typechecker for STLC

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

首先我们需要 check equality for types. 这里非常简单,如果是 SystemF 会麻烦很多,对 要做 local nameless 或者 alpha renaming:

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.

然后我们需要一个 refl 和一个 reflection,准确得说:「define equality by computation」,反方向用 refl 即可易证

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

直接 syntax directed,不过麻烦的是需要 pattern matching option

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

在课堂时提到关于 eqb_ty 的一个细节(我以前也经常犯,在 ML/Haskell 中……): 我们能不能在 pattern matching 里支持「用同一个 binding 来 imply 说他们两需要 be equal」?

1
2
3
4
5
(** instead of this **)
| 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

这里我们可以自己定义一个 Haskell do notation 风格的 monadic 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

最后我们需要验证一下算法的正确性: 这里的 soundness 和 completess 都是围绕 “typechecking function ~ typing relation inference rule” 这组关系来说的:

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

首先我们定义了 value 关系的函数版本 valuef, 然后我们定义 step 关系的函数版本 stepf:

以 pure STLC 为例:

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

证明用了一个 given 的非常夸张的 automation…

不过帮助我找到了 stepfstep 的多处 inconsistency:

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

Completeness

发现了 pair 实现漏了 2 个 case……然后才发现了 Soundness 自动化中的 valuef pair 问题

Extra (Mentioned)


Church Style vs. Curry Style Rice’s Theorem

CakeML

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