LoginSignup
4
3

More than 1 year has passed since last update.

@41semicolon(41semicolon)

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

Last updated at Posted at 2022-04-05

概要

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

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

0. さいしょ

ファイル冒頭にいつものおまじないを書きます:

Set Implicit Arguments.

Require Import List Bool Arith Lia.
Import ListNotations.

1. member型

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

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に似ているので、構成子の名称も似せます。

使用例を挙げます:

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――をとればよさそうです:

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

例を挙げます::

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を使う
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.

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

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

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 の解釈は混合リストとなります。:

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

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

(* 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. コード

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}.
4
3
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
4
3