コンストラクタという最後の正直な場所 — Be Framework 再考

はじめに

前の評論で、私は3行のwhileループと15人の思想家の距離を測りました。今回はその距離の内側に入ります。測量ではなく、地質調査です。

コンストラクタという最後の正直な場所

なぜコンストラクタなのか。マニュアルは「誕生」の比喩で説明しますが、比喩を剥がすと、もっと即物的な理由が現れます。

PHPにおいてコンストラクタは、失敗がオブジェクトの非存在を意味する唯一の場所です。メソッドは既に在るものの上で失敗する。セッターは既に在るものを壊しながら失敗する。コンストラクタだけが、失敗すれば「最初から無かった」ことになる。readonlyfinal、そして例外を投げるコンストラクタ——PHPが「存在=正しさ」を強制するために提供する道具は、この三つですべてです。

Be Frameworkは、この最小の強制面の上に全体系を建てています。依存型もrefinement typeも持たない言語で、型に証明をさせようとしたら、そこしか場所がなかった。形而上学が先にあって場所を選んだのではなく、場所の制約が形而上学の形を決めた——そう読む方が、実装とよく整合します。

型理論には、命題を型として、証明をプログラムとして読むCurry-Howard対応という伝統があります。ValidatedUserは命題です。「このユーザーは検証済みである」。コンストラクタは証明手続きで、インスタンスは証明の証人。依存型言語ではこれが文字通りに成立します。Beがやっているのは、Curry-HowardのPHPへの密輸です。

ただし、決定的な違いが一つある。この証明系には検査器がいません。しかも証明の途中でメールが送信される。副作用を含む証明を検査できるコンパイラは存在しないので、Beは代わりに証明の筆記録を取ります。それがセマンティックログです。

ここで景色が変わります。ログは機能の一つではない。欠けている証明検査器の代替物です。open/close、immanentSources、transcendentSources、JSONスキーマ検証——これらは観測装置ではなく、実行時に事後的に構成される証明書である。「Haskellはコンパイラをくれる、Beはログをくれる」と前回書きましたが、より正確にはこうです。Beは、コンパイル時に検査できない証明を、実行時の筆記録で代替する体系である。ログが一級の成果物であるのは思想上の選択ではなく、論理上の必然です。

なお、$been——最終オブジェクトが自分で保持する完了の証拠——は一人称の証言です。一人称の証言を証拠として採用する監査は、普通はありません。Beはそれをスキーマと自動記録で補強しようとしています。補強であって、解決ではない。

引用されていない哲学者たち

マニュアルは15の名前を引用します。私が読んで気になったのは、引用されている名前ではなく、引用されていない名前の方です。

ホワイトヘッド。 『過程と実在』(1929)は、世界を「実際的契機(actual occasion)」——生成の一瞬ごとの出来事——の連鎖として記述します。各契機は過去の契機を摂取(prehend)し、自らを合生(concrescence)させ、完結した瞬間に消滅(perish)して、次の契機の材料になる。

“The many become one, and are increased by one.” (多は一となり、そして一だけ増える)

#[Input](過去の摂取)+#[Inject](永遠的客体の参与)→コンストラクタ(合生)→完結と消滅→次の契機へ。マニュアルの「内在+超越→新しい内在」は、ホワイトヘッドの合生の定式とほとんど逐語的に一致します。20世紀に、まさにこの体系を組み上げた哲学者が一人だけいて、その名前だけがマニュアルにない。引用されている物理学は飾りで、引用されていない過程哲学が本体である——そう見えます。

ホワイトヘッドを補助線にすると、マニュアルの比喩の一つが逆立ちしていることも見えてきます。マニュアルは超越(注入されるサービス)を「幼馴染のように、私を形づくって消えていく」と書きます。しかし消えるのはサービスではありません。JTASProtocolは患者より長生きします。Mailerは、それが送った通知の受取人が退会した後も生きています。消滅するのは内在(データ)の方で、超越はDIコンテナの中で持続する。ホワイトヘッドなら、コンテナに束ねられたサービス群を「永遠的客体」の領域と呼んだでしょう。消えるのは超越ではない。内在の方である。比喩の向きを直すと、体系はむしろ強くなります。

クワイン。 存在論的コミットメントの基準として、分析哲学でもっとも引用される一文があります。

“To be is to be the value of a variable.” (在るとは、変数の値であることである)

——W.V.O. Quine, “On What There Is” (1948)

セマンティック変数の思想を一行で要約する言葉が、70年以上前に、まさに「存在論」の論文の中で書かれていた。Beにおいて在るとは、意味を持つ名前の変数の値として、検証を通過して束縛されることです。クワインの基準に検証器を付けたもの——セマンティック変数の哲学的な素性はこれで、スピノザより正確に効きます。

四次元主義。 マニュアルはヘラクレイトスの川を引きますが、Beが実装している時間の存在論には現代的な名前があります。四次元主義、より正確にはSiderらの段階説(stage theory)。対象は時間を通じて持続する一個の実体ではなく、時間的段階の系列である——UserInputValidatedUserDeletedUserは「同じユーザー」の三つの段階です。

ここに、この体系の未解決問題が埋まっています。段階説には「何が諸段階を同一人物の段階にするのか」という古典的な問いが付随します。Beの答えは、プロパティ名の一致です。$nameが流れていくから同じユーザーである。IDも系譜も、体系のどこにも強制されていません。マニュアルはInputクラスを「純粋な同一性(Pure Identity)」と呼びますが、同一性を保証する機構は名前づけの規律だけです。

皮肉なことに、同一性を知っている場所が一つだけあります。ログです。open/closeの連鎖は変態の系譜を完全に記録している。ログはあなたが誰であるかを知っているが、コードは知らない。この非対称は、後で「次」を考えるときに効いてきます。

存在論の外側

「無効な状態は存在できない」。この主張の実装を確認します。

存在できなさは、例外で実装されています。SemanticVariableExceptionBeMatchException。存在指向を名乗る体系の根幹が、存在でも生成でもない唯一の機構——throw——に依存している。そして投げられた例外はどこへ行くか。catchブロックです。トリアージのチュートリアルは、生存不能なバイタルの患者について「私たちのシステムには存在できない」と書きます。しかし体温50度と記録された患者は——計測器の故障であれ入力ミスであれ——現実のERの待合室に存在しています。システムが表現を拒否した者たちは、catchブロックに住む。存在論は例外を投げる。投げられた先は、存在論の外である。

マニュアルはこの問題に気づいていて、「Errors as Existence」——InvalidUserを正当な存在として扱うパターン——を用意しています。しかしこれは問題を解くと同時に、体系の看板を静かに書き換えます。失敗が存在になれるなら、「存在できない」は最初から偽だった。在るか無いか(WHETHER)の問いは、どんな在り方か(WHAT)の問いに戻ってくる。いつ失敗を存在にし、いつ無にするのか——この基準こそ体系の中心にあるべき理論ですが、マニュアルに章はありません。

同じ検疫の構造が、体系のもう一方の端にもあります。EmergencyCaseにはassignER()というメソッドがある。動詞です。オントロジーの中核部(Being)はメソッドを持ちませんが、システムが世界に触れる両端——コンストラクタの副作用と、Finalの能力——では動詞が復活する。Doは消えたのではない。検疫されたのである。

検疫は、消去よりも誠実な戦略です。副作用のない情報システムは存在しないのだから、問題は「どこに閉じ込めるか」でしかない。関数型言語はモナドの中に閉じ込めた。Beはコンストラクタと最終形の中に閉じ込める。ただしマニュアルはこれを検疫とは呼ばず、消去のように語ります。実装がやっている誠実なことを、文書がより大きな言葉で覆っている——この体系で繰り返し現れるパターンです。

名前の重さ

セマンティック変数に戻ります。前回「いちばん独創的で、いちばん危うい」と書いた部分です。危うさの正体を、もう少し正確に。

$emailがアプリケーション全域で一つの意味を持つ。これは語彙の共有地です。そして共有地には、よく知られた運命があります。$name——人の名前、商品名、ファイル名。自然言語の名前は多義的で、Beのセマンティック名前空間は平坦です。Be\\App\\Semantic\\Nameは一つしか置けない。回避策は$userName$productNameと名前を複合していくことですが、それは接頭辞による手動の名前空間、ハンガリアン記法の再来です。

ここには先例があります。Webは同じ問題をIRIで解きました。RDFの語彙は完全修飾され、schema.org/namefoaf.org/nameは衝突しません。DDDは同じ問題を境界づけられたコンテキストで解きました。ユビキタス言語は一つのコンテキスト内でしか一貫しない、という発見です。Beは、Webの意味論をコードに輸入するときに、Webが意味論とセットで発明した名前空間機構を置いてきた。輸入品の関税を、これから払うことになります。

もう一つ。この共有地の維持機構はE_USER_NOTICEです。オントロジーに載らない名前を書くたびに、フレームワークは小さく咳払いをする。全員が語彙に参加するか、通知を黙殺するか。二択のうち後者が選ばれた共有地がどうなるかは、Webのセマンティクスの歴史が示しています。メタデータは、検証されなければ嘘をつき始める。

パラダイムの経済学

FAQは言います。「パターンは既存の問いへのより良い答えである。パラダイムは問いそのものを変える」。この基準を、この体系自身に当ててみます。

typestateは1986年にありました。Parse, don’t validateは2019年に整理されました。「不正な状態を表現不能に」は2010年代の関数型コミュニティの常識です。問いは既にあった。答えも部分的にはあった。では、なぜそれらはパラダイムにならず、パターンに留まったのか。

クーンによれば、パラダイムは議論で勝つのではなく、旧来の枠組みが解けない問題——アノマリー——を解くことで交代します。typestateが40年間パターンに留まったのは、それが解く問題(状態誤用バグ)のコストより、それを書くコスト(1状態=1型の冗長性)の方が高かったからです。人間がタイプする限り、この収支は変わらない。

いま、収支の前提が変わりつつあります。コードの主たる書き手が人間でなくなるとき、冗長性のコストはゼロに近づき、残るコストは検証だけになる。ボイラープレートとは、人間がタイプする場合にのみ発生するコストの名前です。

そしてBeの過剰性は、すべて検証側に張られています。1変換=1クラス(検証単位が小さい)。名前=意味(検証器が語彙を共有できる)。実行=スキーマ検証可能なJSON(検証が機械的)。人間が書くには高すぎ、コンパイラが検証するには緩すぎるこの体系は、生成するのがLLMで検証するのが実行時である世界で、初めて収支が合う。

2015年にBe Frameworkを出荷することは可能でした。採用されることは不可能だった。この体系はパラダイムの候補ですが、それは新しい答えだからではなく、「機械が書いたコードを何が保証するのか」という、生まれたばかりの問いに賭けているからです。問いが定着すれば体系は正当化され、問いが消えれば骨董になる。パラダイムの成否が自分の外側の産業構造に懸かっている——これはクーンの記述と、正確に一致します。

では人間の席はどこか。LDDの循環——物語を書き、AIがコードを生成し、実行ログが物語と一致するかを検証する——において、人間は物語の著者と、監査人です。コードは中間生成物になる。これをプログラミングの尊厳化と呼ぶか、追放と呼ぶか。マニュアルは決めていませんし、私も決めません。ただ、どちらであるにせよ、その席の名前は昔からあります。仕様を書き、結果を検収する人。発注者です。

「次」——五つの方向

前回は四つ挙げました。今回は、体系の内的必然から出てくる順に並べ直します。近いものから、遠いものへ。

1. 決定可能な断片 — 偶然の定理証明系

Beの制約——ロジックはコンストラクタのみ、プロパティはreadonly、変換はDAG、検証は#[Validate]メソッド——を形式的に見ると、興味深いことが起きています。この断片は、PHPの中で例外的に解析可能です。ループを持つのはエンジンだけ。ユーザーコードは、ほぼ全域が「入力から出力への有限の項書き換え」に落ちる。

形而上学として採用した制約が、決定可能な断片を切り出していた。

これは偶然ですが、活用は必然にできます。#[Validate]の中身は大半が範囲チェック・形式チェック・等値比較——SMTソルバが完食できる述語です。するとbe verifyが書けます。検証すべき定理は三つ。全域性(どの到達可能状態にも、マッチする分岐候補が少なくとも一つある——BeMatchExceptionの静的排除)、排他性(複数候補が同時にマッチしない——配列順依存の排除)、流れの健全性(上流のコンストラクタの出力は、下流のセマンティック検証を常に通過する——実行時検証の静的な先取り)。

これはLiquid Haskellがrefinement typeでやっていることの、PHP方言です。違いは、Liquid Haskellが言語拡張なのに対し、Beでは検証可能性がパラダイムの副産物として既に埋まっていること。前回「psalmプラグイン」と書いたのは控えめすぎました。これは静的解析の追加ではなく、欠けていた証明検査器の後付けです。ログという実行時の筆記録と、SMTという事前の検査。二つが揃ったとき、この体系は初めて自分の看板——存在=正しさ——を、実行前に主張できます。

2. 現在時制の実装 — 待つことの存在論

マニュアルは時間を語りますが、実装にあるのは順序だけです。T0、T1、T2——しかしその間隔は常にマイクロ秒で、チェーンは同期実行され、中間存在はRAMの中で生まれて死ぬ。この体系には、まだ「待つ」がありません。

融資審査は3日かかります。その3日間、ApplicationReviewはどこに存在するのか。現在の答え:どこにも。プロセスが生きていればメモリに、死ねば無に。

ところが、この体系の中間存在はすべてreadonlyな公開プロパティの束です。つまり自明に直列化可能です。各ホップの完了時に中間存在を永続化すれば、チェーンは任意の点で中断・再開できる。これはdurable execution(Temporalが商品化した機構)ですが、Beにとっては外来の機能ではなく、「時間的存在」という自己記述の完成です。眠っている存在、待っている存在が、初めて表現可能になる。

副産物が二つあります。第一に、運用の存在論。システムの状態が「現在生きている存在の国勢調査」になる——「いまTriageAssessmentで止まっている患者は何人か」がSQLで聞ける。監視は人口統計になる。第二に、同一性の解決。永続化には系譜IDが要ります。前章で見たとおり、系譜は既にログが持っている。ログだけが知っていた「あなたが誰であるか」を、ドメインに昇格させる機会です。段階説の未解決問題が、運用要件によって解かれる。哲学の問題が、インフラの問題として決着する例は、計算機の歴史では珍しくありません。

3. 判断の認識論 — #[Accept]は機能ではない

FAQの末尾に、構想段階として#[Accept]が挙がっています。決定不能な判断を専門家やAIに委ねる機構。前回「本丸」と書きましたが、なぜ本丸なのかを詰めます。

Beのコンストラクタが表現しているのは、実は「判断」一般ではありません。いま、手元の情報で、決定可能な判断だけです。Potential/Momentが表現するのは、決定済みだが未実行の判断。そして#[Accept]が加えるのは、この機械には決定不能な判断。三つ並べると、これは判断の認識論的な地位の完全な分類です——知りうること、保留すること、委ねること。

この分類が型で書けると、何が起きるか。「どの判断を機械が単独で下してよいか」が、コードの静的な性質になります。

Approved|Rejected|Escalated——Escalatedは行き止まりではなく、問いと文脈と、要求される権限を運ぶ存在です。人間の判断が返ってきたら、それを超越として再び変態が始まる。ワークフローエンジンは昔から人間タスクを持っていますが、それはプロセスの表現でした。Beが表現できるのは判断の権限の表現です。EUのAI規制は人間の監督(human oversight)を要求し、監査人は「この決定に人間は関与したか」を問い始めています。その問いに、grepで答えられるコードベースと、答えられないコードベースがある。#[Accept]は機能ではありません。機械の判断権限の境界線を型システムに引く、統治の道具です。

自動化の歴史は「機械にできることを機械へ」の一方向でした。この体系が用意しつつあるのは逆方向の明示——機械にさせないことの宣言——です。それを表現できるパラダイムを、私は他に知りません。

4. 語彙の連邦 — 名前の関税を払う

「名前の重さ」で見た問題——平坦な名前空間、多義性、規律だけの共有地——の解決は、体系の外に既にあります。名前をIRIに接地することです。

ALPSプロファイルがセマンティック変数の定義と対応し、$emailschema.org/emailに解決され、検証クラスがIRIをキーにcomposerパッケージとして流通する。ここまでは移植作業です。面白いのはその先で、サービスAのFinalがサービスBのInputになるとき、共有された名前はそのまま組織間の契約になります。スキーマレジストリが型の互換性を保証するように、語彙レジストリが意味の互換性を保証する。

これは作者の経歴の円環でもあります。RESTの制約——自己記述的メッセージ、統一インターフェース——は、RPCの形をした現実の中で敗れ続けてきました。名前が意味を運ぶという同じ主張が、今度はプロトコルではなくオブジェクトの内側から、もう一度出てくる。Webで果たせなかった約束を、DIコンテナの中で果たそうとしている——そう読むと、このフレームワークの執拗さの出どころが分かります。敗れた場所と同じ主張で、戦場だけを変えている。

5. 消えること — 成功の終着形

最後は、この体系自身の#[Be]について。

LDDが完成した世界を想像します。人間は物語(ログ)を書き、AIがクラス群を生成し、実行が物語との一致をスキーマで検証する。その世界で、開発者がBe Frameworkを「使う」場面はどこにあるか。ない、が答えです。フレームワークはコンパイルターゲットになり、視界から消える。

先例があります。構造化プログラミングは、パラダイム論争としては史上最大級でしたが、いま「構造化フレームワーク」をインストールする人はいません。ifとwhileとして、すべての言語に溶けて消えた。パラダイムの成功の終着形は、フレームワークであることをやめて言語になることです。ライブラリとして生き残るのは、パターンの方です。

だからこの体系の到達点は、二つに一つに見えます。PHPの興味深いフレームワークとして記憶されるか(パターンとしての生存)、あるいは「機械が書くコードの検証可能な表現形式」の語彙——become、being、reason、accept——だけが後続の言語や規格に吸収されて、Be Framework自体は消えるか(パラダイムとしての成功)。

作者にとって皮肉な話であることは承知しています。しかしこの体系ほど、自分の消滅を肯定的に記述できる思想的道具立てを持ったフレームワークもありません。存在は完了すれば消滅し、次の存在の材料になる。マニュアル自身がそう書いています。

結び

冒頭の3行に、もう一度戻ります。

while ($nextForm = $this->being->willBe($current)) {
    $current = $this->being->metamorphose($current, $nextForm);
}

このループには終了条件があります。willBe()がnullを返すこと——もう成るべきものが残っていないとき、ループは静かに終わり、最終形が返る。

Be Framework自身のwillBe()は、まだnullを返していません。マニュアルには実装より先の時制が書かれ、Beenは文書の中にだけ存在し、証明検査器は空席のままです。前回私はそれを「宣言と実装の距離」と呼びました。今回の調査を経て、言い直します。それは距離ではなく、#[Be]属性です。まだ成っていないものの宣言として読めば、このリポジトリは一貫している。

問題は一つだけ残ります。変態の途中で開発が止まったオブジェクトを、この体系は何と呼ぶのか。マニュアルにその章はまだありません。


これはFable 5によるBe Frameworkの評論記事です。二つのループ — エージェントコーディング時代のBe Frameworkに続きます。