Coqで依存型プログラミング: 型付きラムダ計算器の実装（６０行）

# 概要
依存型を使うと簡潔に言語内の言語実装ができます。本稿では、Coq内で型付きラムダ計算器を作ります。コード行数60行です。Coqで依存型プログラミングをするためのバイブル『[Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/)』通称CPDTの 9.2節 が元ネタですが、本稿のみで自己完結するよう配慮します。CPDTは無料で頒布されています。

型付ラムダ計算器の実装にあたって、基本部品が二つ必要です。一つはリストへの所属をあらわす`member`型です。もう一つは各要素の型が違っていてもよい混合リスト型 `hlist` です。これらは依存型プログラミングをするうえで色々な箇所で登場します。本稿では両者をあわせて紹介します。

# 0. さいしょ
ファイル冒頭にいつものおまじないを書きます:
```coq
Set Implicit Arguments.

Require Import List Bool Arith Lia.
Import ListNotations.
```

# 1. member型
`List.In`の Type バージョンを作ります。`List.In` は recursive に定義されていますが`member` は Inductive に定義します:

```coq
Inductive member (A:Type) (a:A) : list A -> Type :=
| M1 : forall ls, member a (a :: ls)
| MS : forall x ls, member a ls -> member a (x :: ls).

Arguments M1 {A a ls}.
Arguments MS {A a x ls} _.
```

先頭に所属しているとき`M1`という証明項があり、二番目に存在しているときは `MS M1`という証明項がある、といった感じです。`member`型の値は、たんなる所属情報だけでなく「リストのどこに所属しているのか」という位置情報をも持っており、リストの要素取得の際に役立ちます。その意味で`Fin.t`に似ているので、構成子の名称も似せます。

使用例を挙げます:

```coq
Check M1: member 4 [4;8;7;10;11].
Check MS M1: member false [true;false;true;true;true].
Check MS (MS M1): member 77 [1;2;77;4;5;6;7].
```

# 2. hlist 型

二つ目の基本部品である混合リストです。Pythonでのリスト `[0, true, "hello"]` のように型が異なるものたちをまとめるための部品です。

混合リストでは要素の型が違っていても、要素の型の型は同じです。なので「要素の型のリスト `list A`」に依存させる形でInductiveに定義します。consするのは Aの値に依存した型の値(つまりA型, A→Typeの型の値)というわけです。例えば `nat`と`bool`の混合リストでは`Set`がAになり、A→Typeとしては恒等関数――natならnat、boolならbool――をとればよさそうです:

```coq
Inductive hlist (A:Type) (B:A->Type) : list A -> Type :=
| hnil : hlist B nil
| hcons : forall (x : A) (ls : list A), B x -> hlist B ls -> hlist B (x :: ls).

Arguments hnil {A B}.
Arguments hcons {A B x ls} _ _.
Infix ":::" := hcons (right associativity, at level 60).
```

例を挙げます::

```coq
Definition ls := [bool;nat;bool;nat].
Definition hls := false:::1:::true:::7:::hnil: hlist (@id Set) ls.
```

前章で定義した `member`型 を使えばhlistの要素選択関数が実装できます。ポイントは、

- `hnil`の場合は`member`型の証明項が得られるはずがないので、その枝では適当にunit型の値を返してしまえばよい
- `hcons`の場合は `member`型が M1 なら cons にくっついてきた値をそのまま返せばよくて、そうでない場合は一つ削って再帰呼び出しでOK（cons にくっついているのが一つ削れたhlistで MS を一つ削れば member も一つ削ったことになる）
- Coqに停止性を教えるために、いったんabstractionしてからすぐにapplyするというTipsを使う

```coq
Fixpoint hget (A:Type) (B:A->Type) (a:A) (ls:list A) (hls : hlist B ls): member a ls -> B a :=
  match hls with
    | hnil => fun mem =>
      match mem in member _ ls' return (if ls' then B a else unit) with
        | M1  => tt
        | MS _ => tt
      end
    | hcons x hls' => fun mem =>
      match mem in member _ ls' return (match ls' with
                                        | nil => Empty_set
                                        | x' :: ls'' => B x' -> (member _ ls'' -> B a) -> B a
                                      end) with
        | M1  => fun x _ => x
        | MS mem' => fun _ y => y mem'
      end x (hget hls')
  end.
```

先の例を再掲するとともに選択関数が動作しているのを確かめます:


```coq
Definition ls := [bool;nat;bool;nat].
Definition hls := false:::1:::true:::7:::hnil: hlist (@id Set) ls.
Definition idx := MS M1: member nat ls.
Example get01 :  1 = hget hls idx. reflexivity. Qed.
Example get02 :  true = hget hls (MS (MS M1)). reflexivity. Qed.
```

# 3. 型付きラムダ計算
原始型/atmic type がただ一つ `U` であるような型付きラムダ計算を実装します。つまり型として `U`, `U→U`,`U→(U→U)`, .... などのみが存在します。すると型`ty`をInductiveに定義できて、それらをCoqの`unit`型とそれらに関連する関数として解釈できます(denotational semantics)。

```coq
Inductive ty:= 
| U
| Arrow: ty->ty->ty.

Fixpoint tyD (t:ty) := match t with
| U => unit
| Arrow a b => (tyD a)->(tyD b)
end.
```

ラムダ項は、list ty と ty の値に依存させる形で定義します。その第一パラメータ `list ty`は自由変項のリストを意図し、第二パラメータの`ty`は自身の型を意図します。意図を汲めば解釈はほぼ自明です。tyの解釈先が `unit` だったり `unit->unit` だったりと型が異なるので、`list ty` の解釈は混合リストとなります。:

```coq
Inductive exp: list ty -> ty -> Type:=
| Const ts: exp ts U
| Var ts t: member t ts -> exp ts t
| App ts d r: exp ts (Arrow d r)-> exp ts d -> exp ts r
| Abs ts d r: exp (d::ts) r -> exp ts (Arrow d r).

Fixpoint expD (ts:list ty) (t:ty) (e: exp ts t) : hlist tyD ts -> tyD t :=
match e with
| Const _ => fun _ => tt
| Var mem =>  fun s => hget s mem
| App  e1 e2 => fun s => (expD e1 s) (expD e2 s)
| Abs e' => fun s => fun x => expD e' (x:::s)
end.
Arguments Const {ts}.
```

例をいくつか記載します:

```coq
(* U*)
Check expD Const hnil : tyD U. 
Example const01: tt = expD Const hnil. reflexivity. Qed.
(*U->U *)
Check expD (Abs (d:=U) (Var M1)) hnil: tyD (Arrow U U).
Example uuau:  (expD (Abs (d:=U) (Var M1)) hnil) tt = tt. reflexivity. Qed.
(* apply U to U->U in DSL *)
Check expD (App (Abs (Var M1)) Const) hnil: tyD U.
Example uuau': tt = expD (App (Abs (Var M1)) Const) hnil. reflexivity. Qed.
(* (U->U)->U *)
Check expD (Abs (d:=Arrow U U) Const) hnil :tyD (Arrow (Arrow U U) U).
Example uuuauu: tt = expD (Abs (d:=Arrow U U) Const) hnil (fun x:unit => x) . reflexivity. Qed.
(* U->U->U *)
Check expD (Abs (d:=U) (Abs (d:=U) (Var M1))) hnil.
Example uuuauau: tt = expD (Abs (d:=U) (Abs (d:=U) (Var M1))) hnil tt tt. reflexivity.  Qed.
```

以上で型付きラムダ計算をCoq上に埋め込むことができました。表示関数を実装しただけですが、それだけで以下の成果が得られました

- 評価: `expD` 自身が評価器となっています
- 型システム: ラムダ計算での型システムはCoqの型チェッカに埋め込まれているのですでに実装済みです。ラムダ計算で型が通らないラムダ項は、Coqにより記述さえできません。
- 停止性: `expD` はFixpointで実装されており、Coqによって停止することが保証されています

# 4. コード

```coq
Set Implicit Arguments.

Require Import List Bool Arith Lia.
Import ListNotations.

(* member *)
Inductive member (A:Type) (a:A) : list A -> Type :=
| M1 : forall ls, member a (a :: ls)
| MS : forall x ls, member a ls -> member a (x :: ls).

Arguments M1 {A a ls}.
Arguments MS {A a x ls} _.

(* hlist *)
Inductive hlist (A:Type) (B:A->Type) : list A -> Type :=
| hnil : hlist B nil
| hcons : forall (x : A) (ls : list A), B x -> hlist B ls -> hlist B (x :: ls).

Arguments hnil {A B}.
Arguments hcons {A B x ls} _ _.
Infix ":::" := hcons (right associativity, at level 60).

Fixpoint hget (A:Type) (B:A->Type) (a:A) (ls:list A) (hls : hlist B ls): member a ls -> B a :=
  match hls with
    | hnil => fun mem =>
      match mem in member _ ls' return (if ls' then B a else unit) with
        | M1  => tt
        | MS _ => tt
      end
    | hcons x hls' => fun mem =>
      match mem in member _ ls' return (match ls' with
                                        | nil => Empty_set
                                        | x' :: ls'' => B x' -> (member _ ls'' -> B a) -> B a
                                      end) with
        | M1  => fun x _ => x
        | MS mem' => fun _ y => y mem'
      end x (hget hls')
  end.

(* typed lambda calculation with dependent types *)
Inductive ty:= 
| U
| Arrow: ty->ty->ty.

Fixpoint tyD (t:ty) := match t with
| U => unit
| Arrow a b => (tyD a)->(tyD b)
end.

Inductive exp: list ty -> ty -> Type:=
| Const ts: exp ts U
| Var ts t: member t ts -> exp ts t
| App ts d r: exp ts (Arrow d r)-> exp ts d -> exp ts r
| Abs ts d r: exp (d::ts) r -> exp ts (Arrow d r).

Fixpoint expD (ts:list ty) (t:ty) (e: exp ts t) : hlist tyD ts -> tyD t :=
match e with
| Const _ => fun _ => tt
| Var mem =>  fun s => hget s mem
| App  e1 e2 => fun s => (expD e1 s) (expD e2 s)
| Abs e' => fun s => fun x => expD e' (x:::s)
end.
Arguments Const {ts}.
```