Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Donut とは

Note: Donut は開発中のプロトタイプです。仕様や動作は予告なく変更される可能性があり、このドキュメントも不完全・不正確な部分を含む場合があります。ドキュメントの大部分は Claude Code によって生成されています。

Donut は 高次元セル を合成してプログラムを組み立てる言語です。

通常のプログラミング言語が「値」と「関数」を扱うのに対し、Donut では セル を宣言して繋ぎ合わせます。セルには次元があり、次元ごとに異なる役割を持ちます:

次元意味
0-cell環境・コンテキストC: *
1-cellInt: 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
  • u0-cell(環境)
  • xu 上の 1-cell(型)
  • mx 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 → uu から 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 → xS = Tm: Sm: x x → x と解釈されます。

型の階層

意味
*0-cellu: *
A → B1-cell 以上(射)x: u → u
A ~ B等価性e: x ~ y
A ~> BfunctorF: 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)と書くことで任意の次数を数値で指定することもできます。

優先順位

高次の合成ほど結合が弱くなります:

  1. スペース(0次)— 最も強い
  2. ;(1次)
  3. ;;(2次)
  4. ;;;(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].xcat[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

exy が等しいことを示す 2-cell です。 と同じく arrow 型ですが、方向を持たない(対称的な)関係を表現します。

との違い

意味方向
x → yx から y への射あり
x ~ yxy の等価性なし

は一方向の射を表しますが、~ は双方向の等価関係を表します。

定義 (:=) との関連

定義 (:=) を使うと、等価性が自動的に生成されます。

x: * := y

これは x: * を宣言し、x.def: x ~ y を自動生成します。xy は異なるセルとして存在しますが、評価上は等しいことを ~ で表現しています。

定義

:= を使うと、宣言と定義を同時に行えます。

基本

a: *
x: * := a

これは以下を行います:

  • x: * を新しいセルとして宣言する
  • x.def: x ~ a を自動生成する(xa の等価性)
  • ランタイムで x を評価する際、a として計算する

型は右辺から推論することもできます:

import "sys"
add := f32.add

用途

定義は「新しい名前を付けつつ、計算は既存のセルに委譲する」パターンで使います。図式上では独立したセルとして表示されますが、評価時には右辺として計算されます。

次元の自動リフト

低次元のセルが高次元の位置で使われた場合、自動的に identity cell としてリフト(昇格)されます。

u: *
h: u → u = u

u は 0-cell ですが、u → u(1-cell の型)の位置で使われています。この場合 uu 上の identity 1-cell(恒等射)として解釈されます。

合成での自動リフト

合成の中で次元の異なるセルが混在する場合、低い方が自動的にリフトされます。

u: *
x: u → u
μ: x x → x

// μ は 2-cell。x は 1-cell だが、2-cell の位置で使われると id(x) にリフトされる
α: μ x; μ → x μ; μ

μ xx は 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 の違い

importuse はどちらも無名で使うとライブラリの中身をスコープに展開します。違いは 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" だけで natrat も使えます。

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 → f32f32.negf32 → 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)

各行で手元のワイヤーがどう変化するかを追うのがコツです:

  1. a b — 入力 (2本)
  2. val.dup[f32] val.dup[f32] — 各ワイヤーを複製: a a b b (4本)
  3. f32 val.swap[f32, f32] f32 — 1本目はそのまま、中央2本を入れ替え、4本目はそのまま: a b a b
  4. f32.add f32.sub — 前2本を加算、後2本を減算: (a+b) (a-b) (2本)
  5. 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真偽値
u3232bit 符号なし整数
i3232bit 符号付き整数
f3232bit 浮動小数点数
f32x2f32 の2要素ベクトル
f32x3f32 の3要素ベクトル

bool

演算説明
bool.lit[n]C → boolリテラル(n: nat
bool.trueC → bool
bool.falseC → bool
bool.notbool → bool否定
bool.andbool bool → bool論理積
bool.orbool bool → bool論理和
bool.ind[x]x x bool → x分岐。真なら第1引数、偽なら第2引数を返す

u32

演算説明
u32.lit[n]C → u32リテラル(n: nat
u32.addu32 u32 → u32加算
u32.subu32 u32 → u32減算
u32.mulu32 u32 → u32乗算
u32.divu32 u32 → u32除算
u32.modu32 u32 → u32剰余
u32.negu32 → u32符号反転
u32.eq, u32.neu32 u32 → bool等値比較
u32.lt, u32.le, u32.gt, u32.geu32 u32 → bool順序比較
u32.to_f32u32 → f32f32 への変換
u32.to_i32u32 → i32i32 への変換

i32

演算説明
i32.lit[n]C → i32リテラル(n: nat
i32.addi32 i32 → i32加算
i32.subi32 i32 → i32減算
i32.muli32 i32 → i32乗算
i32.divi32 i32 → i32除算
i32.modi32 i32 → i32剰余
i32.negi32 → i32符号反転
i32.eq, i32.nei32 i32 → bool等値比較
i32.lt, i32.le, i32.gt, i32.gei32 i32 → bool順序比較
i32.to_f32i32 → f32f32 への変換

f32

演算説明
f32.lit[n]C → f32リテラル(n: rat
f32.addf32 f32 → f32加算
f32.subf32 f32 → f32減算
f32.mulf32 f32 → f32乗算
f32.divf32 f32 → f32除算
f32.negf32 → f32符号反転
f32.floorf32 → i32切り捨て
f32.ceilf32 → i32切り上げ
f32.eq, f32.nef32 f32 → bool等値比較
f32.lt, f32.le, f32.gt, f32.gef32 f32 → bool順序比較

f32x2

演算説明
f32x2.lit[x, y]C → f32x2リテラル(x, y: rat
f32x2.packf32 f32 → f32x22つの f32 をパック
f32x2.unpackf32x2 → f32 f32f32x2 を2つの f32 に展開
f32x2.addf32x2 f32x2 → f32x2加算
f32x2.subf32x2 f32x2 → f32x2減算
f32x2.mulf32x2 f32x2 → f32x2乗算
f32x2.divf32x2 f32x2 → f32x2除算
f32x2.negf32x2 → f32x2符号反転
f32x2.scalef32 f32x2 → f32x2スカラー倍

f32x3

演算説明
f32x3.lit[x, y, z]C → f32x3リテラル(x, y, z: rat
f32x3.packf32 f32 f32 → f32x33つの f32 をパック
f32x3.unpackf32x3 → f32 f32 f32f32x3 を3つの f32 に展開
f32x3.addf32x3 f32x3 → f32x3加算
f32x3.subf32x3 f32x3 → f32x3減算
f32x3.mulf32x3 f32x3 → f32x3乗算
f32x3.divf32x3 f32x3 → f32x3除算
f32x3.negf32x3 → f32x3符号反転
f32x3.scalef32 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通りあり、それぞれが topbot に対応します。

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

topbot はどちらも同じ 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-cell
  • T: 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]

resultT; 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-cell
  • f32.add, f32.mul, f32.sub — 算術演算(2つの f32 を受け取り f32 を返す 2-cell)
  • f32x2.pack / f32x2.unpackf32 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) を計算します。

データフローを追うと:

  1. val.dup[f32x2] — 入力 (a, b) を複製: (a, b) (a, b)
  2. f32x2.unpack f32x2.unpack — 展開: a b a b
  3. (fdup; f32.mul) (fdup; f32.mul) (f32.lit[2] f32.mul; f32.mul)
    • 最初の2つ: a を複製して a*ab を複製して b*b
    • 3つ目: 定数 2ab を掛けて 2*a*b
    • 結果: a² b² 2ab
  4. f32.sub f32a² - b²2ab
  5. f32x2.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) を返します。

  1. square val.dup[f32x2]zsquare を適用して にし、c を複製: z² c c
  2. f32x2.add f32x2z² + cc: (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 の値から色を決定します。

  1. f32x2.unpack(a, b)a b に展開
  2. (fdup; f32.mul) (fdup; f32.mul) を計算
  3. f32.add f32.lit[2]a² + b² と定数 2
  4. f32.lea² + b² ≤ 2bool
  5. f32.lit[1] f32.lit[0] bool — 定数 1、定数 0、判定結果を並べる
  6. 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 を返します。

  1. 初期値の準備: z = (0, 0)c を用意。c は入力座標を (0.6, 0.5) を中心に、スケール 3 で変換したもの
  2. step64 — 64 回反復
  3. f32x2 val.drop[f32x2]c を捨てて z だけ残す
  4. coloring — 発散判定して色に変換

ポイント

  • すべてのロジックが 2-cell の合成 で表現されている
  • 分岐(if/else)は bool.ind で実現
  • ループは rep4 のパラメトリック定義を入れ子にして実現
  • :=(定義)を使うことで、中間セルに名前を付けつつ評価時は展開