「SF-PLF」11. TypeChecking

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:

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 即可易证

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…

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」？

(** 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:

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.

好看一些吧反正：

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” 这组关系来说的：

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）

(** 还不能这么写 **)
| 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 为例：

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

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.

对于关系，一直就是 implicitly applied 的，在可用时即使用。
对于函数，我们需要手动指定 match 的顺序
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…

不过帮助我找到了 stepf 和 step 的多处 inconsistency:

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