スポンサーLobeHubLobeHub詳しく見る
dshfind
論文精読入門

Cordis 論文精読:時空コンポーザビリティのプログラミングパラダイム

『時空コンポーザビリティのためのプログラミングパラダイム』をゼロから読み解きます。型理論の背景知識は不要。コードの直感で可逆エフェクトとリアクティブコエフェクトを理解できます。

13 レッスン約 5.2 時間進捗 0/13
学習を続ける:レッスン 1
要旨と序論:動的コンポジションと2つの次元
このレッスンを始める

コースカタログ

1
要旨と序論:動的コンポジションと2つの次元次のレッスン
時間コンポーザビリティと空間コンポーザビリティとは何か
2
動機づけの例:VSCode プラグインと AI エージェント
なぜ今のソフトウェアは実行時にアンロードできないのか
3
貢献の振り返りと型判断 Γ ⊢ t : T
エフェクト注釈:型は戻り値だけでなく副作用も記録する
4
モナド:副作用を箱に入れる
Promise はモナド:η で値を包み、flatMap で平坦化する
5
コエフェクト:計算が環境に求めるもの
エフェクトは「何を変えたか」を問い、コエフェクトは「何が必要か」を問う
6
可逆エフェクト:取り付けられ、取り外せる
すべてのコンテキスト変換に明示的な逆変換が付属する
7
エフェクトの合成:逆変換は自動で合成される
⋄ 演算:合成されたエフェクトの逆は合成から自然に得られる
8
リアクティブコエフェクト:依存が揃えば自動で起動
充足性とアクティブ化 / 非アクティブ化 / 中立遷移の分類
9
コンポーネントライフサイクル:冪等・反復・エポック・非同期
慣性状態マシン:遷移は一度始まると完了まで実行される
10
コンテキストパラダイム:統一されたコンテキスト型
エフェクトコンテキストとコエフェクトコンテキストを1つの実体に統合
11
Cordis コアライブラリ:エフェクト追跡とコエフェクト解決
ctx.effect、ctx.set、ファイバーと慣性状態マシン
12
コンポーネントローダーと Koishi のケーススタディ
宣言的設定、ホットモジュールリプレースメント、4000+ のプラグインエコシステム
13
考察、関連研究、まとめ
サービス多重化、アクセス制御、バージョン管理

用語集 · 論文付録 A

この用語集は、論文が新たに提案した概念、または特別な意味を与えた概念のみを収録しています。一般的な概念は繰り返し掲載しません。

時間コンポーザビリティ
temporal composability
コンポーネントが削除される際に、そのコンポーネントが共有環境に加えた変更を完全かつ安全に取り消す能力。
空間コンポーザビリティ
spatial composability
コンポーネントが互いの依存関係を、構造化された検証可能な方法で宣言・発見・解決する能力。
可逆エフェクト
revertible effect
すべてのコンテキスト変換が逆関数を明示的に持ち、ランタイムが逆関数を記録・合成するため、アンインストールすれば状態が復元されます。
リアクティブコエフェクト
reactive coeffect
コンポーネントが依存関係の仕様を宣言し、依存の充足状態が変化すると、アクティブ化と非アクティブ化が自動的に駆動されます。
エフェクトコンテキスト
effect context
∂Γ ≔ Γ × 𝔉Γ:現在の状態と累積された復元変換からなるランタイムコンテキスト。
コエフェクトコンテキスト
coeffect context
Σ ≔ (k ∶ K) ⇀ 𝒱ₖ:依存キーから型付き値への有限な依存部分関数。
エポック
epoch
解決済みの依存値のタプル。目標状態の具体的な依存構成に番号を付けるために使われます。
慣性状態
inertial state
非同期ライフサイクルにおける Reload/Unload 遷移。一度開始すると完了まで実行されます。