Donut とは
Note: Donut は開発中のプロトタイプです。仕様や動作は予告なく変更される可能性があり、このドキュメントも不完全・不正確な部分を含む場合があります。ドキュメントの大部分は Claude Code によって生成されています。
Donut は 高次元セル を合成してプログラムを組み立てる言語です。
通常のプログラミング言語が「値」と「関数」を扱うのに対し、Donut では セル を宣言して繋ぎ合わせます。セルには次元があり、次元ごとに異なる役割を持ちます:
| 次元 | 意味 | 例 |
|---|---|---|
| 0-cell | 環境・コンテキスト | C: * |
| 1-cell | 型 | Int: C → C |
| 2-cell | 演算・プログラム | add: Int Int → Int |
| 3-cell | 等式・書き換え | α: m x; m → x m; m |
次元は上に開いており、4-cell、5-cell… と続きます。
基本的な考え方
- 宣言: プリミティブなセルを置く。型は source と target で決まる
- 合成: セルをスペースや
;で繋ぐ。境界が一致すれば合成できる - 型検査: 合成の整合性を自動で検証する
何ができる?
抽象構造の記述: モノイドなどの代数的構造を宣言し、結合律(pentagon identity)のような高次の coherence 条件を表現できます。
具体的な計算: import "sys" でプリミティブ型(f32, bool 等)を読み込み、2-cell の合成で Mandelbrot 集合のようなプログラムを書けます。評価結果はリアルタイムに確認でき、条件を満たせば GLSL にコンパイルしてシェーダー描画もできます。
Functor: ~> で2つの構造間のマッピングを定義します。プリミティブの対応だけ書けば、合成セルは自動的に変換されます。
最初の例
u: *
x: u → u
m: x x → x
uは 0-cell(環境)xはu上の 1-cell(型)mはx xからxへの 2-cell(二項演算)
m の型 x x → x は、1-cell x を2つ並べたものを受け取り x を返す 2-cell です。これだけで「モノイド的な構造」の骨格が記述できています。
さらに結合律を表す 3-cell を宣言すると:
α: m x; m → x m; m
m(m(a,b), c) = m(a, m(b,c)) という結合律の「証拠」が 3-cell として現れます。
基本構文
Donut のプログラムは 宣言 の列です。各宣言は名前、型、値を持ちます。
name: type
name = value
name: type = value
name: type := value
コメントは // で始まる行コメントです。
// これはコメントです
u: *
インデントはスペースのみ(タブ不可)。
同時宣言
スペースで区切って複数の名前を同時に宣言できます。すべて同じ型になります。
C D: * // C: * と D: * を同時に宣言
a b: C → D // a: C → D と b: C → D を同時に宣言
宣言と型
型宣言(Decl)
名前と型を宣言します。値は自動的に生成されます。
u: *
x: u → u
* は 0-cell の型です。u → u は u から u への 1-cell の型です。
値の定義(Alias)
名前に値を束縛します。型は値から推論されます。
f = x x
明示的な型注釈も可能です:
f: u → u = x x
型エイリアスとしての利用
型を表す値を alias に束縛すると、型として使えます。
T = x x → x
m: T // m: x x → x と同じ
パラメトリックな型エイリアスも可能です:
Endo[X: *] = X → X
f: Endo[u] // f: u → u と同じ
エイリアスの連鎖も展開されます: T = x x → x → S = T → m: S は m: x x → x と解釈されます。
型の階層
| 型 | 意味 | 例 |
|---|---|---|
* | 0-cell | u: * |
A → B | 1-cell 以上(射) | x: u → u |
A ~ B | 等価性 | e: x ~ y |
A ~> B | functor | F: src.C ~> tgt.D |
meta | メタ値(nat, rat, color 等) | n: nat |
Arrow の次元
Arrow の次元は source/target から自動的に決まります:
u: * // 0-cell
x: u → u // 1-cell (0-cell → 0-cell)
μ: x x → x // 2-cell (1-cell → 1-cell)
α: μ x; μ → x μ; μ // 3-cell
合成
セルを繋ぎ合わせて高次のセルを構築します。
0次合成
スペースで区切ると 0次合成 になります。左の target と右の source が一致する必要があります。
u: *
x: u → u
y: u → u
xy = x y // u → u
x の target(u)と y の source(u)が一致するため合成でき、結果は u → u の 1-cell になります。
1次合成
; で区切ると 1次合成 になります。1つ上の次元で、左の target と右の source が一致する必要があります。
u: *
x: u → u
μ: x x → x
xm = x x; μ // x x → x
n次合成
; を n 個並べると n次合成 になります。;; は 2次、;;; は 3次です。(n+1) 次元以上のセルで使います。
α: μ x; μ → x μ; μ
result =
α x; μ ;;
x μ x; α
;N(例: ;3)と書くことで任意の次数を数値で指定することもできます。
優先順位
高次の合成ほど結合が弱くなります:
- スペース(0次)— 最も強い
;(1次);;(2次);;;(3次)— …
a b; c d ;; e f; g は ((a b); (c d)) ;; ((e f); g) と解釈されます。
括弧 () で優先順位を制御できます。
モジュール
{ } でモジュールを定義できます。モジュール内の宣言はドット記法でアクセスします。
基本
cat = {
u: *
x: u → u
m: x x → x
}
// モジュールのメンバーにアクセス
f: cat.u → cat.u
ネスト
モジュールはネストできます。
a = {
b = {
u: *
x: u → u
}
y: b.u → b.u
}
// a.b.x でアクセス
f: a.b.x a.b.x → a.b.x
with 節
with { } で追加の宣言ができます。with 節の中では元の宣言のメンバーが直接使えます。
モジュールに使う場合:
cat = {
u: *
x: u → u
} with {
m: x x → x
}
// cat.m も定義される
宣言に使う場合:
C: *
x: C → C with {
m: x x → x
}
// x.m でアクセスできる
where 節
where { } でローカルな補助定義を書けます。where 節はモジュールだけでなく、一般の定義にも使えます。where 節の中の宣言は外部からはアクセスできません。
r[C: *, x: C → C, f: x → x]: x → x = g where {
g = f; f
}
モジュールと組み合わせることもできます:
cat = {
u: *
x: u → u
m: x x → x
} where {
helper = x x; m
}
where 節はネストできます:
r[C: *, x: C → C, f: x → x]: x → x = k where {
k = g; g
} where {
g = f; f
}
内側の where 節が先に評価されます。上の例では g が先に定義され、それを使って k が定義されます。
+= によるメンバー追加
既存のモジュールや宣言にメンバーを追加できます。
f32: C → C
f32 += {
lit[n: rat]: C → f32
add: f32 f32 → f32
neg: f32 → f32
}
// f32.lit[1], f32.add 等が使える
+= の右辺は { } モジュールです。追加されたメンバーは元の名前のドット記法でアクセスできます。これは sys ライブラリの内部で、型に演算を追加するために使われています。
パラメータ
宣言にパラメータを付けることで、構造を抽象化できます。
基本
パラメータは名前の直後に [...] で書きます。
cat[C: *] = {
x: C → C
m: x x → x
assoc: m x; m → x m; m
}
インスタンス化
パラメータを渡してインスタンスを作ります。
u: *
c = cat[u]
// c.x, c.m, c.assoc が使える
異なるパラメータで作ったインスタンスは異なるセルを持ちます: cat[u].x と cat[v].x は別のセルです。
複数パラメータ
Hom[X: *, Y: *] = X → Y
高次のパラメータ
0-cell だけでなく、1-cell や 2-cell もパラメータにできます。
rep2[C: *, x: C → C, f: x → x] = f; f
rep2 は 0-cell C、1-cell x、2-cell f: x → x を受け取り、f を2回合成した f; f を返します。
等価性 (Equality)
~ は2つのセルの間の 等価性 を表す型です。
基本
u: *
x: u → u
y: u → u
e: x ~ y
e は x と y が等しいことを示す 2-cell です。→ と同じく arrow 型ですが、方向を持たない(対称的な)関係を表現します。
→ との違い
| 型 | 意味 | 方向 |
|---|---|---|
x → y | x から y への射 | あり |
x ~ y | x と y の等価性 | なし |
→ は一方向の射を表しますが、~ は双方向の等価関係を表します。
定義 (:=) との関連
定義 (:=) を使うと、等価性が自動的に生成されます。
x: * := y
これは x: * を宣言し、x.def: x ~ y を自動生成します。x と y は異なるセルとして存在しますが、評価上は等しいことを ~ で表現しています。
定義
:= を使うと、宣言と定義を同時に行えます。
基本
a: *
x: * := a
これは以下を行います:
x: *を新しいセルとして宣言するx.def: x ~ aを自動生成する(xとaの等価性)- ランタイムで
xを評価する際、aとして計算する
型は右辺から推論することもできます:
import "sys"
add := f32.add
用途
定義は「新しい名前を付けつつ、計算は既存のセルに委譲する」パターンで使います。図式上では独立したセルとして表示されますが、評価時には右辺として計算されます。
次元の自動リフト
低次元のセルが高次元の位置で使われた場合、自動的に identity cell としてリフト(昇格)されます。
例
u: *
h: u → u = u
u は 0-cell ですが、u → u(1-cell の型)の位置で使われています。この場合 u は u 上の identity 1-cell(恒等射)として解釈されます。
合成での自動リフト
合成の中で次元の異なるセルが混在する場合、低い方が自動的にリフトされます。
u: *
x: u → u
μ: x x → x
// μ は 2-cell。x は 1-cell だが、2-cell の位置で使われると id(x) にリフトされる
α: μ x; μ → x μ; μ
μ x の x は 2-cell の文脈で使われているので、自動的に id(x) (identity 2-cell) にリフトされます。
仕組み
k-cell が n-cell(n > k)の位置で使われた場合、identity cell で包んで次元を合わせます。リフトは必要な回数だけ自動的に適用されます。
- 0-cell
Aを 1-cell の位置で →A上の identity 1-cell - 1-cell
xを 2-cell の位置で →id(x)(identity 2-cell) - 1-cell
xを 3-cell の位置で →id(id(x))(2回リフト)
デコレータ
デコレータは宣言の表示スタイルを制御します。宣言の前に [...] で記述します。
使用するには import "ui" が必要です。
色の指定
import "ui"
// HSV で指定
[style.color[hsv[0.6, 1, 1]]]
x: u → u
// RGB で指定
[style.color[rgb[255, 0, 128]]]
m: x x → x
// グレースケール
[style.color[gray[80]]]
u: *
// 色相のみ指定(彩度・明度は自動)
[style.color[hue[0.33]]]
y: u → u
自動カラー
デコレータを指定しない場合、自動的に色が割り当てられます。色はセルの次元と宣言順に基づいて決まります。
Lighten / Darken
自動色をベースに明るさを調整できます。
[style.lighten[0.3]]
a: x → x
[style.darken[0.2]]
b: x → x
import と use
組み込みライブラリを読み込むための2つの方法があります。
import
import はライブラリの中身をスコープに読み込みます。
import "sys"
// f32, f32.add 等が直接使える
x = f32.lit[1]
名前を付けて import すると、モジュールとしてスコープに入ります:
s = import "sys"
// s.f32, s.f32.add 等でアクセス
x = s.f32.lit[1]
use
use も同様にライブラリの中身をスコープに展開します。
use "base"
// nat, rat 等が直接使える
n: nat = 42
import と use の違い
import と use はどちらも無名で使うとライブラリの中身をスコープに展開します。違いは origin の扱いです。import で読み込まれた宣言はライブラリ由来としてマークされ、donut-app のセル一覧には表示されません。use で読み込まれた宣言にはそのようなマークが付きません。
組み込みライブラリ一覧
| ライブラリ | 内容 |
|---|---|
"sys" | プリミティブ型と演算(f32, u32, bool, val.dup 等) |
"base" | メタ型の定義(nat, rat, color, decorator) |
"ui" | デコレータ関連(rgb, hsv, hue, gray, style 等) |
"ui" は内部で "base" を use しているため、import "ui" だけで nat や rat も使えます。
Functor
Functor は2つの構造間のマッピングを定義します。プリミティブの対応だけ指定すれば、合成セルは自動的に変換されます。
宣言
~> で functor の型を宣言し、各プリミティブの対応を F(src) = tgt の形で記述します。
nat = {
C: *
Nat: C → C
zero: C → Nat
succ: Nat → Nat
add: Nat Nat → Nat
}
u8 = {
D: *
U8: D → D
zero: D → U8
succ: U8 → U8
add: U8 U8 → U8
}
compile: nat.C ~> u8.D
compile(nat.Nat) = u8.U8
compile(nat.zero) = u8.zero
compile(nat.succ) = u8.succ
compile(nat.add) = u8.add
自動変換
functor を定義すると、プリミティブセルの合成で作られたセルにも自動的に適用できます。
// nat のプリミティブだけで構成されたセル
two = nat.zero; nat.succ; nat.succ
// compile(two) は自動的に u8.zero; u8.succ; u8.succ になる
compiled_two = compile(two)
functor はソース構造のプリミティブの合成を再帰的に辿り、各プリミティブを対応するターゲットに置き換えます。ソース構造に属さないプリミティブが含まれている場合はエラーになります。
functoriality チェック
functor のマッピングは整合性がチェックされます。各マッピング F(X) = Y に対して、X の source/target を functor で変換した結果が Y の source/target と一致するか検証されます。一致しない場合はエラーになります。
制約の自動生成
パラメータのセルに functor を適用すると、マッピングが未定義なため即座には解決できません。この場合 制約 が自動生成されます。
src = {
C: *
X: C → C
}
tgt = {
D: *
Y: D → D
}
F: src.C ~> tgt.D
F(src.X) = tgt.Y
h[m: src.C → src.X] = F(m)
F(m) の m はパラメータであり F のマッピングに含まれないので、Donut は F(m) の結果を表すフレッシュなセルを生成します。h の型は制約付きで表示されます:
h[m: src.C → src.X | F(m) = ...]: tgt.D → tgt.Y
| の後が制約です。制約はユーザーが記述するものではなく、自動的に生成されます。
呼び出し時の検証
h を具体的なセルで呼び出すとき、制約が検証されます。
src += { u: C → X }
tgt += { v: D → Y }
F(src.u) = tgt.v
result = h[src.u] // OK: F(src.u) = tgt.v が定義されている
F のマッピングに含まれないセルを渡すとエラーになります。
制約の伝搬
制約付きの定義を別の定義から呼ぶと、制約が伝搬します。
g[n: src.C → src.X] = h[n]
// g にも h と同じ制約が付く
ネストした functor
functor の適用をネストすることもできます。
f(g(m))
// g(m) と f(g(m)) の両方に制約が生成される
計算の書き方
import "sys" を使った具体的な計算の書き方を説明します。
ワイヤーの束
Donut の計算では、データは ワイヤー(1-cell)の束として流れます(donut-app では上から下に描画されます)。計算のどの時点でも「今、手元にどんなワイヤーがあるか」を意識します。
import "sys"
// f32.lit[3] は「何もないところから f32 を1本生やす」
// C → f32
three = f32.lit[3]
ここで C は「ワイヤーが0本」の状態です。f32.lit[3] は 0本の状態から f32 ワイヤーを1本作ります。
1次合成(;)
; で2つの操作を繋ぐと、前の出力が次の入力になります。
// f32.lit[3]; f32.neg
// C → f32 → f32
// = -3
neg_three = f32.lit[3]; f32.neg
f32.lit[3] が C → f32、f32.neg が f32 → f32 なので、繋ぐと C → f32 になります。
0次合成(スペース)
スペースで2つの操作を並べると、別々のワイヤーに対して同時に動作します。
// f32.lit[1] f32.lit[2]
// C → f32 f32
// 手元に f32 が2本ある状態
pair = f32.lit[1] f32.lit[2]
この2本のワイヤーを f32.add に渡すと:
// f32.lit[1] f32.lit[2]; f32.add
// C → f32 f32 → f32
// = 3
sum = f32.lit[1] f32.lit[2]; f32.add
ワイヤーの管理
通常のプログラミング言語では変数に名前を付けて自由に何度でも参照できます。Donut ではそうではなく、ワイヤーの束を明示的に操作します。
複製: val.dup
値を2回使いたい場合、明示的に複製します。
// val.dup[f32]: f32 → f32 f32
// 1本のワイヤーを2本に分ける
// x² を計算する: x を複製して掛ける
square: f32 → f32 = val.dup[f32]; f32.mul
破棄: val.drop
使わないワイヤーは明示的に捨てます。
// val.drop[f32]: f32 → C
// ワイヤーを1本消す
// 2本のうち最初だけ残す
first: f32 f32 → f32 = f32 val.drop[f32]
f32 val.drop[f32] は「最初の f32 はそのまま通し、2番目の f32 を捨てる」という並列合成です。
入れ替え: val.swap
ワイヤーの順番を入れ替えます。
// val.swap[f32, u32]: f32 u32 → u32 f32
考え方: 手元のワイヤーを追う
計算を書くときは、各ステップで「今ワイヤーが何本、どんな型で並んでいるか」を追います。
例: (a + b) * (a - b) を計算する関数 f32 f32 → f32
// 入力: a b (f32 が2本)
diff_of_squares: f32 f32 → f32 =
val.dup[f32] val.dup[f32]; // a a b b
f32 val.swap[f32, f32] f32; // a b a b
f32.add f32.sub; // (a+b) (a-b)
f32.mul // (a+b)*(a-b)
各行で手元のワイヤーがどう変化するかを追うのがコツです:
a b— 入力 (2本)val.dup[f32] val.dup[f32]— 各ワイヤーを複製:a a b b(4本)f32 val.swap[f32, f32] f32— 1本目はそのまま、中央2本を入れ替え、4本目はそのまま:a b a bf32.add f32.sub— 前2本を加算、後2本を減算:(a+b) (a-b)(2本)f32.mul— 乗算:(a+b)*(a-b)(1本)
identity と定数の組み合わせ
1-cell の名前をそのまま値として書くと、そのワイヤーを素通りさせる identity になります。これと定数生成を 0次合成すると「元の値を保ちつつ定数を追加」できます。
// x を受け取り、x と 1 のペアにする
with_one: f32 → f32 f32 = f32 f32.lit[1]
f32 は identity(f32 → f32)、f32.lit[1] は定数(C → f32)。0次合成で f32 → f32 f32 になります。
括弧 () を使うと部分式をまとめられます:
// 入力 x に対して (x², x) を作る
square_and_keep: f32 → f32 f32 = val.dup[f32]; (val.dup[f32]; f32.mul) f32
まとめ
- 計算の状態は常に「ワイヤーの束」
;で前の出力を次の入力に繋ぐ- スペースで別々のワイヤーに同時に操作する
- 値を使い回すには
val.dupで複製 - 不要な値は
val.dropで破棄 - 変数名で参照する代わりに、ワイヤーの並び順で管理する
sys ライブラリ
import "sys" で使えるプリミティブ型と演算の一覧です。
すべての型は C → C の 1-cell として定義されています。C は sys ライブラリの共通の 0-cell です。
型
| 型 | 説明 |
|---|---|
bool | 真偽値 |
u32 | 32bit 符号なし整数 |
i32 | 32bit 符号付き整数 |
f32 | 32bit 浮動小数点数 |
f32x2 | f32 の2要素ベクトル |
f32x3 | f32 の3要素ベクトル |
bool
| 演算 | 型 | 説明 |
|---|---|---|
bool.lit[n] | C → bool | リテラル(n: nat) |
bool.true | C → bool | 真 |
bool.false | C → bool | 偽 |
bool.not | bool → bool | 否定 |
bool.and | bool bool → bool | 論理積 |
bool.or | bool bool → bool | 論理和 |
bool.ind[x] | x x bool → x | 分岐。真なら第1引数、偽なら第2引数を返す |
u32
| 演算 | 型 | 説明 |
|---|---|---|
u32.lit[n] | C → u32 | リテラル(n: nat) |
u32.add | u32 u32 → u32 | 加算 |
u32.sub | u32 u32 → u32 | 減算 |
u32.mul | u32 u32 → u32 | 乗算 |
u32.div | u32 u32 → u32 | 除算 |
u32.mod | u32 u32 → u32 | 剰余 |
u32.neg | u32 → u32 | 符号反転 |
u32.eq, u32.ne | u32 u32 → bool | 等値比較 |
u32.lt, u32.le, u32.gt, u32.ge | u32 u32 → bool | 順序比較 |
u32.to_f32 | u32 → f32 | f32 への変換 |
u32.to_i32 | u32 → i32 | i32 への変換 |
i32
| 演算 | 型 | 説明 |
|---|---|---|
i32.lit[n] | C → i32 | リテラル(n: nat) |
i32.add | i32 i32 → i32 | 加算 |
i32.sub | i32 i32 → i32 | 減算 |
i32.mul | i32 i32 → i32 | 乗算 |
i32.div | i32 i32 → i32 | 除算 |
i32.mod | i32 i32 → i32 | 剰余 |
i32.neg | i32 → i32 | 符号反転 |
i32.eq, i32.ne | i32 i32 → bool | 等値比較 |
i32.lt, i32.le, i32.gt, i32.ge | i32 i32 → bool | 順序比較 |
i32.to_f32 | i32 → f32 | f32 への変換 |
f32
| 演算 | 型 | 説明 |
|---|---|---|
f32.lit[n] | C → f32 | リテラル(n: rat) |
f32.add | f32 f32 → f32 | 加算 |
f32.sub | f32 f32 → f32 | 減算 |
f32.mul | f32 f32 → f32 | 乗算 |
f32.div | f32 f32 → f32 | 除算 |
f32.neg | f32 → f32 | 符号反転 |
f32.floor | f32 → i32 | 切り捨て |
f32.ceil | f32 → i32 | 切り上げ |
f32.eq, f32.ne | f32 f32 → bool | 等値比較 |
f32.lt, f32.le, f32.gt, f32.ge | f32 f32 → bool | 順序比較 |
f32x2
| 演算 | 型 | 説明 |
|---|---|---|
f32x2.lit[x, y] | C → f32x2 | リテラル(x, y: rat) |
f32x2.pack | f32 f32 → f32x2 | 2つの f32 をパック |
f32x2.unpack | f32x2 → f32 f32 | f32x2 を2つの f32 に展開 |
f32x2.add | f32x2 f32x2 → f32x2 | 加算 |
f32x2.sub | f32x2 f32x2 → f32x2 | 減算 |
f32x2.mul | f32x2 f32x2 → f32x2 | 乗算 |
f32x2.div | f32x2 f32x2 → f32x2 | 除算 |
f32x2.neg | f32x2 → f32x2 | 符号反転 |
f32x2.scale | f32 f32x2 → f32x2 | スカラー倍 |
f32x3
| 演算 | 型 | 説明 |
|---|---|---|
f32x3.lit[x, y, z] | C → f32x3 | リテラル(x, y, z: rat) |
f32x3.pack | f32 f32 f32 → f32x3 | 3つの f32 をパック |
f32x3.unpack | f32x3 → f32 f32 f32 | f32x3 を3つの f32 に展開 |
f32x3.add | f32x3 f32x3 → f32x3 | 加算 |
f32x3.sub | f32x3 f32x3 → f32x3 | 減算 |
f32x3.mul | f32x3 f32x3 → f32x3 | 乗算 |
f32x3.div | f32x3 f32x3 → f32x3 | 除算 |
f32x3.neg | f32x3 → f32x3 | 符号反転 |
f32x3.scale | f32 f32x3 → f32x3 | スカラー倍 |
val(構造操作)
| 演算 | 型 | 説明 |
|---|---|---|
val.dup[x] | x → x x | 値の複製 |
val.drop[x] | x → C | 値の破棄 |
val.swap[x, y] | x y → y x | 値の入れ替え |
x, y は任意の C → C 型(1-cell)をパラメータとして受け取ります。
実行
donut-app では、import "sys" で定義されたプリミティブだけで構成された 2-cell を 評価 できます。
評価の条件
評価できるセルは以下を満たす必要があります:
import "sys"のC上の 2-cell であること(C → Cの 1-cell 間の射)- パラメータを持たないこと
- すべてのプリミティブが sys ライブラリに属すること
ドロップダウンでセルを選択すると、評価可能な場合は結果が表示されます。
例
import "sys"
one = f32.lit[1]
// → 1
add_one: f32 → f32 = f32.lit[1] f32; f32.add
// → failed to eval: needs 1 input(s)
入力がないセル(C → ...)はそのまま値が計算されます。入力を取るセル(f32 → f32 等)は評価できず、エラーメッセージが表示されます。
GLSL コンパイル
sys のプリミティブだけで構成された 2-cell は GLSL にコンパイルできます。シェーダービューポートで描画するには以下の条件を満たす必要があります:
- 入力の float 成分数が 1〜2(例:
f32,f32x2,f32 f32) - 出力の float 成分数が 1〜3(例:
f32,f32x2,f32x3,f32 f32 f32)
入力にはピクセル座標(vec2 uv)が渡され、出力は RGB 色として解釈されます。出力が 1 成分ならグレースケール、2 成分なら RG、3 成分なら RGB になります。
例
Donut の具体的な使い方を例を通じて紹介します。
例: pentagon
モノイドの結合律に関する pentagon identity(五角恒等式)を Donut で記述する例です。
全体コード
u: *
x: u → u
μ: x x → x
α: μ x; μ → x μ; μ
icl: (x μ; μ) x → x μ x; μ x
icr: x μ x; x μ → x (μ x; μ)
top =
α x; μ ;;
icl; μ ;;
x μ x; α ;;
icr; μ ;;
x α; μ
ic0: μ x x; x μ → μ μ
ic1: μ μ → x x μ; μ x
kl: (μ x; μ) x → μ x x; μ x
kr: x x μ; x μ → x (x μ; μ)
bot =
kl; μ ;;
μ x x; α ;;
(ic0 ;; ic1); μ ;;
x x μ; α ;;
kr; μ
pentagon: top → bot
result = pentagon
解説
基本構造
u: *
x: u → u
μ: x x → x
u— 0-cell(対象)x— 1-cell(u上の射)μ— 2-cell(二項演算。xを2つ受け取りxを返す)
これはモノイドの骨格です。
結合律 (associator)
α: μ x; μ → x μ; μ
α は 3-cell です。source と target はそれぞれ x を3つ合成する2通りの括弧付けを表します:
μ x; μ—μ(μ(a, b), c)— 左から結合x μ; μ—μ(a, μ(b, c))— 右から結合
interchange cell
icl: (x μ; μ) x → x μ x; μ x
icr: x μ x; x μ → x (μ x; μ)
4つの x を結合する際に、括弧の位置を入れ替える 3-cell です。
2つの経路
x を4つ結合するとき、括弧の付け方は5通りあります:
((ab)c)d → (a(bc))d → a((bc)d) → a(b(cd))
((ab)c)d → (ab)(cd) → a(b(cd))
完全左結合 ((ab)c)d から完全右結合 a(b(cd)) に至る経路が2通りあり、それぞれが top と bot に対応します。
top: 上の経路
top =
α x; μ ;; -- ((ab)c)d → (a(bc))d
icl; μ ;; -- interchange: 括弧を外す
x μ x; α ;; -- 内側に α を適用
icr; μ ;; -- interchange: 括弧を戻す
x α; μ -- → a(b(cd))
各ステップは 3-cell で、;; による 2次合成で繋いでいます。上の経路の図では3ステップですが、コードでは interchange cell(icl, icr)による中間ステップが必要なため5ステップになっています。α x; μ は「左3つに α を適用し、残りの x は恒等的に通す」ことを意味します。
bot: 下の経路
bot =
kl; μ ;; -- ((ab)c)d → (ab)(cd)
μ x x; α ;; -- (ab)(cd) に α を適用
(ic0 ;; ic1); μ ;; -- interchange
x x μ; α ;; -- 左側に α を適用
kr; μ -- → a(b(cd))
こちらは途中で (ab)(cd) という「2つずつに分ける」括弧付けを経由します。
pentagon: coherence
pentagon: top → bot
top と bot はどちらも同じ source(完全左結合)と target(完全右結合)を持つ 3-cell です。pentagon はこの2つの経路の間の 4-cell であり、「どちらの経路で括り直しても結果は同じ」という coherence 条件を表現しています。
これが Mac Lane の pentagon identity — モノイダル圏の公理の中核です。
例: functor によるコンパイル
Functor は抽象的な構造のプログラムを具体的な実装に翻訳する「コンパイラ」として使えます。しかし functor F(...) は Donut のメタ操作であり、型チェック時に展開されるだけの存在です。この例では、functor と同じ翻訳を セル合成 で表現する方法を示します。
設定
自然数のような抽象構造を定義します。
D: *
x: D → D
zero: D → x
succ: x → x
add: x x → x
Functor: メタ的なコンパイル
functor でマッピングを定義すると、D のプログラムを sys の i32 演算に翻訳できます。
import "sys"
F: D ~> C
F(x) = i32
F(zero) = i32.lit[0]
F(succ) = i32.lit[1] i32; i32.add
F(add) = i32.add
two = zero; succ; succ
F(two) // i32.lit[0]; ...; i32.add
F(two two; add) // F(two) F(two); i32.add
F(...) は便利ですが、あくまでメタ操作です。Donut のセル合成 (;, ;;, スペース) の体系からは外にあり、セルとして合成したり、高次のセルの source/target に置いたりすることはできません。
セル合成による翻訳
functor と同じ翻訳を、通常のセルの合成で表現するプリミティブを導入します。
L: C → D
R: D → C
T: C → L R
B: L x R → F(x)
L,R— C と D を行き来する 1-cellT: C → L R— C から L R への変換B: L x R → F(x)— L で埋め込んだ空間での計算結果を F(x) に変換
これらを組み合わせると:
compile[u: D → x] = T; L u R; B
compile[u] の型は C → F(x) です。T で L R の空間に入り、L u R で抽象プログラム u を適用し、B で具体的な値に変換します。
メタ操作との等価性
compile と functor F が同じ結果を生むことを宣言できます。
η[u: D → x]: compile[u] ~ F(u)
u はパラメータなので F(u) に対して functor 制約が自動生成されます。
具体的なプログラムでは:
three = zero; succ; succ; succ
result = compile[three]
result は T; L (zero; succ; succ; succ) R; B というセル合成です。F(three) がメタ操作による展開なのに対し、compile[three] は L, R, T, B という宣言されたセルの合成として構成されています。
なぜこれが重要か
F(...) はメタ操作なので、セル合成の体系の中では「見えない」存在です。F(two) の結果は i32 の演算に展開されますが、その「翻訳した」という構造は消えてしまいます。
一方 compile[u] = T; L u R; B はセル合成そのものです。つまり:
compile[u]を source/target に持つ 3-cell を宣言できる- 他のセルと
;や;;で自由に 合成 できる ηのような等価性を通じて、メタ操作Fとの関係を高次セルで記述できる
翻訳という操作自体がセル合成の体系の中の一級市民になり、その性質(正しさ、他の翻訳との関係など)をセルの言葉で語れるようになります。
例: mandelbrot
import "sys" のプリミティブを使って Mandelbrot 集合 を描画するプログラムです。すべてのロジックが 2-cell の合成として記述されています。
全体コード
import "sys"
fdup = val.dup[f32]
square :=
val.dup[f32x2];
f32x2.unpack f32x2.unpack;
(fdup; f32.mul) (fdup; f32.mul) (f32.lit[2] f32.mul; f32.mul);
f32.sub f32;
f32x2.pack
step: f32x2 f32x2 → f32x2 f32x2 =
square val.dup[f32x2]; f32x2.add f32x2
rep4[x: C → C, f: x → x]: x → x = f; f; f; f
step4 := rep4[f32x2 f32x2, step]
step16 := rep4[f32x2 f32x2, step4]
step64 := rep4[f32x2 f32x2, step16]
coloring: f32x2 → f32 := f32x2.unpack;
(fdup; f32.mul) (fdup; f32.mul);
f32.add f32.lit[2];
f32.le;
f32.lit[1] f32.lit[0] bool;
bool.ind[f32]
result = f32x2.lit[0,0] (f32x2 f32x2.lit[0.6,0.5]; f32x2.sub; f32.lit[3] f32x2; f32x2.scale);
step64;
f32x2 val.drop[f32x2];
coloring
解説
前提: sys ライブラリ
import "sys" により、以下のプリミティブが使えます:
f32,f32x2— 浮動小数点型。すべてC → Cの 1-cellf32.add,f32.mul,f32.sub— 算術演算(2つのf32を受け取りf32を返す 2-cell)f32x2.pack/f32x2.unpack—f32 f32 ↔ f32x2の変換val.dup[x]—x → x x(値の複製)val.drop[x]—x → C(値の破棄)
Donut では関数は 2-cell の合成であり、すべてのデータは 1-cell の「ワイヤー」として流れます。
fdup: f32 の複製
fdup = val.dup[f32]
f32 → f32 f32。1つの f32 値を複製して2つにします。頻出するのでエイリアスしています。
square: 複素数の二乗
square :=
val.dup[f32x2];
f32x2.unpack f32x2.unpack;
(fdup; f32.mul) (fdup; f32.mul) (f32.lit[2] f32.mul; f32.mul);
f32.sub f32;
f32x2.pack
型は f32x2 → f32x2。複素数 (z = a + bi) の二乗 (z^2 = (a^2 - b^2) + 2abi) を計算します。
データフローを追うと:
val.dup[f32x2]— 入力(a, b)を複製:(a, b) (a, b)f32x2.unpack f32x2.unpack— 展開:a b a b(fdup; f32.mul) (fdup; f32.mul) (f32.lit[2] f32.mul; f32.mul)- 最初の2つ:
aを複製してa*a、bを複製してb*b - 3つ目: 定数
2とaとbを掛けて2*a*b - 結果:
a² b² 2ab
- 最初の2つ:
f32.sub f32—a² - b²と2abf32x2.pack—(a² - b², 2ab)にパック
:= で定義しているので、square は独立したセルとして宣言されつつ、評価時にはこの合成として計算されます。
step: Mandelbrot の反復ステップ
step: f32x2 f32x2 → f32x2 f32x2 =
square val.dup[f32x2]; f32x2.add f32x2
型は f32x2 f32x2 → f32x2 f32x2。入力は (z, c) で、(z \leftarrow z^2 + c) を計算して (z', c) を返します。
square val.dup[f32x2]—zにsquareを適用してz²にし、cを複製:z² c cf32x2.add f32x2—z² + cとc:(z²+c, c)
c を保持したまま z を更新するので、繰り返し適用できます。
rep4 と反復
rep4[x: C → C, f: x → x]: x → x = f; f; f; f
step4 := rep4[f32x2 f32x2, step]
step16 := rep4[f32x2 f32x2, step4]
step64 := rep4[f32x2 f32x2, step16]
rep4 はパラメトリックな定義で、任意の 2-cell f: x → x を4回繰り返します。
step4= step を 4 回 = 4 回反復step16= step4 を 4 回 = 16 回反復step64= step16 を 4 回 = 64 回反復
:= で定義しているので、それぞれ独立したセルとして扱いつつ、評価時には展開されます。
coloring: 発散判定
coloring: f32x2 → f32 := f32x2.unpack;
(fdup; f32.mul) (fdup; f32.mul);
f32.add f32.lit[2];
f32.le;
f32.lit[1] f32.lit[0] bool;
bool.ind[f32]
型は f32x2 → f32。最終的な z の値から色を決定します。
f32x2.unpack—(a, b)をa bに展開(fdup; f32.mul) (fdup; f32.mul)—a²とb²を計算f32.add f32.lit[2]—a² + b²と定数2f32.le—a² + b² ≤ 2→boolf32.lit[1] f32.lit[0] bool— 定数1、定数0、判定結果を並べるbool.ind[f32]—boolの値で分岐。真なら1(集合内)、偽なら0(発散)
result: 全体の組み立て
result = f32x2.lit[0,0] (f32x2 f32x2.lit[0.6,0.5]; f32x2.sub; f32.lit[3] f32x2; f32x2.scale);
step64;
f32x2 val.drop[f32x2];
coloring
型は f32x2 → f32。ピクセル座標 f32x2(入力)を受け取り、色 f32 を返します。
- 初期値の準備:
z = (0, 0)とcを用意。cは入力座標を(0.6, 0.5)を中心に、スケール3で変換したもの step64— 64 回反復f32x2 val.drop[f32x2]—cを捨ててzだけ残すcoloring— 発散判定して色に変換
ポイント
- すべてのロジックが 2-cell の合成 で表現されている
- 分岐(if/else)は
bool.indで実現 - ループは
rep4のパラメトリック定義を入れ子にして実現 :=(定義)を使うことで、中間セルに名前を付けつつ評価時は展開