例: 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との関係を高次セルで記述できる
翻訳という操作自体がセル合成の体系の中の一級市民になり、その性質（正しさ、他の翻訳との関係など）をセルの言葉で語れるようになります。