本ブログは 2026 年 4 月 17 日に公開された Amazon Science Blog “ Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine ” を翻訳したものです。 Isabelle/HOL は、数学的な記述の表現力、自動化、スケーラビリティのバランスによって、世界初の形式的に検証されたクラウドハイパーバイザーを実現しました。 2025 年の Amazon re:Invent カンファレンスにおいて、Amazon Web Services (AWS) は Nitro Isolation Engine (NIE) を発表しました。NIE は、お客様のデータのセキュリティを確保しながら AWS のお客様にリソースを提供する役割を担うソフトウェアモジュールです。あわせて AWS は、 Isabelle/HOL という定理証明支援系 (proof assistant) を使用して、この Isolation Engine の正当性とセキュリティ保証を形式的に検証したことも発表しました。世界初の形式的に検証されたクラウドハイパーバイザーとして、NIE はクラウドセキュリティの新しい標準を打ち立てています。 Isabelle はもともと ケンブリッジ大学 と ミュンヘン工科大学 で開発され、現在は世界中の機関や個人による数多くのコントリビューションを取り込んでいます。 定理証明支援系とは、人間のユーザーが形式的証明を構築するのを支援する自動化ツールです。その対象は、数学の定理からハードウェアやソフトウェアシステムの妥当性まで、あらゆるものに及びます。広く使われている定理証明支援系はいくつかありますが、私たちが Isabelle/HOL を選んだのは、表現力、自動化、証明の読みやすさ、スケーラビリティのバランスが私たちの用途に最も適していたからです。これは具体的にどういうことなのでしょうか? コンピュータによる論理的推論 数学に決まった言語というものはありませんが、プログラミング言語が計算タスクを表現するのと同じように、数学的推論を表現するための言語を作ることができます。そして、プログラミング言語に表現力とパフォーマンスのトレードオフがあるように、数学的言語にも表現力と自動化のしやすさのトレードオフがあります。形式的証明の構築は時間がかかり、極めて根気のいる作業であるため (ボトルの中に船を組み立てる作業に似ています)、自動化は不可欠です。 形式的証明の構築は、ボトルの中に船を組み立てる作業に似ています。厳格な論理的制約の中で、すべての部品を正確に組み立てなければなりません。Isabelle/HOL は、この緻密な作業を可能にするツールを提供します。 最も初歩的な数学的言語はブール論理です。これは、AND、OR、NOT といった論理演算子の世界です。この言語は非常にシンプルであるため、強力な自動ソルバーが存在します。2016 年、カーネギーメロン大学の Marijn Heule 教授 (現在は Amazon Scholar ) とその同僚たちは、未解決の数学的問題であるブール・ピタゴラス数問題をブール論理に符号化し、自動ソルバーを使って、200 テラバイトという 史上最大の証明 を作り上げました。 一階述語論理 と呼ばれるより豊かな数学的言語では、整数などの対象領域について語り、その領域上の関数を定義できます。また、「すべての～について」や「～が存在する」という 量化子 を主張に含めることで、ブール論理を超える表現が可能になります。この種の言語では、「2 より大きいすべての素数は奇数である」といった文を表現できます。また、Lewis Carroll による次の定理を証明することもできます。 ワルツを踊るアヒルはいない。ワルツを断る士官はいない。私の家禽はすべてアヒルである。ゆえに、私の家禽の中に士官はいない。 しかし、ほとんどの人は、プログラミングと同じように型を定義できる、さらに強力な数学的言語を好みます。 高階論理 には、 Haskell などの関数型プログラミング言語に見られるような関数型さえ存在します。高階論理は一階述語論理よりもはるかに豊かで、「 数 1 を含み、加法について閉じているすべての集合は、すべての正の整数を含む 」といった文を表現できます。数学の大部分を表現できるほど豊かであると考えられています。 最も豊かな数学的言語である 依存型理論 では、型が任意の値をパラメータとして取ることさえ可能です。例えば T(i) のように、 i を整数とすることができます。この種の言語で最もよく知られているのは Lean と Rocq です。 一階述語論理には強力な自動定理証明器が存在しますが、高階論理やそれ以上の言語では、完全な自動化は利用できません。これが表現力の代償です。 定理証明支援系 を使えば、ユーザーは部分的な自動化の支援を受けながら対話的に証明を構築でき、独自の証明探索をコーディングすることも可能です。定理証明支援系は、論理法則への厳格な準拠を強制します。これは通常、定理を作成する権限をコードの限られた部分にのみ与えるカーネルアーキテクチャによって実現されます。 定理証明支援系は、非常に大規模になり得る形式的仕様の階層を対話的に開発することもサポートします。例えば、Nitro Isolation Engine (NIE) の検証は、Graviton-5 プロセッサのアーキテクチャの仕様、ハイパーコールの Rust コードとその機能的正当性、そして証明すべきセキュリティ特性の仕様の上に成り立っています。形式的証明を構成する 25 万行の大部分は、これらの仕様が占めています。 高階論理は、密接に関連する 2 つの定理証明支援系である HOL と HOL Light でサポートされており、1990 年代からハードウェア設計、浮動小数点アルゴリズム、純粋数学の検証に使われてきました。AWS のシニアプリンシパルアプライドサイエンティストである John Harrison は HOL Light を開発し、暗号アルゴリズムの最適化バージョンを検証することで、Amazon の Graviton2 チップにおけるデジタル署名の パフォーマンスを最大 94% 向上 させました。このコードは繊細であり、網羅的なテストは 現実的ではありません 。このような重要なソフトウェアをデプロイする前に取り得る手段は、完全な機能的正当性の形式的検証しかありませんでした。しかし、ここで注目したいのは Isabelle/HOL です。 Isabelle/HOL の概要 Isabelle/HOL と他の HOL システム (いずれも高階論理に基づいています) の最も目に見える違いは、その仕様記述言語と証明言語です。ほとんどの定理証明支援系では、ユーザーは証明したいことを記述した後、一種のモグラたたきゲームのように、元のゴールを一連のサブゴールに置き換えるコマンドを次々と続けていきます。Isabelle では (Lean でもある程度は)、証明言語によって望ましい中間ゴールを明示的に書き出すことができるため、証明プロセスをより適切に制御でき、より読みやすい証明ドキュメントが得られます。 オンラインには多くの例 があります。 その他の 注目すべき機能 は以下のとおりです。 Rust 言語のかなりの部分を仕様に埋め込むことを可能にした ユーザー設定可能なパーサー 例えば + に、さまざまな数値型だけでなくマシンワードやその他の適切な文脈でも自然な意味を与える、原則に基づいたオーバーロードのための 型クラス 仕様の階層を定義し、証明の中でさえさまざまな方法で解釈できる軽量なモジュールシステムである ロケール (locales) 単純化と後ろ向き連鎖による証明探索を通じた、強力な 組み込みの自動化 さらに強力な外部の自動化にワンクリックでアクセスできる sledgehammer 実際には偽である主張を特定するための 反例発見ツール 適合性のテストに使用した、実行可能な高階仕様からの コード生成 NIE の検証にあたっては、まず 分離論理 (separation logic) と呼ばれる特化した言語を Isabelle/HOL の上に実装することから始めました。分離論理は、共有リソースを操作するプログラムコードの検証のために設計されたものです。私たちは独自の証明自動化をコーディングし、組み込みの自動化も活用しました。そのため、分離論理を使いつつ、必要に応じて通常の高階論理も使うことができました。Isabelle は、非常に巨大なサブゴールにも対処できるほど堅牢かつ効率的であることがわかりました。市販のラップトップを使って、25 万行の証明を 30 分で実行できたのです。 Isabelle/HOL の応用事例 NIE 以前の Isabelle の応用事例として最も印象的なのは、おそらく広く使われているマイクロカーネルである seL4 の検証 でしょう。この証明も最初に発表された時点では約 25 万行でしたが、現在ではさらに長くなっています。seL4 の開発者たちは、マイクロカーネルの C 実装が抽象的仕様を詳細化したものであることを証明し、コア操作の完全な機能的正当性を実現しました。そして、検証されたコード部分ではバグが一切観測されていません。ただし、未検証の部分や形式化できない一部の前提条件をカバーするために、テストは依然として重要な役割を果たしています。 Isabelle は以下のプロジェクトでも使用されました。 エラーの特定、特にその型システムの 健全性の証明 を目的とした、 WebAssembly 言語のセマンティクスの形式化 Cogent プログラミング言語のための 検証フレームワーク の作成 分散編集に使用される、競合のないレプリケートデータ型 (CRDT) のアルゴリズムの 正当性の証明 純粋数学における 数多くの結果の形式化 抽象レベルでの 暗号プロトコルの検証 Isabelle は無料のオープンソースソフトウェアであり、 ダウンロードして利用 できます。十分なメモリを備えたマシンであれば、主要なオペレーティングシステムすべてで動作します。 著者について Larry Paulson Larry Paulson は、ケンブリッジ大学の計算論理学の名誉教授であり、Amazon Scholar です。 本ブログは Security Solutions Architect の 中島 章博 が翻訳しました。

.images-row {width: 100% !important;} Developer Engagementブロックの @ikkou です。2026年5月22・23日の2日間にわたりベルサール羽田空港で「TSKaigi 2026」が開催されました。 ZOZOはGold Sponsorとして協賛し、スポンサーブースを出展しました。ZOZOがTSKaigiに協賛するのは今回が初めてです。 technote.zozo.com 本記事では、前半はZOZOのWebフロントエンドエンジニアが気になったセッションを紹介します。後半では、ZOZOのスポンサーブースの様子と各社のブースにおけるコーディネートを写真中心に報告します。 ZOZOのWebフロントエンドエンジニアが気になったセッション 開発体験を左右するライブラリの API 設計 ― GraphQL スキーマ構築ライブラリから考える 「関数型プログラミング」を分解する.ts 純粋性について 型でエフェクトを表す いつテストを書くか？―ソフトウェア開発における安心と不安について考える LLM時代のリファクタリング戦略：AIエージェントによる段階的・安全なTS移行方法 TypeScript の型で副作用の実行順序を制御する ZOZOのスポンサーブースの紹介 協賛企業ブースのコーディネートまとめ おわりに ZOZOのWebフロントエンドエンジニアが気になったセッション 開発体験を左右するライブラリの API 設計 ― GraphQL スキーマ構築ライブラリから考える ssssota です。izumin5210さんの「 開発体験を左右するライブラリの API 設計 ― GraphQL スキーマ構築ライブラリから考える 」を紹介します。 speakerdeck.com このセッションでは、スキーマや型情報をいかにTypeScriptの実装に接続するかという観点で、既存ライブラリのアプローチやその長短を深ぼる内容でした。弊社ではOpenAPIを使っているケースが非常に多く、いかにOpenAPIスキーマを実装に接続するかは往々にして発生する問題の1つです。 セッションではGraphQLに焦点が当てられていましたが、スキーマから実装を生成するスキーマファースト、コードからスキーマを生成するコードファースト、コードファーストのうちDecoratorsを使うパターン、DSL的な独自のbuilderパターン、計3パターンについて評価していました。比較・評価軸として、1.スキーマと実装の分離、2.型整合性、3.DBモデルとの接続、の3軸を用いています。 スキーマと実装の分離については、スキーマファーストが優れているのは言うまでもありませんが分離する強いモチベーションがなければ優先度は低くなります。型整合性は採用するライブラリのtype ergonomicに依りますが、コードファーストなDSL builderパターンが強い傾向にあります。DBモデルとの接続においてはGraphQL特有と見ることができますが、コードファーストなDSL builderパターンで型整合問題と合わせて解決できることを示唆しています。 セッションの最後には、自作のライブラリでこのギャップを埋める取り組みとAIを用いた評価結果を紹介していました。気になる方はスライドも合わせて確認してみてはいかがでしょうか。 私自身、OpenAPIスキーマと実装の接続に関して関心があり、ライブラリ（ openapi-ts-hono ）を作った経験から非常に共感できるところがありました。もちろんGraphQLとはギャップがありますが、スキーマと実装の分離、型整合性などは感覚としてもっていながらも、改めて言語化されることで気付きのあるセッションでした。 「関数型プログラミング」を分解する.ts www_REM_zzz です。おーみーさんの『 「関数型プログラミング」を分解する.ts 』を紹介します。 tsk-2026-aumy.vercel.app 自分の話ですが、TypeScriptに入門する前はScalaを書いていた経験があります。当時はコップ本と呼ばれる本とHaskellの公式ドキュメントが日本語で関数型プログラミングに入門する入口でした。Object指向プログラミングとは全く別の世界からやってきたような考え方で、面白くもあり、苦労もした過去があります。 このセッションでは、そもそも関数型プログラミングとは何なのかの考え方に触れながら、TypeScriptで真の関数型はできないのかに触れられています。僕もTypeScriptで真の関数型が書けたらいいのにと思った一人です（OCaml書けよというのは一旦置いといて）。スライドの中で語られた関数型プログラミングは「いい感じのソフトウェアを作るため」というのは本質的だなと思いました。ついつい手段に引っ張られてしまうところがあるのですが、心に留めておきたいです。 純粋性について 特に純粋性についてのところはReactでも他のライブラリでも語られる部分であり、意味の純粋性の部分は悩ましいと感じたことがあるので共感しました。 // 「副作用を表す値」を返すだけ（純粋関数） function pureAlert ( msg : string ) { return [ "alert" , msg ] as const ; } // 副作用の実行は別の関数に委ねる function executeAction ( action : readonly [ "alert" | "confirm" , string ] ) { switch (action[ 0 ]) { case "alert" : alert (action[ 1 ]); break ; case "confirm" : confirm (action[ 1 ]); break ; } } const actions = [ pureAlert( "hey" ), pureAlert( "bye" ) ] ; actions. forEach (( a ) => executeAction(a)); 引用： https://tsk-2026-aumy.vercel.app/29 このような「何をするかの宣言」と「実行」が分離されている書き方は普段からできるし、メンテナンスを考えると普段から実践していきたいと思いました。 return は「この関数の呼び出し元（= 継続）に値を渡して戻る」という考え方はTSを書いていてなんとなく感じていたものがはっきりと言語化されてスッキリした気持ちになりました。 型でエフェクトを表す () => T // 特に何も起きない純粋な処理 () => Option< T > // 失敗しうる処理 () => Promise < T > // 非同期処理 これを徹底すると 関数の型を見るだけで「何が起きるか・何が起きないか」がわかる 純粋な部分と副作用のある部分が型レベルで分離される 「支払い処理を起こしうる部分」だけを特定して二重実行を防げる これはTypeScriptを堅牢に書くうえで実践したいと思います。ちょうど業務でも似たシチュエーションがあることを思い出して、まず「この関数は副作用を持つか？」を命名（ execute , get , ! 記法）で示すのが現実的な入口かなと思いました。 いつテストを書くか？―ソフトウェア開発における安心と不安について考える ジン（ @Jin_pro_01 ）です。自分の気になったセッションとして、 lacolacoさん の「 いつテストを書くか？―ソフトウェア開発における安心と不安について考える 」を紹介します。 docs.google.com このセッションでは、テストをどのような時に書くべきなのかを「開発者の安心と不安」を起点に問い直したlacolacoさんの気づきの共有、問いの提示、視点の提案をするというセッションでした。 セッションの中ではソフトウェアの保守性の本質は「変更容易性」であり、それは予期的変更容易性（変更する前に感じる不安）と経験的変更容易性（変更をする中で実際に感じる手応え）の二層モデルとして見ることができるとしていました。その上でテストはその両方にフィードバックを返すセンサーであるとし、変更前に感じる不安があるならそれを取り除く安心のために書き、変更のしやすさを試したり構造に問題が見つかったりするなら設計を見直すために書くという体系的な整理がされており、とても興味深いセッションでした。 自分が従事しているZOZOTOWNでは、新規機能の実装や既存機能の改修と並行で、フロントエンドリプレイスも各チームで進行しています。ZOZOTOWNの発展を止めずに開発を進める体制である一方、考慮すべきことが多く、自分にとっては比較的「予期的変更容易性」が低い状態だと表現できることに気づきました。そして、まさにこの「予期的変更容易性」を高めるためのテストへの投資価値が高いと感じました。 さらにAIを使ってコーディングをしていく時代に入り、開発の生産量が増える一方で、自分が直接書いていないコードや構造との距離は広がっていきます。その距離は新たな不安、つまり予期的変更容易性の低下にもつながると感じています。だからこそ変更の前後で「振る舞いが変わっていないこと」を担保し、その不安を取り除くセンサーとしてのテストの価値は、AI時代にこそますます高まっていくのだと考えました。 最大の収穫は、テストを書く目的を「ソフトウェアがソフトであり続けるための、変更容易性のセンサー」と説明できるようになったことです。テストはあくまで手段の1つと捉えつつ、ZOZOTOWNがソフトであり続けるために、他に何ができるかも考えていきたいと思いました。 LLM時代のリファクタリング戦略：AIエージェントによる段階的・安全なTS移行方法 いもけん（ @iimokeenpi ）です。「 LLM時代のリファクタリング戦略：AIエージェントによる段階的・安全なTS移行方法 」について紹介します。 speakerdeck.com このセッションは、JSのコードをAIエージェントを使い安全にTSに移行するというものでした。しかし、JSからTSへの移行のみならず日常的なリファクタリングにおいても活用できそうなノウハウが詰まっていました。 特に自分が興味を持った部分としては”test-firstフロー”と”役割ごとにサブエージェントを切り出す”の2つがあります。AIエージェントの使用有無にかかわらずリファクタリングの際にデグレには細心の注意を払って行っていきたいところです。そこで”test-firstフロー”というのは、デグレの防止策としても効果が高くAIエージェントとの相性もかなり良いなと感じました。 そして“役割ごとにサブエージェントを切り出す”という点に関してです。自分は基本的に全てOpusで乗り切ろうとしていたのですが、消費トークンの効率や時間的な効率の面でも損をすることが多々あります。なので役割ごとにサブエージェントを切り出し、モデルを使い分けることはすぐにでも実践したいと感じました。 TypeScript の型で副作用の実行順序を制御する 佐藤です。私が印象に残ったセッションは「 TypeScript の型で副作用の実行順序を制御する 」です。 speakerdeck.com Branded Typeは「 UserId と ProductId を区別するためのタグ付け」くらいにしか使えないと思っていましたが、Type-State Patternを使えばそれが実行順序の制御に転用できます。TypeScriptの型システムでここまで表現できるのかと、型に対する認識が更新されました。 加えて魅力的なのが、ライブラリ依存ゼロで既存コードに薄く入れられる点です。Effect-TSやXStateは強力ですが導入コストは高いです。Type-Stateパターンなら守りたい箇所だけにピンポイントで適用できます。 実際、 getServerSideProps 内に「バリデーション→取得→加工」のような実行順序を守らなければならない処理があり、これまではAIのルールや運用上の規約に頼らざるを得ませんでした。型で制御できるようになれば、コードレビューや属人的な注意に依存せず、エディタ上でミスを即座に検出できます。自分のチームに導入できないか実践したいと思えるトークでした。 サンプルコードは GitHubで公開されています 。既存ライブラリとの比較実装も含まれているので、ぜひ手元で動かしてみてください。 ZOZOのスポンサーブースの紹介 ZOZOのスポンサーブースとWebフロントエンドエンジニアたち ZOZOのスポンサーブースでは「 Google I/O 2026から帰国したばかりのZOZOフロントエンドエンジニア テックリード ssssota に挑戦！ 」と題したTypeScript & JavaScript Quizをメインコンテンツとして提供しました。日替わりで全10問、ブースにはその日のクイズから1問だけ掲示しました。 TypeScript & JavaScript Quiz Day 1 & Day 2 ZOZOブースでは #GoogleIO から帰国したばかりの Web フロントエンド テックリード @ssssotaro が考えた JavaScript & TypeScript Quiz を実施中です！難易度は高め！ぜひ挑戦してください！ #TSKaigi pic.twitter.com/7K9ZTt22Qq — ZOZO Developers (@zozotech) 2026年5月22日 ＼TSKaigi 2026 最終日／ 今日もクイズ企画を開催しています！昨日とは異なる問題で、今日は特典をゲットしやすくなっています！ オリジナル洗濯ネットをご用意していますので、ぜひご参加ください！ #TSKaigi pic.twitter.com/QwR6v2F96t — ZOZO Developers (@zozotech) 2026年5月23日 難しい！　ということが話題になり、とても多くの方に挑戦してもらいました。難しいのは作問者の意図通りですが、この「難しい」ということが反響を呼び、楽しんでもらえたのではないでしょうか。 No Bugs, Just Clean. というメッセージの込められた特製ノベルティの洗濯ネット クイズに挑戦し、7問以上正解した方には特製ノベルティの「洗濯ネット」をお渡ししました（Day 2は3問以上正解した方に変更）。 Day 1、Day 2の7問以上正解者 また、上位正解者の皆さんにはリーダーボードにもハンドルネームなどを書いてもらいました。2日間を通しての全問正解者は、Day 1が @uhyo_ さんと @vaaaaanquish さんの2名、Day 2が @U3Qc9 さんの1名だけでした。改めて全問正解おめでとうございます！ このTypeScript & JavaScript Quizに関する解説記事を別記事として公開しています。あのクイズの答えが気になるという方はもちろん、もう一度あのクイズに挑戦したい、当日できなかったので挑戦したい！　という方もぜひご覧ください。 techblog.zozo.com 10分セッションに登壇中のテックリード ssssota この難問揃いのクイズを作問したテックリードのssssotaはDay 2に「 ReactとSvelteのその先、Ripple-TS 」というタイトルで10分セッションにも登壇しています。こちらもあわせてご覧ください。 speakerdeck.com 協賛企業ブースのコーディネートまとめ ジン（ @Jin_pro_01 ）です。セッションを見たり、自社ブースに立ったりしている合間にTSKaigi 2026の全協賛企業ブースを回ってきました。当日の会場の様子を思い出しながら、各社の個性や雰囲気の出るデザイン・着こなしをぜひご覧ください。 ウェルスナビさん。 / @WealthNavi_Tech AVITAさん。 Dress Codeさん。 / @dresscode_com Hacobuさん。 / @MHacobu sattoさん。 / @satto_ai_agent アサインさん。 / @ASSIGN_dev レバレジーズさん。 PLAINERさん。 / @plainer_inc ビットキーさん。 / @bitkey_dev UPSIDERさん。 / @upsider_inc ニーリーさん。 / @nealle_pr LayerXさん。 / @LayerX_tech エブリーさん。 / @every_engineer スリーシェイクさん。 / @3shake_Inc ミツモアさん。 / @meetsmore Ubieさん。 / @UbieCorp_JP Nstockさん。 / @Nstock_jp プレイドさん。 / @PLAID_Tech ギークプラスさん。 / @GeekJapan1 ウォンテッドリーさん。 / @wantedly_dev サイボウズさん。 / @cybozuinsideout ドワンゴさん。 / @dwango_tech CodeRabbitさん。 / @Coderabbitaija シェルパ・アンド・カンパニーさん。 ファインディさん。 / @findy_code ディップさん。 / @dip_developers RightTouchさん。 / @righttouch_dev Gaji-Laboさん。 / @gaji_labo スタメンさん。 / @stmn_eng TOKIUMさん。 / @TOKIUM_Dev カオナビさん。 / @kaonavi_jp テイラーさん。 / @TailorERP_JP KINTOテクノロジーズさん。 / @KintoTech_Dev MOSHさん。 / @MOSHinc_jp 皆さん照れていたりウキウキしていたりしてよかったです！　ご協力いただいた皆さん本当にありがとうございました！ おわりに TSKaigi 2026 協賛企業一覧 TSKaigiへの初協賛を通して、ZOZOのことが少しでも来場者の皆さまに伝わっていれば嬉しいです。みなさま、ありがとうございました！ TSKaigi 2026をきっかけとしてZOZOのWebフロントエンドエンジニアに興味を持たれた方は、技術スタックなどがまとまったページをぜひご覧ください。 techblog.zozo.com ZOZOでは、一緒にサービスを作り上げてくれる方を募集中です。ご興味のある方は、以下のリンクからぜひご応募ください。 corp.zozo.com

こんにちは、モバファクエンジニアの id:knj-mf です。 今回は TypeScript の型レベルプログラミングでちょっと面白いものを作ったので紹介したいと思います。 何を作ったの？ TypeScript の型レベルプログラミングは、予想に反して様々なものが実装できてしまうことで有名だったりします。 type-challenges のように、「これは普通のプログラミングで実装するものでは？」と思ってしまうようなものまで実装できてしまいます。そこで、作ってみたものが下記になります。 早速、動作を紹介します。このような Brainf**k プログラムの文字列型が… このように、型計算上で解釈されてしまう！というものです。 ある程度の形になるものはできたので、この記事では、型レベルプログラミングと書き味の近い (個人差があります) Haskell 実装と照らしながら、どのように考えてこの「型」を実装していったのかを紹介します。 cwd-k2/bf-in-type のリポジトリ に実装があるので、気になる方は手元で動作や実装を見てみてください。 Brainf**k？ たった 8 つの命令からなる難読プログラミング言語です。言語の仕様としてかなり単純明快ではありますが、チューリング完全として知られています。(ちょっと企業の公式ブログには載せづらい表記を含むので、今回は ** という風に伏せさせていただきます…) 要素として、次の 4 つのものを持ちます。 要素 内容 プログラムテープ 実行するプログラム列 メモリテープ 値を記録するセルの列 プログラムポインタ 現在参照しているプログラム命令列上の位置 メモリポインタ 現在参照しているメモリテープの位置 8 つの命令は次のような単純なものです。 命令 内容 > メモリポインタをインクリメント（次のセルへ） < メモリポインタをデクリメント（前のセルへ） + 現在セルの値をインクリメント - 現在セルの値をデクリメント . 現在セルの値を ASCII 文字として出力 , 1 バイト読み込み、現在セルへ格納 [ 現在セルが 0 なら、対応する ] の直後へジャンプ ] 現在セルが 0 でなければ、対応する [ の直後へジャンプ ざっくり、プログラムテープ上に記載された 8 つの命令の列を順次実行しながらメモリテープの値を書き換えつつ、適宜 I/O していく形のプログラミング言語になります。 実際の Brainf**k プログラムそのものはまったく実用性がないのですが、この簡単な命令セットからなる言語処理系の実装には教育的価値があります。結構書いてみたことがあるというエンジニアの方も多いのではないでしょうか。 TypeScript の型レベルプログラミング ところで、TypeScript には (TypeScript に限りませんが) 型レベルプログラミングがあります。本当に単純な例だと、下記のようなものです。 type ExtendsObject < T > = T extends object ? true : false これが何をしているのかというと、型チェックの際に実施される型計算を実装しているということです。上記のような条件分岐などのロジックが型レベルで解決されてしまうということですね。 この型レベルプログラミングなのですが、表現力はさておき、チューリング完全な系になってしまっているとのもっぱらの評判です。 型から型を新たに計算できてしまうということは… 楽しいプログラミングの時間の始まりですね。 実装方針 長くなってしまうので、以降では Brainf**k を BF と記載することにします。 BF 処理系を型レベルに落とし込むにあたって、次の 4 つの要素に分けて考えます。 テープ構造体 ( Tape ) — メモリ・プログラムを共通して表現するデータ構造 現在位置を持ちつつ、前後に移動する能力を持つ 評価器 ( Runner ) — メモリテープとプログラムテープを束ねた実行状態 メモリを変化させつつプログラムポインタを移動するため、同時に扱う アクション ( Action ) — 1 ステップ実行の結果として外界に要求する効果 (なにもしない / 入力 / 出力 / 終了) 評価ループ ( Exec ) — アクションを解釈して評価器を回し、入力を消費しつつ出力を蓄積するメインループ 型レベルプログラミングでは副作用を素直に書けないため、入出力を「アクション型」としてデータに落としておき、外側のループでそれを解釈する形にしたのがポイントです。以降、この順で各要素の実装を見ていきます。 また、適宜参考実装として Haskell の実装も合わせて示しています。 TypeScript 実装は v5.4 以降で動作確認しています。 実装上の制約 制約として、実装レベルに効いてくるものもあります。数値での演算や数値⇔文字の変換が基本的にできない、というものです。不可能ではないですが、タプル (型レベル配列) の length を取るような実装になりがちなのでまわりくどくなります。 今回は ASCII 範囲でインクリメント・デクリメントを考えるだけなので、気合いで誤魔化すことができます。 NumToCharMap[65] のように参照すると 'A' という型に解決される、というマップを定義しました。 数値文字変換、インクリメント・デクリメントマップの実装 export type NumToCharMap = [ '\x00' , '\x01' , '\x02' , '\x03' , '\x04' , '\x05' , '\x06' , '\x07' , '\x08' , '\x09' , '\x0A' , '\x0B' , '\x0C' , '\x0D' , '\x0E' , '\x0F' , '\x10' , '\x11' , '\x12' , '\x13' , '\x14' , '\x15' , '\x16' , '\x17' , '\x18' , '\x19' , '\x1A' , '\x1B' , '\x1C' , '\x1D' , '\x1E' , '\x1F' , '\x20' , '\x21' , '\x22' , '\x23' , '\x24' , '\x25' , '\x26' , '\x27' , '\x28' , '\x29' , '\x2A' , '\x2B' , '\x2C' , '\x2D' , '\x2E' , '\x2F' , '\x30' , '\x31' , '\x32' , '\x33' , '\x34' , '\x35' , '\x36' , '\x37' , '\x38' , '\x39' , '\x3A' , '\x3B' , '\x3C' , '\x3D' , '\x3E' , '\x3F' , '\x40' , '\x41' , '\x42' , '\x43' , '\x44' , '\x45' , '\x46' , '\x47' , '\x48' , '\x49' , '\x4A' , '\x4B' , '\x4C' , '\x4D' , '\x4E' , '\x4F' , '\x50' , '\x51' , '\x52' , '\x53' , '\x54' , '\x55' , '\x56' , '\x57' , '\x58' , '\x59' , '\x5A' , '\x5B' , '\x5C' , '\x5D' , '\x5E' , '\x5F' , '\x60' , '\x61' , '\x62' , '\x63' , '\x64' , '\x65' , '\x66' , '\x67' , '\x68' , '\x69' , '\x6A' , '\x6B' , '\x6C' , '\x6D' , '\x6E' , '\x6F' , '\x70' , '\x71' , '\x72' , '\x73' , '\x74' , '\x75' , '\x76' , '\x77' , '\x78' , '\x79' , '\x7A' , '\x7B' , '\x7C' , '\x7D' , '\x7E' , '\x7F' , ] & { [ i: number ] : ' \x00 ' } ; export type CharToNumMap = { '\x00' : 0 x00 , '\x01' : 0 x01 , '\x02' : 0 x02 , '\x03' : 0 x03 , '\x04' : 0 x04 , '\x05' : 0 x05 , '\x06' : 0 x06 , '\x07' : 0 x07 , '\x08' : 0 x08 , '\x09' : 0 x09 , '\x0A' : 0 x0A , '\x0B' : 0 x0B , '\x0C' : 0 x0C , '\x0D' : 0 x0D , '\x0E' : 0 x0E , '\x0F' : 0 x0F , '\x10' : 0 x10 , '\x11' : 0 x11 , '\x12' : 0 x12 , '\x13' : 0 x13 , '\x14' : 0 x14 , '\x15' : 0 x15 , '\x16' : 0 x16 , '\x17' : 0 x17 , '\x18' : 0 x18 , '\x19' : 0 x19 , '\x1A' : 0 x1A , '\x1B' : 0 x1B , '\x1C' : 0 x1C , '\x1D' : 0 x1D , '\x1E' : 0 x1E , '\x1F' : 0 x1F , '\x20' : 0 x20 , '\x21' : 0 x21 , '\x22' : 0 x22 , '\x23' : 0 x23 , '\x24' : 0 x24 , '\x25' : 0 x25 , '\x26' : 0 x26 , '\x27' : 0 x27 , '\x28' : 0 x28 , '\x29' : 0 x29 , '\x2A' : 0 x2A , '\x2B' : 0 x2B , '\x2C' : 0 x2C , '\x2D' : 0 x2D , '\x2E' : 0 x2E , '\x2F' : 0 x2F , '\x30' : 0 x30 , '\x31' : 0 x31 , '\x32' : 0 x32 , '\x33' : 0 x33 , '\x34' : 0 x34 , '\x35' : 0 x35 , '\x36' : 0 x36 , '\x37' : 0 x37 , '\x38' : 0 x38 , '\x39' : 0 x39 , '\x3A' : 0 x3A , '\x3B' : 0 x3B , '\x3C' : 0 x3C , '\x3D' : 0 x3D , '\x3E' : 0 x3E , '\x3F' : 0 x3F , '\x40' : 0 x40 , '\x41' : 0 x41 , '\x42' : 0 x42 , '\x43' : 0 x43 , '\x44' : 0 x44 , '\x45' : 0 x45 , '\x46' : 0 x46 , '\x47' : 0 x47 , '\x48' : 0 x48 , '\x49' : 0 x49 , '\x4A' : 0 x4A , '\x4B' : 0 x4B , '\x4C' : 0 x4C , '\x4D' : 0 x4D , '\x4E' : 0 x4E , '\x4F' : 0 x4F , '\x50' : 0 x50 , '\x51' : 0 x51 , '\x52' : 0 x52 , '\x53' : 0 x53 , '\x54' : 0 x54 , '\x55' : 0 x55 , '\x56' : 0 x56 , '\x57' : 0 x57 , '\x58' : 0 x58 , '\x59' : 0 x59 , '\x5A' : 0 x5A , '\x5B' : 0 x5B , '\x5C' : 0 x5C , '\x5D' : 0 x5D , '\x5E' : 0 x5E , '\x5F' : 0 x5F , '\x60' : 0 x60 , '\x61' : 0 x61 , '\x62' : 0 x62 , '\x63' : 0 x63 , '\x64' : 0 x64 , '\x65' : 0 x65 , '\x66' : 0 x66 , '\x67' : 0 x67 , '\x68' : 0 x68 , '\x69' : 0 x69 , '\x6A' : 0 x6A , '\x6B' : 0 x6B , '\x6C' : 0 x6C , '\x6D' : 0 x6D , '\x6E' : 0 x6E , '\x6F' : 0 x6F , '\x70' : 0 x70 , '\x71' : 0 x71 , '\x72' : 0 x72 , '\x73' : 0 x73 , '\x74' : 0 x74 , '\x75' : 0 x75 , '\x76' : 0 x76 , '\x77' : 0 x77 , '\x78' : 0 x78 , '\x79' : 0 x79 , '\x7A' : 0 x7A , '\x7B' : 0 x7B , '\x7C' : 0 x7C , '\x7D' : 0 x7D , '\x7E' : 0 x7E , '\x7F' : 0 x7F , } & { [ k : string ]: 0 x00 ; } ; export type DecrementMap = [ 0 x7F , 0 x00 , 0 x01 , 0 x02 , 0 x03 , 0 x04 , 0 x05 , 0 x06 , 0 x07 , 0 x08 , 0 x09 , 0 x0A , 0 x0B , 0 x0C , 0 x0D , 0 x0E , 0 x0F , 0 x10 , 0 x11 , 0 x12 , 0 x13 , 0 x14 , 0 x15 , 0 x16 , 0 x17 , 0 x18 , 0 x19 , 0 x1A , 0 x1B , 0 x1C , 0 x1D , 0 x1E , 0 x1F , 0 x20 , 0 x21 , 0 x22 , 0 x23 , 0 x24 , 0 x25 , 0 x26 , 0 x27 , 0 x28 , 0 x29 , 0 x2A , 0 x2B , 0 x2C , 0 x2D , 0 x2E , 0 x2F , 0 x30 , 0 x31 , 0 x32 , 0 x33 , 0 x34 , 0 x35 , 0 x36 , 0 x37 , 0 x38 , 0 x39 , 0 x3A , 0 x3B , 0 x3C , 0 x3D , 0 x3E , 0 x3F , 0 x40 , 0 x41 , 0 x42 , 0 x43 , 0 x44 , 0 x45 , 0 x46 , 0 x47 , 0 x48 , 0 x49 , 0 x4A , 0 x4B , 0 x4C , 0 x4D , 0 x4E , 0 x4F , 0 x50 , 0 x51 , 0 x52 , 0 x53 , 0 x54 , 0 x55 , 0 x56 , 0 x57 , 0 x58 , 0 x59 , 0 x5A , 0 x5B , 0 x5C , 0 x5D , 0 x5E , 0 x5F , 0 x60 , 0 x61 , 0 x62 , 0 x63 , 0 x64 , 0 x65 , 0 x66 , 0 x67 , 0 x68 , 0 x69 , 0 x6A , 0 x6B , 0 x6C , 0 x6D , 0 x6E , 0 x6F , 0 x70 , 0 x71 , 0 x72 , 0 x73 , 0 x74 , 0 x75 , 0 x76 , 0 x77 , 0 x78 , 0 x79 , 0 x7A , 0 x7B , 0 x7C , 0 x7D , 0 x7E , ] & { [ i: number ] : 0x7F ; } ; export type IncrementMap = [ 0 x01 , 0 x02 , 0 x03 , 0 x04 , 0 x05 , 0 x06 , 0 x07 , 0 x08 , 0 x09 , 0 x0A , 0 x0B , 0 x0C , 0 x0D , 0 x0E , 0 x0F , 0 x10 , 0 x11 , 0 x12 , 0 x13 , 0 x14 , 0 x15 , 0 x16 , 0 x17 , 0 x18 , 0 x19 , 0 x1A , 0 x1B , 0 x1C , 0 x1D , 0 x1E , 0 x1F , 0 x20 , 0 x21 , 0 x22 , 0 x23 , 0 x24 , 0 x25 , 0 x26 , 0 x27 , 0 x28 , 0 x29 , 0 x2A , 0 x2B , 0 x2C , 0 x2D , 0 x2E , 0 x2F , 0 x30 , 0 x31 , 0 x32 , 0 x33 , 0 x34 , 0 x35 , 0 x36 , 0 x37 , 0 x38 , 0 x39 , 0 x3A , 0 x3B , 0 x3C , 0 x3D , 0 x3E , 0 x3F , 0 x40 , 0 x41 , 0 x42 , 0 x43 , 0 x44 , 0 x45 , 0 x46 , 0 x47 , 0 x48 , 0 x49 , 0 x4A , 0 x4B , 0 x4C , 0 x4D , 0 x4E , 0 x4F , 0 x50 , 0 x51 , 0 x52 , 0 x53 , 0 x54 , 0 x55 , 0 x56 , 0 x57 , 0 x58 , 0 x59 , 0 x5A , 0 x5B , 0 x5C , 0 x5D , 0 x5E , 0 x5F , 0 x60 , 0 x61 , 0 x62 , 0 x63 , 0 x64 , 0 x65 , 0 x66 , 0 x67 , 0 x68 , 0 x69 , 0 x6A , 0 x6B , 0 x6C , 0 x6D , 0 x6E , 0 x6F , 0 x70 , 0 x71 , 0 x72 , 0 x73 , 0 x74 , 0 x75 , 0 x76 , 0 x77 , 0 x78 , 0 x79 , 0 x7A , 0 x7B , 0 x7C , 0 x7D , 0 x7E , 0 x7F , 0 x00 , ] & { [ i: number ] : 0x00 ; } ; テープ構造体 BF では、メモリを用意してポインタ操作・ポインタを介した操作が前提になっています。 もちろん型レベルプログラミングで副作用は記述しにくいため、ポインタ前提となっている部分を再考し、同じ表現力の別の形に置き換える必要があります。 メモリ、プログラムを同じテープ構造で捉えます。今着目している値、その左右に列が続いている様子を考えたのが下記のような構造になります。 テープ構造体の実装 このような構造体は、Haskell での data 宣言と同じような形で、TypeScript の型ではオブジェクト型による宣言ができます。 data Tape a = Tape { prevs :: [a] , curr :: a , nexts :: [a] } extends unknown[] によって単なる配列型ではなく、各要素が独立した 型レベル配列としてのタプル を利用できます。 export type Tape < Hs extends unknown [], C , Ts extends unknown []> = { h : Hs c : C t : Ts } ここでいくつかの基本的な操作も定義してしまいましょう。 現在の値に対する操作 インクリメント・デクリメント 読み出し、書き込み テープ上の移動 着目するヘッドを左右に移動する操作 対応する [ , ] へのジャンプは繰り返しによって実現する 基本操作の実装 Tape a から新しい Tape a を作る ( Tape a -> Tape a ) という形の実装となります。 -- | 次の要素に移動 next :: Tape a -> Tape a next (Tape prevs curr (n : nexts)) = Tape (curr : prevs) n nexts -- | 前の要素に移動 prev :: Tape a -> Tape a prev (Tape (p : prevs) curr nexts) = Tape prevs p (curr : nexts) -- | 現在の要素をインクリメント incr :: Enum a => Tape a -> Tape a incr (Tape prevs curr nexts) = Tape prevs (succ curr) nexts -- | 現在の要素をデクリメント decr :: Enum a => Tape a -> Tape a decr (Tape prevs curr nexts) = Tape prevs (pred curr) nexts -- | 現在の要素を取得 get :: Tape a -> a get (Tape _ curr _) = curr -- | 現在の要素を設定 put :: a -> Tape a -> Tape a put a (Tape prevs _ nexts) = Tape prevs a nexts TypeScript の型でも同様に、 Tape を受け取って新しい Tape を作成するという方針で実装できます。 [infer H, ...infer Hs] のパターンマッチングにより、型レベル配列の要素 (head, rest) を扱うことができてしまいます。 export type Prev < M > = M extends Tape < [infer H , ... infer Hs] , infer C , infer Ts > ? Tape< Hs , H , [C , ... Ts] > : never export type Next < M > = M extends Tape < infer Hs , infer C , [infer T , ... infer Ts] > ? Tape< [C , ... Hs] , T , Ts > : never export type Incr < M > = M extends Tape < infer Hs , infer C extends number , infer Ts > ? Tape< Hs , IncrementMap [C], Ts > : never export type Decr < M > = M extends Tape < infer Hs , infer C extends number , infer Ts > ? Tape< Hs , DecrementMap [C], Ts > : never export type PutC < M , C > = M extends Tape < infer Hs , unknown , infer Ts > ? Tape < Hs , C , Ts > : never プログラム実行 基本的な構造、操作は定義してしまったので、次はインタプリタとして重要な実行について考えます。 評価器としての実行系内部 (メモリ・プログラムポインタ) と外界とのやりとりを含む効果の管理の部分を、次のような形で切り分けます。 型レベルプログラミングでは入出力をそのまま扱うことはできないので、入力待ちや出力があるということは特別な状態として表現することにします。 評価器の内部状態 こちらは至ってシンプルです。 状態はメモリ、プログラムのテープ (現在位置を保持する) から成る これを評価に通すことによって、次の実行に関する状態が出てくる data Machine = Machine { memory :: DT.Tape Int , program :: DT.Tape Char } type Runner < M , P > = { mem : M prg : P } 外部とのやりとりを含むアクション 今のメモリ・プログラムを含む、先程の構造を評価して得られるアクションです。 -- | 何もしない、入力要求、出力要求、終了の 4 つのアクションを持つ data WithAction a = ActionN { hold :: a } -- ^ 外部には何もしない | ActionI { hold :: a } -- ^ 入力要求 | ActionO { hold :: a, out :: Int } -- ^ 出力要求 | ActionE -- ^ 終了 これを型レベルプログラミングで再現すると、ADT よりは個別の型として定義してあげて、後で extends などの条件分岐してあげる方が素直になります。 type ActionN < R > = { action : "N" ; runner : R } type ActionI < R > = { action : "I" ; runner : R } type ActionO < R , O > = { action : "O" ; runner : R ; output : O } type ActionE = { action : "E" } 8 つの命令に対する操作の整理 評価器の状態とアクションを型として定義できたので、次はプログラムの示す命令を処理していく実装も考えていきます。 これは最初に確認した BF の 8 つの命令に対して、次の評価器の状態と計算の効果を含む全体を返す形で定義していけば良いです。 インクリメント デクリメント 次を参照 (ポインタインクリメント) 前を参照 (ポインタデクリメント) while (ジャンプ) while end (ジャンプバック) getchar putchar 命令→次の状態・アクション さて、図で整理できたので、実装にそのまま落としていきます。 現在の命令ポインタが指す命令に応じて、次の Action と状態を返します。 -- | 次のステップを実行し、状態とアクションを返す step :: Machine -> WithAction Machine step machine = case pc of '+' -> ActionN $ machine { memory = DT.incr (memory machine), program = DT.next (program machine) } '-' -> ActionN $ machine { memory = DT.decr (memory machine), program = DT.next (program machine) } '>' -> ActionN $ machine { memory = DT.next (memory machine), program = DT.next (program machine) } '<' -> ActionN $ machine { memory = DT.prev (memory machine), program = DT.next (program machine) } '[' -> ActionN $ machine { program = if mc == 0 then skip (program machine) else DT.next (program machine) } ']' -> ActionN $ machine { program = if mc /= 0 then back (program machine) else DT.next (program machine) } ',' -> ActionI { hold = machine { program = DT.next (program machine) } } '.' -> ActionO { hold = machine { program = DT.next (program machine) }, out = DT.get (memory machine) } _ -> ActionE where (pc, mc) = (,) <$> DT.get . program <*> DT.get . memory $ machine TypeScript で書いても、ほとんど同じ対応があります。 type Step < R > = R extends Runner < infer M extends TapeMm , infer P extends TapePg > ? P[ 'c' ] extends '+' ? ActionN< Runner < Incr < M >, Next < P >>> : P[ 'c' ] extends '-' ? ActionN< Runner < Decr < M >, Next < P >>> : P[ 'c' ] extends '>' ? ActionN< Runner < Next < M >, Next < P >>> : P[ 'c' ] extends '<' ? ActionN< Runner < Prev < M >, Next < P >>> : P[ 'c' ] extends '[' ? ActionN< Runner < M , M [ 'c' ] extends 0 ? Skip < P > : Next < P >>> : P[ 'c' ] extends ']' ? ActionN< Runner < M , M [ 'c' ] extends 0 ? Next < P > : Back < P >>> : P[ 'c' ] extends ',' ? ActionI< Runner < M , Next < P >>> : P[ 'c' ] extends '.' ? ActionO< Runner < M , Next < P >>, M [ 'c' ]> : ActionE : never; 状態・アクション→継続 次は状態、アクションを受けて、次のステップに継続していくループを実装していきます。 上記の step を実行し、その Action に応じた操作を実行していきます。 -- | 入力を消費・出力を収集しながら step を繰り返す loop :: (Machine -> WithAction Machine) -> (String, Machine) -> String loop step (input, machine) = go (step machine) where -- アクションに対応した動作を実行し、再帰に進む go (ActionN machine') = loop step (input, machine') -- そのまま次へ go (ActionI machine') = loop step (iTail, machine'') where -- 入力を消費してメモリに書き込み、次に進む (iHead : iTail) = input machine'' = machine' { memory = DT.put (fromEnum iHead) (memory machine') } go (ActionO machine' out) = toEnum out : loop step (input, machine') -- 出力を収集し、次に進む go ActionE = [] -- 終端 TypeScript の型の方では、今回は文字列の累積を保持する形で実装しています。ちょっと命名が異なってしまっていますが、やっていることは同じです。 type Exec < R , I extends string , O extends string = '' > = Step < R > extends infer WithAction ? WithAction extends ActionN< infer Q > ? Exec< Q , I , O > : WithAction extends ActionI< infer Q > ? I extends ` ${ infer F }${ infer S } ` ? Exec< Read < Q , CharToNumMap [F]>, S , O > : Exec< Read < Q , 0>, I , O > : WithAction extends ActionO< infer Q , infer N extends number > ? Exec< Q , I , ` ${ O }${ NumToCharMap [N] } ` > : WithAction extends ActionE ? O : never : never; まとめ TypeScript で Brainf**k 処理系の型レベルプログラムの実装について見ていきました。 補足として、TypeScript の型レベルプログラミング実行系には次のような制約があります。 型の再帰評価回数、つまり実行できるステップ数が制限されている Tape 構造体の保持する要素列の長さに制限がある (どちらも大体 1,000 程度のイメージ) 一方、このような制限がある中でも、冒頭に示した例のように簡単な Hello World の例までは実装できてしまいます。 みなさんもぜひ自分の型レベルプログラミングに挑戦してみてください。 私が今回示した実装も最善ではないと思います。「もっと良いものを書いてみよう」など、楽しんでみてください。 付録 Haskell のコード全文を掲載しておきます。 cwd-k2/bf-in-type のリポジトリ と比較する、または手元でテスト実行するなどしてください。 ディレクトリ構成 . ├── Data │   └── Tape.hs ├── Interpreter.hs └── Main.hs Data/Tape.hs module Data.Tape ( Tape( .. ), zeros, fromList, next, prev, incr, decr, get, put, ) where -- | テープ様構造体 -- * 前後に無限に要素があり、現在要素 (針の先にあるもの) を中心に配置している -- -- > <-prev- ... 4 5 6 <<7>> 8 9 10 ... -next-> data Tape a = Tape { prevs :: [a] , curr :: a , nexts :: [a] } deriving Show -- | ゼロ初期化された無限長のテープ zeros :: Enum a => Tape a zeros = Tape (repeat $ toEnum 0 ) (toEnum 0 ) (repeat $ toEnum 0 ) -- | リストからテープを作成 fromList :: [a] -> Tape a fromList (x : xs) = Tape [] x xs fromList [] = undefined -- 今回は特に考えずに未定義とする -- | 次の要素に移動 next :: Tape a -> Tape a next (Tape prevs curr (n : nexts)) = Tape (curr : prevs) n nexts -- | 前の要素に移動 prev :: Tape a -> Tape a prev (Tape (p : prevs) curr nexts) = Tape prevs p (curr : nexts) -- | 現在の要素をインクリメント incr :: Enum a => Tape a -> Tape a incr (Tape prevs curr nexts) = Tape prevs (succ curr) nexts -- | 現在の要素をデクリメント decr :: Enum a => Tape a -> Tape a decr (Tape prevs curr nexts) = Tape prevs (pred curr) nexts -- | 現在の要素を取得 get :: Tape a -> a get (Tape _ curr _) = curr -- | 現在の要素を設定 put :: a -> Tape a -> Tape a put a (Tape prevs _ nexts) = Tape prevs a nexts Interpreter.hs module Interpreter ( bf ) where import qualified Data.Tape as DT import Data.List (unfoldr) -- | メモリとプログラムを持つ data Machine = Machine { memory :: DT.Tape Int , program :: DT.Tape Char } deriving Show -- | 何もしない、入力要求、出力要求、終了の 4 つのアクションを持つ data WithAction a = ActionN { hold :: a } -- ^ 外部には何もしない | ActionI { hold :: a } -- ^ 入力要求 | ActionO { hold :: a, out :: Int } -- ^ 出力要求 | ActionE -- ^ 終了 deriving Show -- | 対応する @']'@ までプログラムをスキップする skip :: DT.Tape Char -> DT.Tape Char skip = skipInner 0 where skipInner n program = let program' = DT.next program in case DT.get program' of '[' -> skipInner (n + 1 ) program' ']' -> if n == 0 then program' else skipInner (n - 1 ) program' _ -> skipInner n program' -- | 対応する @'['@ までプログラムを戻す back :: DT.Tape Char -> DT.Tape Char back = backInner 0 where backInner n program = let program' = DT.prev program in case DT.get program' of ']' -> backInner (n + 1 ) program' '[' -> if n == 0 then program' else backInner (n - 1 ) program' _ -> backInner n program' -- | 次のステップを実行し、状態とアクションを返す step :: Machine -> WithAction Machine step machine = case pc of '+' -> ActionN $ machine { memory = DT.incr (memory machine), program = DT.next (program machine) } '-' -> ActionN $ machine { memory = DT.decr (memory machine), program = DT.next (program machine) } '>' -> ActionN $ machine { memory = DT.next (memory machine), program = DT.next (program machine) } '<' -> ActionN $ machine { memory = DT.prev (memory machine), program = DT.next (program machine) } '[' -> ActionN $ machine { program = if mc == 0 then skip (program machine) else DT.next (program machine) } ']' -> ActionN $ machine { program = if mc /= 0 then back (program machine) else DT.next (program machine) } ',' -> ActionI { hold = machine { program = DT.next (program machine) } } '.' -> ActionO { hold = machine { program = DT.next (program machine) }, out = DT.get (memory machine) } _ -> ActionE where (pc, mc) = (,) <$> DT.get . program <*> DT.get . memory $ machine -- | 入力を消費・出力を収集しながら step を繰り返す loop :: (Machine -> WithAction Machine) -> (String, Machine) -> String loop step (input, machine) = go (step machine) where -- アクションに対応した動作を実行し、再帰に進む go (ActionN machine') = loop step (input, machine') -- そのまま次へ go (ActionI machine') = loop step (iTail, machine'') where -- 入力を消費してメモリに書き込み、次に進む (iHead : iTail) = input machine'' = machine' { memory = DT.put (fromEnum iHead) (memory machine') } go (ActionO machine' out) = toEnum out : loop step (input, machine') -- 出力を収集し、次に進む go ActionE = [] -- 終端 -- | Bf プログラムから、入力を受け取って出力を返す関数を作る bf :: String -> [Char] -> String bf program input = loop step (input', machine) where input' = input ++ repeat ' \0 ' machine = Machine { memory = DT.zeros , program = DT.next $ DT.fromList ( "#" ++ program ++ "#" ) } Main.hs module Main where import Interpreter -- | ハローワールドする Bf プログラム helloWorld :: String helloWorld = "++++++++++[>+++++++>++++++++++>+++++++++++>+++>+++++++++>+<<<<<<-]>++.>+.>--..+++.>++.>---.<<.+++.------.<-.>>+.>>." -- | エコーする Bf プログラム echo :: String echo = "+[,.]" main :: IO () main = do let getOutputBf = bf helloWorld putStr $ getOutputBf "こんにちは \n "