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

これは株式会社LabBase テックカレンダー Advent Calendar 2025 12日目の記事です。 概要 学生時代から、論文などの議論の精読に対して、「絶対誰かがもう論理的な整合性を確かめたことあるんだろうな〜」と思い、その度に論理的な整合性の再確認に対してめんどくささを感じてきました。 本稿では形式意味論と定理証明支援系を利用して、あらゆる議論を形式化することで、これを打破することを目論みます。 もし自然言語が「コンパイル」できたら？ プログラミング言語では、コードを書くと同時にコンパイラや静的解析ツールが働き、文法ミスや型の不整合、論理的な破綻を検出してくれます。