このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

Call-By-Push-Valueの不純な関数型言語

雑記／備忘

パウル・ブラ・レヴィ（Paul Blain Levy）による計算モデルにCall-By-Push-Value（CBPVと略記）があります。最近知ったのですが、昔（20世紀）から有名らしいです。

CBPVの理論には、ラムダ計算の拡張である項言語（term language）が登場するのですが、コレ気に入りました。最初から不純なプログラム（impure program）を視野に入れています。僕は不純が好きですからね。不純な計算モデルであるデカルト作用圏やフレイド圏と相性が良さそうです。それと、積分を入れたラムダ計算とも何か関係がありそうな予感。

レヴィのCBPV言語は、ラムダ計算の項言語の拡張ですが、かなり現実の言語に近いものです。そのまま実装しても実用になりそうです。どんな構文かを紹介します。僕の好みを入れて少し変形します。

内容：

前置き

Call-By-Push-Valueについては、Call-By-Push-Value FAQからたどって情報を得られます。レヴィの論文は http://www.cs.bham.ac.uk/~pbl/papers/ にリストされています。僕が拾い読みした論文は、"Call-By-Push-Value: A Subsuming Paradigm (Extended Abstract)"と"Adjunction models for call-by-push-value with stacks"です。

CBPV言語は、時代と共に多少の変更がなされています。例えば、初期のキーワードproduceは後ではreturnになっています。基本的には、より新しい"Adjunction models for call-by-push-value with stacks"のほうの構文に基いて紹介しますが、let文は初期の形を採用します。初期の let x be V が let V be x へと、変数をキーワードbeの後に書く形に変更されました。僕自身は「左から右」派なので、let V be x （式Vを変数xに突っ込む）の順は好きです。しかし、多くの人が違和感を抱きそうなので x = V の形を採用します。

文と式の区別

変数の型と式と型については、普通の型付きラムダ計算と同じです。型コンテキストΓのもとでの型判断（型シーケント）は Γ ⇒ V:A のように書けます。Vは式でAはデータ型（値の型）です。文（プログラム）にも型があるので、Γ ⇒ M:P のようなプログラムの型判断も意味を持ちます。

型に関しては次のルールがあります。

  1. Aがデータ型（値の型）なら、Prog(A) はプログラムの型である。
  2. Pがプログラムの型なら、Thunk(P) はデータ型である。Thunk(P) は、P型のプログラムをデータとみなしたモノのデータ型である。プログラム（の挙動）を表現するデータをここではサンク（thunk）と呼ぶ。
  3. AとBがデータ型のとき、A×B はAとBのペアの型（直積型）を表す。
  4. Iが名前（または番号）の集合、i∈I に対してAi がデータ型のとき、Σ(i∈I | Ai) は（タグ付きの）直和型であり、これもデータ型である。
  5. Iが名前（または番号）の集合、Pi がプログラムの型のとき、Π(i∈I | Pi) は（タグ付きの）直積型であり、プログラムの型となる。
  6. Aがデータ型、Pがプログラムの型のとき、A→P はA型の引数を取りPとして振る舞うプログラムの型である。

名前付き直和データ型と名前付き直積プログラム型の構成では、識別子（名前、番号、タグ、ラベル）の集合であるIが使われます。識別子の構文や分類にはここでは触れません。実際のプログラム言語では、名前の構文や分類（名前空間の構造）は重要な問題となります。

A→P は一種の指数型です。しかし、P→Q のようなプログラム型どうしの指数を定義してないことに注意してください。高階の式はあっても、高階のプログラムはないのです。引数はあくまでデータであり、プログラムを引数にしたいならサンクを作るしかありません。Thunk(P)→Q という型は許されます。

サンクの実体は特に規定しませんが、クロージャのようなデータを想定してもいいし、コンパイルされたコード（バイト列）へのポインターと解釈してもかまいません。プログラムを表すナニカで、変数に代入したり、引数スタックにプッシュできるようなものがサンクですね。

thunkという言葉に関しては、higeponさんの http://d.hatena.ne.jp/higepon/20071202/1196605979 に、shiroさんによるコメントがあります。

式の型付け

式とそのデータ型は、通常の単純型付きラムダ計算と大差ありません。しかし、ラムダ抽象と適用は式を作るのではなくて文を作るので、式の構文はけっこう寂しいです。

  1. 変数は式である。
  2. V, Wが式のときペア (V, W) は式である。
  3. Mがプログラムのとき thunk M は式である。
  4. Vが式、i∈I が名前（または番号）のとき、@i V は式である。@iはタグと呼ぶ。

変数に束縛できるのは式だけなので、変数の型は必ずデータ型です。変数がプログラムの型を持つことはありません（これ、大事）。式の型判断を Γ ⇒ V:A の形で書いて、シーケントの推論として型付け規則を書きます。⇒' はプログラムに関する型判断の記号だとします。

      *
  -----------[公理]
  x:A ⇒ x:A

 Γ ⇒ V:A     Γ ⇒ W:B
 -------------------------[ペア]
    Γ ⇒ (V, W):A×B

       Γ ⇒' M:P
 ---------------------------[サンク]
 Γ ⇒ (thunk M):Thunk(P)

       Γ ⇒ V:Ai
  ------------------------------[直和入射]
  Γ ⇒ (@i V):Σ(i∈I | @i Ai)

文の種類と型付け

CBPV言語の文を、短い説明と共に列挙します。個々の文に関するコメントは後述します。また、ラムダ抽象、適用、ライブラリ、手続き呼び出しなどは別な節で述べます。

  1. return文 -- 評価した値を結果として戻してプログラムを終了します。
  2. let文 -- 式を変数に束縛し、その束縛のもとで文を実行します。
  3. to文 -- 文の結果を変数に束縛し、その束縛のもとで次の文を実行します。
  4. force文 -- サンクを実行します。
  5. match文 -- ペアを分解してから文を実行します。
  6. case文 -- 場合分けをします。タグが適合した文を実行します。

文の結果（これはデータ）は、return文で生成されます。let文とto文はどちらも束縛を作りますが、let文は式と変数、to文は文と変数を束縛します。force文はthunkで作ったサンクデータを実行する文です。match文とcase文は、レヴィのオリジナル構文ではpm文です。分かりにくいのでキーワードを変えて2つの文に分けました。match文はlet文を拡張すれば不要でしょう。適用とラムダ抽象は、ラムダ計算と同じですが、文に関するものです。

文の構文と型付けを同時に定義します。

       Γ ⇒ V:A
  ----------------------------[return文]
   Γ ⇒' (return V) :Prog(A)

  Γ ⇒ V:A      Γ, x:A ⇒' M:P
  ------------------------------[let文]
    Γ ⇒' (let x = V in M) :P

   Γ ⇒' M:Prog(A)   Γ, x:A ⇒' N:Q
  -------------------------------------[to文]
      Γ ⇒' (M to x in N) :Q

   Γ ⇒ V:Thunk(A)
  ------------------------------[force文]
   Γ ⇒' force(V) :P

   Γ ⇒ V:A×B     Γ, x:A, y:B ⇒' M:P
  ---------------------------------------[match文]
   Γ ⇒ (match V as (x, y) in M) :P

case文は分岐が2つの場合を書きます。実際は任意個数の分岐が許されます。

   Γ ⇒ V:(@1 A) + (@2 B)   Γ, x:A ⇒' M:P   Γ, x:B ⇒' N:P 
  -------------------------------------------------------------[case文]
   Γ ⇒' (case V as x in 1 => M | 2 => N end) :P

文に対する補足説明

return文は、式を、同じ値を持つ文とみなす方法を与えます。恒常的なデータを、そのデータを生成する動作に変換するとも言えるでしょう。多くのプログラミング言語が備えているreturn文に、多くのプログラマがいだいている直感的イメージで解釈していいと思います。

let文も素直に解釈すればいいかと。let文の直感的意味は、変数と式の束縛を作って、その束縛内でプログラムを実行することです。変数に代入（束縛）できるのは値（を表す式）に限る、というのも「そりゃそうだよな」という気がします。プログラムを変数に代入しているように見えても、実際にはサンクを作って代入しているので、より現実に近い定式化と言えます。

let文では式の値しか束縛できませんが、to文はプログラムの結果を束縛できます。return文とto文の組合せで、プログラムの動作（行為、振る舞い）の結果を値として取り出して名付けることができます。Kuwataさんと僕が開発していたCatyには（偶然ですが）、to文と同じ構文があります。M > x; N が M to x in N に相当する構文です -- 語順も意味も同じです。

force文は、thunkでデータとして閉じ込めたプログラムを実行します。execとかdoとかのキーワードだと感じが出るかもしれません。thunkはだいたいクロージャを作ることに対応し、forceがクロージャの実行なので、thunk/forceはカリー化／反カリー化に類似してます。後で、ラムダ抽象と適用も出てきますが、thunk/forceとの違いを見極める事は重要かも知れません。

match文とcase文は、どちらもパターンマッチングなので、レヴィはpm文としてひとまとめにしています。しかし、match文は直積で、case文は直和なので分けたほうがいいと思います。match文のほうは、let (x, y) = M in N という、ペアのパターンマッチング付きlet文があれば不要でしょう。あるいは、ペアzの射影（成分の取り出し）を x.1, x.2 とでもすれば、次の入れ子let文でmatch文を代用できます。

 let z = M in
 let x = z.1 in
 let y = z.2 in
 N

case文は、タグを目印として構成された直和型（排他的ユニオン型）のデータを、タグで仕分けして分岐します。V as x は、Vの値をxに束縛してから分岐の実行に進むことを意味します。case V in (1 as x) => M | (2 as y) => N end のように、分岐ごとに使う変数を変える構文もあります（一時、レヴィが使っていた）が、その必要性はないと思います。タグに番号（@1 と @2）を使ってますが、もちろん名前でもかまわないし、名前でないと人間には辛いでしょう。

このcase文も、Catyのwhen式と同じ意味とメカニズムです。もっとも、直和型を入れると、ほぼ必然的にこの構文になります。上記のmatch文をlet文に吸収して、キーワードcaseをmatchに置き換えたほうが普通っぽい構文でしょう。

抽象と呼び出し

ラムダ計算の拡張と言いながら、ラムダ抽象がまだ出てきてませんでした。ラムダ抽象の構文と型付けは次のとおり。

   Γ, x:A ⇒' M:P
  ----------------------[ラムダ抽象]
   Γ ⇒' λx:A.M :A→P

特に変わったことはありません。ただし、ラムダ抽象は文から文を作る操作である点に注意してください。ラムダ抽象を、関数を意味するfunとかfnとかのキーワードで、fun x:A -> M のように表すことがありますが、キーワードを使うならfunよりproc（手続きの意味）でしょう。λx:A.M は、proc x:A -> M という感じ。

次に適用ですが、レヴィは適用の中置演算子に`（バッククォート）を使っています。しかも、左に引数です。

   Γ ⇒ V:A   Γ ⇒' M :A→P
  -----------------------------[適用]
   Γ ⇒' V`M :P

V`M をキーワードで表すなら V into M とかでしょうか。適用がlet文と違うのは、変数を介在させてないことです。Mはラムダ抽象なので、変数の名前は文字通り“抽象”されていて、名前無しで計算を連結することが出来ます。これは、パイプ結合 V | M に近いとも言えます。

ラムダ抽象は無名の手続きを作る操作ですが、CBPV言語では、名前付きの手続きも作れます。λ{a := M} がその構文です。aは名前（または番号）で、Mは手続き本体となるプログラムです。名前付き手続きは一度にたくさん定義できて、λ{a := M, b :=N} も許されます。一般には次の形です。

  • λ{i := Mi | i∈I}

λ{i := Mi | i∈I} も、文（プログラム）を直積に組んだ文なのですが、普通の感覚で言えば、手続き定義の集まりなのでモジュールです。なのでここではモジュールと呼ぶことにします。入れ子にして、λ{m := λ{i := Mi | i∈I}, n := λ{j := Nj | j∈J} のようにも出来るので、階層化された名前空間も作れます。

モジュールMから名前がaである手続きを取り出すことを、レヴィは a`M と書いています。適用と同じ記法です。確かに、適用と名前ルックアップは類似しているのですが、区別したほうが分かりやすいと思うので、a@M とします。アットマークが、直和を作るときのタギングとカブってますが、文脈で判断可能だからいいとしましょう。

モジュールの構成と手続きの取り出しは次の規則で制御されます。

   Γ ⇒' Mi:Pi （すべての i∈I について）
  ----------------------------------------[モジュール]
   Γ ⇒' λ{i := Mi | i∈I} :Π(i∈I | Pi)


   Γ ⇒' M:Π(i∈I | Pi)
  -----------------------[手続き]
   Γ ⇒' a@M :Pa

レヴィは、このCBPV言語に対して色々な意味論を構成しています。今日は構文だけの紹介です。それでも、通常のプログラミング言語に近いので直感的な意味は想像しやすいでしょう。文は結果以外に副作用を持ってもよいので不純な計算を定式化しやすく、名前付き直積型でモジュール概念を入れられたりもするので、現実のモデル化に向いていると思います。