維度類型系統與確定性內存管理：原生編譯中的設計時語義保持

維度類型系統與確定性內存管理：原生編譯中的設計時語義保持

Dimensional Type Systems and Deterministic Memory Management:Design-Time Semantic Preservation in Native Compilation

https://arxiv.org/pdf/2603.16437v6

摘要

我們提出了一種編譯框架，在該框架中，維度類型注釋在多階段MLIR降級（lowering）過程中得以保留，從而使編譯器能夠將數值表示選擇與確定性內存管理作為單一程序語義圖（PSG）的共效應（coeffect）屬性進行聯合求解。這兩項關注點之間的耦合是本工作的核心貢獻：維度推理決定值域；值域決定數值表示的選擇；數值表示的選擇決定字寬與內存占用大小；而內存占用大小結合逃逸分類，共同決定分配策略、緩存行為以及跨目標平臺的傳輸保真度。該鏈條中的每一步均消耗前一步推理的輸出結果。

維度類型系統（DTS）在Hindley–Milner合一算法的基礎上引入了源自有限生成阿貝爾群的約束，從而實現了可在多項式時間內判定、完備（無需額外標注）且具備主類型（principal）特性的維度推理。傳統系統通常在代碼生成前擦除維度注釋，而DTS則將其作為編譯元數據貫穿每一個降級階段，使其在需要進行數值表示選擇與內存布局決策的節點上保持可用。計算值的維度范圍指導各目標平臺的格式選擇：在FPGA目標上采用具有錐形精度（tapered precision）的Posit算術，在通用CPU上采用IEEE 754標準，或在神經形態核心上采用定點數格式。

確定性內存管理（DMM）在同一圖中被形式化為一種共效應規范，將逃逸分析與內存布局同維度框架相統一。該逃逸分析將值生命周期劃分為四類（棧作用域、閉包捕獲、返回逃逸、引用逃逸），每一類均映射至一種在編譯期完成驗證的特定分配策略。針對Posit目標，其Quire累加器的分配、生命周期及精確累加語義均作為共效應屬性在PSG中予以解析。我們明確了其對自動微分的意義：維度代數在鏈式法則下保持封閉，且前向模式梯度計算[3]展現出特定的共效應簽名（無需激活磁帶、每層僅需O(1)輔助內存），該框架能夠對此進行驗證。其實際成果是構建了一個開發環境，在該環境中，逃逸診斷、分配策略、表示保真度以及緩存局部性估計均可作為編譯圖在設計期的視圖直接呈現。

1 引言

1.1 維度注釋生命周期

當代用于數值計算的類型系統，在編譯期間維度信息保持可用的時長上存在差異。帶有維度注釋的系統（如 F# 的度量單位 [14]、C++ 中的 Boost.Units [25]）會在代碼生成之前丟棄這些注釋。維度信息僅作為編譯期檢查使用，隨后便消失；所生成的代碼對維度毫無感知。我們將此稱為早期擦除：注釋在類型檢查階段被消耗，無法存活至進行數值表示選擇與內存放置決策的編譯階段。具有豐富依賴類型的系統（如 F* [28]、Idris [4]、Agda [18]）會將類型級信息保留至生成的代碼中，但代價是犧牲了自動化能力：盡管按設計對完全細化（elaborated）項進行類型檢查是可判定的，但在一般依賴情況下的證明搜索與類型推斷并非完全可自動化，因此實際系統需要用戶提供證明項并采用交互式開發，且基于求解器的驗證依賴于超時啟發式策略。

這兩種方法均無法滿足在異構硬件目標上與物理現實交互的系統的要求。運行于 x86 主機、FPGA 加速器與神經形態處理器上的傳感器融合流水線，需要維度約束在編譯過程中持續足夠長的時間，以指導內存放置并為跨目標數據傳輸協議提供依據。早期擦除在該信息可被利用之前就將其丟棄。完整的依賴類型系統在實踐中提供了交互式開發環境（如 Lean 4、Agda、Idris 2）；按設計，在這些系統中對完整項進行類型檢查是可判定的，但在一般依賴情況下的證明搜索與類型推斷并非完全可自動化，仍需用戶提供證明項并進行交互式開發。這帶來了無限制的注釋負擔，并阻礙了無條件的語言服務器響應時間保證，且實際系統依賴于超時啟發式策略與燃料限制（fuel limits）來進行基于求解器的驗證。

DTS 采取了一條中間路徑：維度注釋作為編譯元數據貫穿多階段降級（lowering）過程，在每個需要其輔助決策的階段均可用，并在原生代碼發射之前被丟棄。這些注釋在運行時并不存在；沒有具象化的類型信息，沒有 typeof 操作，也沒有基于維度的運行時分發。與早期擦除的區別在于注釋的生命周期，而非具象化（reification）。DTS 對可判定代數理論（整數集 Z 上的阿貝爾群、枚舉排序、位向量約束）的限制，保證了每次查詢的推斷均在有界時間內完成；這一特性簡化了語言服務器架構，并為設計期工具提供了無條件的響應時間保證。其代價是表達能力：DTS 無法編碼任意謂詞。該可判定性保證使得一類特定的設計期反饋成為可能：多目標解析、內存放置分析、逃逸診斷以及表示保真度評分。在依賴類型系統中將這些編譯器內部屬性編碼為類型，將帶來架構上不必要的開銷，因為編譯器在常規細化（elaboration）過程中已經計算了這些屬性。

1.2 貢獻

本文提出三項主張：

1. 貫穿編譯過程持續存在的維度注釋使得數值表示選擇與內存管理能夠聯合求解。 這種耦合是本工作的核心貢獻，也是 DTS 與 DMM 出現在同一篇論文中的原因。維度推理決定值域；值域決定數值表示的選擇；數值表示的選擇決定字寬與內存占用大小；內存占用大小結合逃逸分類，共同決定分配策略、緩存行為以及跨目標平臺的傳輸保真度。這些決策作為共效應（coeffect）屬性在程序語義圖（Program Semantic Graph, PSG）中組合而成，該鏈條若被分解將會丟失各階段之間流動的信息。其代數基礎是整數集 ? 上的有限生成阿貝爾群，這一基礎將 DTS 置于一個特定的形式化生態位：可在多項式時間內判定、可通過擴展 Hindley–Milner 合一算法實現完全推斷、并且可作為元數據在多階段編譯中保留而不改變生成代碼的操作語義。這一生態位既區別于依賴類型，也區別于參數多態（第 2.4 節）。
2. 推斷機制推導出決定下游編譯決策的組合依賴屬性。 維度注釋可以通過多條路徑進入系統：從未注釋源代碼進行的 Hindley–Milner 推斷（默認方式）、程序員顯式標注、領域庫綁定（例如預填充維度約束的物理庫），或包括 AI 輔助代碼生成在內的外部工具。無論來源如何，編譯流水線的行為均保持一致。推斷工作的貢獻并非注釋的便利性，而是推導那些從程序圖中約束交互涌現出來的屬性。維度范圍、逃逸分類以及表示兼容性均是組合依賴的：它們無法從任何單個值的注釋中確定，而是產生于函數邊界、循環嵌套以及跨模塊接口處的約束交互。這些推導出的屬性共同決定數值表示選擇、字寬、分配策略以及緩存行為。
3. 統一的 DTS+DMM 圖啟用了一類新型的軟件設計期工具。 由于 PSG 在編譯過程中保留了維度與內存注釋，語言服務器可以將編譯器的內部分析呈現為交互式設計指導：逃逸分析診斷、分配提升警告、緩存局部性估計以及重構建議。這將編譯圖從一種瞬態的構建產物轉變為一種持久化的設計期資源。

1.3 范圍與背景

本文所述的系統在 Clef 編程語言與 Fidelity 編譯框架中實現。Clef 是一種屬于 ML 家族的函數式語言，其主要語法與語義譜系源自 F#，但另有若干其他系統對其設計產生了形成性影響。F* [28] 證明了表示寬度與類型同一性可作為相互獨立的關注點進行處理，這一分離直接啟發了 Clef 對維度持久化的處理方式：類型承載物理語義，而表示形式（Posit 位寬、浮點格式、定點配置）則按目標平臺獨立解析。F* 使用 SMT-LIB2 [2] 進行自動化證明卸載，也確立了將基于求解器的驗證集成至 ML 家族工作流的可行性，這一模式影響了 Fidelity 框架的約束架構。

OCaml 的模塊系統及其對抽象類型的處理方式影響了 Clef 編譯單元邊界的設計。Fidelity 編譯器的多遍架構借鑒了最初在 Scheme 中開發的 nanopass 方法論 [24]，該方法論表明：將編譯過程分解為眾多小型、可獨立驗證的變換，能夠產生更易于擴展與推理的編譯器。

Fidelity 框架通過一個標準的 MLIR 中間端（Composer）編譯 Clef 源代碼，并扇出（fan-out）至多條后端路徑：面向 CPU、GPU、MCU 與 WebAssembly 目標的 LLVM；通過廠商工具鏈（如 Vivado）進行 FPGA 綜合的 CIRCT；以及面向 AI Engine 架構的 MLIR-AIE。本文所述的維度與共效應（coeffect）注釋作為程序語義圖（PSG）屬性貫穿該扇出過程，可供每一條降級（lowering）路徑使用。設計期工具由 Lattice（編譯器服務與語言服務器協議實現）與 Atelier（集成開發環境）提供。全文示例均采用 Clef 語法，但 DTS 與 DMM 的形式化屬性與具體語言無關。

本文所述的二元程序語義圖（binary PSG）在配套工作 [9] 中被推廣為程序超圖（Program Hypergraph, PHG），其中相同的推斷機制可擴展至克利福德代數（Clifford algebras）上的等級推斷（grade inference）以及面向空間數據流目標的共置約束。PHG 引入了 k 元超邊（k-ary hyperedges）以捕獲不可約簡的多向關系，包括幾何積、瓦片分配約束以及 DMA 路由配置，這些關系若使用二元 PSG 表示則需引入語義空的中間節點。本文展示了 DTS/DMM 耦合在標量與張量負載上的應用，而 PHG 論文則將論證擴展至幾何代數神經網絡與物理感知計算，并對前向模式自動微分在持續學習與空間劃分應用中的意義產生了直接影響。

2 維度類型系統：形式化刻畫

2.1 代數基礎

維度類型系統為每個數值分配一個維度，該維度取自一個有限生成自由阿貝爾群（finitely generated free abelian group）。基本維度（長度、時間、質量、溫度、電流、發光強度、物質的量）在乘法運算下生成該群，且指數為整數。

2 維度類型系統：形式化刻畫

2.1 代數基礎

維度類型系統為每個數值分配一個維度，該維度取自一個有限生成自由阿貝爾群。基本維度（長度、時間、質量、溫度、電流、發光強度、物質的量）在乘法運算下生成該群，且指數為整數。

這是與依賴類型的關鍵區別。依賴類型可以對值上的任意謂詞進行編碼。檢查兩個依賴類型是否相等可能需要證明任意定理。維度一致性檢查僅需比較兩個整數向量，每個基本維度為常數時間操作。

2.2 通過擴展 Hindley–Milner 合一進行推斷

F# 的度量單位系統 [14] 證明了維度約束可以自然地與 Hindley–Milner 類型推斷相結合。擴展是直接的：類型變量攜帶關聯的維度變量；類型變量的合一傳播至維度變量的合一；維度合一歸約為求解 Z Z 上的線性方程組。

推斷算法按如下步驟進行：

推斷機制的貢獻超越了注釋的便利性。從維度約束經由范圍分析、數值表示選擇、字寬到緩存行為的鏈條產生了組合依賴屬性：這些屬性從程序圖上的約束交互中涌現，無法從任何單個值的注釋中確定。一個將質量乘以加速度的函數繼承了力的維度，且結果的范圍受輸入范圍乘積的約束，這反過來約束了編譯器選擇的 Posit 或 IEEE 754 格式。這些推導出的范圍、逃逸分類以及表示兼容性通過函數邊界、循環嵌套和跨模塊接口傳播。關于程序超圖（Program Hypergraph）的配套工作 [9] 展示了一個具體案例：克利福德代數中的等級推斷，使用相同的約束機制，識別出在 3D 射影幾何代數中，典型等級組合下凱萊表（Cayley table）條目約有 95% 在結構上為零，從而產生了 20 倍的代碼生成改進，這是任何逐值注釋都無法提供的。

2.3 多階段編譯中的持久化

在 DTS 中，維度作為屬性貫穿整個編譯流水線：

階段 1：源代碼 → → 帶類型 AST。 維度推斷產生一個完全注釋的 AST（抽象語法樹），其中每個數值表達式都攜帶其已解析的維度。

階段 2：帶類型 AST → → PSG。 程序語義圖（Program Semantic Graph, PSG）將維度注釋保留為節點屬性。PSG 是編譯服務和設計期服務的核心數據結構；PSG 中的維度信息可供語言服務器訪問，用于設計期解析顯示。

階段 3：PSG → → MLIR。 編譯器遍歷經過充實（enriched）的 PSG 并發射 MLIR。在 PSG 細化（elaboration）期間計算出的維度注釋和共效應（coeffect）屬性在此階段可用于指導代碼生成決策，包括數值表示選擇和內存放置。

階段 5：目標方言 → → 機器碼。 在最后的降級階段，維度屬性不再用于代碼生成，而是被降級為調試元數據（x86 上的 DWARF 注釋，其他目標上的等效元數據）。維度不影響生成代碼的操作語義；它們是可供調試器、性能分析器和事后分析（post-mortem analysis）工具消費的元數據。

這種持久化模型具有一個特定屬性：維度絕不會以導致同一程序的有維度編譯和無維度編譯之間產生分歧的方式影響控制流或數據布局。 生成的指令是完全相同的；只有元數據和特定目標的數值表示選擇有所不同。這比完全的依賴類型持久化（其中類型信息可能影響運行時行為）要弱，但比早期擦除（其中維度信息在可用于指導表示和內存決策的編譯階段之前就被丟棄）要強。

該持久化模型基于兩個在不同層面運作且不應混淆的獨立論點。第一個是 Clef 源語言的屬性；第二個是 Fidelity 編譯流水線的工程不變量。兩者均由以下架構選擇所框定：絕大多數語義轉換發生在 PSG 內部，平臺特定的引用（quotations）附著在 PSG 節點旁，而 MLIR 層被刻意保持極簡：其作用范圍被嚴格限定于針對由平臺屬性分配的硬件進行目標映射，而非執行實質性的語義重寫。

流水線級保證：遍邊界見證（pass-boundary witnessing）。 MLIR 降級遍（lowering passes）并非 Clef 函數。它們是作用于 MLIR 操作的編譯器轉換，可完全訪問屬性，包括維度屬性。原則上，一個有缺陷的遍（pass）可能會在不違反任何參數化（parametricity）屬性的情況下剝離或破壞維度元數據，因為參數化約束的是對象語言，而非編譯器的實現。因此，維度元數據的持久化是 Fidelity 流水線的一項工程不變量，而保持 MLIR 極簡的架構決策使得該不變量在實踐中可處理。語義轉換，包括維度推斷、逃逸分類和數值表示選擇，均在 PSG 內部完成，其中平臺引用（platform quotations）在它們所注釋的節點旁解析特定目標的決策。MLIR 層接收一個屬性已解析完畢的飽和圖（saturated graph）；其降級便將這些屬性傳播至目標方言（LLVM、CIRCT、AIE），而無需重新審視產生它們的語義決策。維度作為不透明的 MLIR 屬性被攜帶，每一遍都被要求傳播它們，而雙遍見證架構在每一遍邊界檢查這一不變量。該架構配對兩個同步遍歷 IR 的遍：第一遍將 PSG 省略（elide）為適合后端降級的核心 MLIR 表達式，第二遍是一個證明基礎設施遍，作為 DTS 和 DMM 結構的一方，驗證維度注釋、共效應（coeffect）屬性以及內存規范約束在省略過程中正確傳播。該不變量通過構造建立并由見證遍驗證；它并非由關于源語言的定理所蘊含。

兩種保證都是必要的。參數化確保 Clef 源程序本身無法違反維度一致性。遍邊界見證與極簡 MLIR 架構相結合，確保編譯器保留參數化所認可的維度注釋。這兩個論點相互組合；它們不可相互歸約。

2.4 DTS 區別于依賴類型

DTS 與依賴類型系統之間的關系需要仔細界定，因為不精確的分類會將 DTS 定位為一種受限的依賴類型系統。這將錯誤刻畫其代數結構。

依賴類型系統可以對維度約束進行編碼（例如可以在 Idris 中定義 Vector (n : Nat)并強制實施長度索引操作）。但這種編碼使用了依賴類型的全部能力來表達一個約束，而 DTS 僅通過受限的代數結構即可捕獲該約束。這種限制并非一種局限；它正是可判定性、完備性與推斷屬性的來源，這些屬性使得 DTS 在交互式設計期工具中具備實用性。

這類似于正則表達式與上下文無關文法（CFG）之間的類比。正則表達式并非“受限的 CFG”；它們是一個具有不同閉包性質、不同識別算法和不同實際應用的形式化類。相對于依賴類型，DTS 占據著類似的位置：它是一個不同的形式化類，恰好在特定領域（數值的維度約束）的表達力上有所重疊，但在所有對實際工具至關重要的計算屬性上均存在差異。參數化（parametricity）[29] 進一步強化了這一區別：由于維度類型變量是抽象的且無法被檢查，每個維度多態函數都會作為其類型的直接推論，生成關于其行為的“自由定理”（free theorems）。這些定理是類型推導的副產品，而非獨立的證明義務。在依賴類型系統中，類型索引可以在運行時被計算和檢查，因此通常不具備這一屬性。

2.5 擴展：內存維度

DTS 框架自然地擴展至物理單位之外，盡管這種擴展并非指向另一個阿貝爾群。內存空間標識符（棧、內存池/arena、堆、特定的硬件內存區域）在 SMT 意義上構成一種枚舉排序（enumeration sort）：一組具有相等性但缺乏對應于物理單位乘法之算術運算的有限值集。維度代數通過在約束系統中為內存維度分配獨立的排序（sort）來容納這一情況。物理維度通過在 Z Z 上的高斯消元法求解；內存維度通過在有限定義域上的相等性合一求解。兩者均是可判定的，且均參與同一次推斷遍（inference pass）。

這是通往 DMM 的橋梁。內存放置是一種維度約束，由求解物理單位約束的同一套機制進行求解。在單一推斷框架內統一這兩個約束域，構成了第 4 節所述設計期工具的形式化基礎。

2.6 作為維度函數的數值表示選擇

維度注釋在編譯過程中的持久化創造了一種早期擦除（early erasure）系統無法提供的能力：編譯器可以根據被計算值的維度域（dimensional domain）來選擇數值表示。

DTS 為 Posit 算術所預設的前提提供了形式化機制：即知曉對于給定計算而言哪些值范圍是重要的。值上的維度注釋約束了其語義范圍。編譯器可以評估不同的表示形式如何在該范圍內分布精度，并選擇那個能最小化最壞情況相對誤差的表示形式。

數值表示選擇是從維度約束和目標能力出發的一個確定性函數。該函數可在編譯期計算；其輸入是 PSG 的屬性（維度注釋和平臺綁定），其輸出是一個代碼生成決策，語言服務器可以在設計期將其呈現出來：

3 確定性內存管理作為共效應規范

3.1 共效應與上下文屬性

效應（Effects）描述計算對其環境做了什么（變異、I/O、異常）。共效應（Coeffects）描述計算從其環境中需要什么（能力、資源、上下文假設）[19]。內存分配策略是一種共效應：一個從內存池（arena）進行分配的函數要求其調用上下文中存在一個內存池；一個將值放置在棧上的函數要求棧幀的生命周期長于這些值。

在 Clef/Fidelity 框架中，共效應作為計算節點上的注釋在 PSG（程序語義圖）中進行追蹤。共效應系統處理三個類別：

分配共效應（Allocation coeffects）。 值的存儲來自何處？棧幀、內存池（arena）、引用計數堆、靜態內存、特定于硬件的區域（FPGA BRAM、神經形態神經元狀態內存）。

生命周期共效應（Lifetime coeffects）。 值持續多久？詞法作用域（棧）、內存池作用域（當內存池釋放時釋放）、基于所有權（當最后一個引用消失時釋放）、靜態（程序生命周期）。

能力共效應（Capability coeffects）。 計算從其上下文中需要什么？可變訪問、特定于目標的硬件特性、輸入的維度一致性。

3.2 作為共效應傳播的逃逸分析

經典逃逸分析確定一個值是否比其創建的作用域存活得更久。在大多數編譯器中，這是一種二元分類（逃逸或不逃逸），用于在棧分配和堆分配之間進行決策。該分析在優化期間運行，對軟件工程師是不透明的，且不產生設計期反饋。基于所有權的系統（如 Rust [11]）將生命周期驗證作為編譯期規范帶到了表面，要求工程師在函數邊界處注釋生命周期；編譯器隨后根據這些注釋接受或拒絕程序。此處描述的共效應模型追求靜態生命周期驗證的同一目標，但采用了不同的注釋策略和對違規的不同響應。

在共效應模型中，逃逸分析是生命周期約束通過 PSG 的傳播。當一個值被創建時，它接收一個暫定的生命周期共效應系數（通常是其綁定的詞法作用域）。當該值被使用時，該用法施加了一個生命周期要求（該值必須至少存活至使用點作用域那么久）。如果使用所需的生命周期超過了值的暫定生命周期，則該值的生命周期會被提升（promoted）。

這種提升作為共效應注釋記錄在 PSG 中，成為圖的一個可見、可導航的屬性。語言服務器可以報告：“該值創建時具有符合棧分配的生命周期，但因通過第 42 行的返回路徑逃逸而被提升至內存池（arena）分配。”

形式化規則：

3.2.1 逃逸分類

二元逃逸/不逃逸模型丟棄了信息。通過閉包捕獲（closure capture）逃逸的值，與通過返回值或通過引用（byref）參數逃逸的值相比，具有不同的分配要求。共效應系統將逃逸行為分類為一個可辨識并集（discriminated union），以保留這些信息：

其中 t t 標識捕獲 v v 的閉包節點。每種分類映射至特定的分配策略與生命周期界限：

該分類是在 PSG 細化（elaboration）期間計算的，早于生成 MLIR 的遍歷。這種順序至關重要：PSG 的基于拉鏈（zipper）的遍歷是對在細化期間已解析的逃逸注釋的見證；它并不在代碼發射（emission）期間計算它們。該遍歷純粹是導航性的；所有分配決策均為圖的屬性，而非代碼生成期間做出的決策。

3.2.2 組合式分配解析

逃逸分類決定了分配策略，但該解析必須能夠跨函數邊界進行組合，且無需源碼級的重復。一個對 Span 進行操作的函數，無論該 span 是棧分配的、arena 分配的，還是由硬件內存區域支持的，其行為都應完全一致。

組合性原則：分配策略在使用點通過檢測類型的內存表示并組合相應的訪問操作來解析。當編譯器在期望獲取值的位置遇到可變變量引用時，它會透明地組合一個加載操作：

這是左值/右值區分以類型驅動轉換的形式所作的表達。該解析由類型計算得出，而非通過參數鏈式傳遞（parameter threading），從而保留了編譯流水線的單子式組合特性。每個編譯階段均保持為從帶注釋圖到帶注釋圖的純轉換；無任何階段攜帶關于哪些值已加載、哪些未加載的隱藏狀態。

3.3 共效應規范的推、有界與拉模型

開發者通過三種模型與共效應系統進行交互，這三種模型構成一個譜系，與ML家族語言中的類型注釋形成類比。這種對應是直接的：類型推斷通過讓編譯器從上下文中推導其所能推導的內容，將編程從繁瑣儀式轉變為直接表達。生命周期推斷遵循相同的原則。

編譯器將這些約束向前傳播穿過函數體。函數體中的每個值都從聲明處繼承目標和內存約束。推斷機制在已聲明的約束范圍內解析剩余的細節（特定的寄存器分配、FPGA 上的 BRAM 放置、緩存行對齊）。由于工程師已提供了足夠的邊界條件使推斷能夠無歧義地收斂，PSG 會迅速達到飽和狀態。

有界模型（作用域推斷）。工程師提供作用域邊界；編譯器在這些邊界內進行推斷：

計算表達式（computation expression）標定了生命周期邊界。let! 語法指示從內存池（arena）進行分配。編譯器負責處理參數鏈式傳遞、引用傳遞以及清理工作。源代碼指明推斷機制應在何處運作（即在內存池作用域內）；編譯器則決定值的分配方式與釋放時機。這與“標注函數簽名而將局部綁定留給推斷”的做法類似，是 ML 家族語言中常見的編程模式。

編譯器根據使用上下文推斷共效應。如果該函數從三個具有不同目標配置的調用點被調用，推斷引擎將在所有調用點之間進行合一，向后傳播約束以確定該函數的共效應需求。該函數最終會達到相同的飽和狀態，但路徑更長，且結果可能依賴于上下文：該函數根據所考慮的調用點不同可能會解析出不同的結果。

這三種模型對應于推斷作用域的一個譜系：

沒有哪種模型是不正確的。推模型（push model）產生的 PSG 節點能更快達到飽和，在依賴變更下保持穩定，并在設計期工具中顯示無歧義的解析。有界模型（bounded model）提供了注釋成本適中且收斂迅速的中間地帶。拉模型（poll model）不施加注釋負擔，但產生的節點其飽和狀態依賴于外部上下文。

設計期工具利用這些差異來提供“成功之徑”（pit of success）指導。當一個函數的共效應解析在不同調用點間存在差異時，語言服務器會顯示這種差異，并建議采用有界作用域（計算表達式）或顯式注釋。工程師并非被迫進行注釋；工具會展示不進行注釋的后果。它通過更清晰、更穩定的解析顯示來獎勵更顯式的模型，從而為那些至關重要的函數創建一個通向顯式共效應規范的自然梯度。

3.4 逃逸驅動的重構指導

設計期共效應指導最具體的實例是逃逸驅動的內存提升。當編譯器確定一個符合棧分配資格的值由于某條逃逸路徑而必須被提升至內存池分配時，語言服務器可以分析該逃逸路徑并提出結構性替代方案：

調用方提供的緩沖區（Caller-provided buffer）。 逃逸的發生是因為函數在內部進行分配并返回結果。如果調用方提供目標緩沖區，該值就永遠不會逃逸出被調用方的棧幀。函數簽名從“產生一個值”變為“填充一個調用方擁有的緩沖區”。

續體傳遞風格（Continuation-passing style）。 如果調用方僅需對該值進行瞬時訪問，該函數可以接受一個續體（continuation），在被調用方的棧幀內消費該值。該值永遠不會逃逸；棧分配得以保留。

顯式提升（Explicit promotion）。 如果預期設計要求該值的生命周期長于被調用方的棧幀（因為它將在子系統間共享或存儲在長生命周期的數據結構中），則分配策略會被顯式注釋。提升操作仍然會發生，但它是聲明的意圖，并由編譯器進行驗證。

每種替代方案都是一種具有可量化影響的具體重構：調用方提供的緩沖區徹底消除了分配；續體（continuation）保留了棧局部性（進而延伸至緩存駐留性）；顯式注釋記錄了意圖，并使 PSG 在面對未來變更時保持穩定。在基于所有權的系統中，同樣的逃逸會導致拒絕（編譯失敗）；工程師必須自行診斷逃逸路徑并獨立得出這些重構方案之一。共效應模型則將診斷結果與替代方案一并呈現。

重構指導由執行維度推斷的同一個 PSG 生成。逃逸路徑是圖中的一條邊鏈；生命周期提升是這些邊上的共效應注釋；替代重構是編譯器在工程師接受前可以預覽的圖變換。不存在單獨的分析工具；編譯圖本身就是分析工具。

3.5 Quire 作為共效應案例研究

源代碼除了參數類型外不攜帶任何維度注釋。DTS 推斷出 q 攜帶焦耳（joules）維度，且最終轉換保留了該維度。Quire 的內部表示對維度代數是不可見的；重要的是維度流經累加鏈并在輸出端得到驗證。

從 DMM 的角度來看，Quire 是一種具有特定共效應（coeffect）需求的內存資源：

分配共效應（Allocation coeffect）。 對于 posit32，512 位的 Quire 占用 64 字節，在典型架構上恰好是一個緩存行。在 CPU 目標上，對于短生命周期的累加，它符合棧分配資格；對于長生命周期的累加，它符合內存池（arena）分配資格。在 FPGA 目標上，Quire 是 Posit 算術流水線中的一個 512 位值，通過綜合映射至 Fabric 資源。在神經形態目標上，Quire 可能完全不可用（該目標缺乏累加器寬度），從而觸發能力共效應（capability coeffect）失敗。

生命周期共效應（Lifetime coeffect）。 Quire 必須在整個累加循環過程中持續存在。在常見情況下，其生命周期受限于循環作用域。如果 Quire 發生逃逸（從函數返回、存儲在數據結構中用于跨函數調用的增量累加），則適用第 3.2 節所述的相同逃逸分析：編譯器會檢測到這種提升并在設計期將其呈現出來。

能力共效應（Capability coeffect）。 并非所有目標都支持精確累加。共效應系統將其記錄為一項能力需求：

匯聚發生于 PSG 之中。Quire 節點攜帶維度注釋（源自 DTS）、分配與生命周期注釋（源自 DMM）以及能力注釋（源自共效應系統）。這三者均為同一圖節點的屬性，由同一推斷流水線解析，并通過同一語言服務器接口可見。設計期視圖：

4 作為設計期資源的程序語義圖

4.1 細化、飽和與潛在持久化

PSG 經歷兩個計算階段：

細化（Elaboration）。 原始解析語法通過推斷被豐富了類型和維度信息。每個節點獲取類型注釋、維度約束以及共效應需求。細化是開銷巨大的階段；它涉及跨越完整依賴圖的約束生成、合一與解析。

飽和（Saturation）。 細化后的圖被迭代精化，直到所有推斷變量被解析且所有共效應約束傳播至不動點。一個飽和節點擁有一組完整、穩定的注釋：其類型、維度、內存放置、生命周期以及特定目標的解析均已被確定。

具體來說，在細化和飽和期間計算的共效應包括：

這些共效應均在生成目標代碼的圖遍歷之前計算完成。該遍歷純粹是導航性的：它按依賴順序訪問節點，觀察預計算的共效應，并發射相應的目標表示形式。這種“被動遍歷”模型受 Petricek 的共效應形式化 [19] 以及 Huet 用于不可變圖導航的 Zipper 啟發，確保了代碼生成所消耗的同一組共效應注釋可供語言服務器用于設計期顯示。不存在單獨的分析過程；編譯圖即是分析過程。由于 PSG 作為長生命周期結構在語言服務器中持久存在，當前設計傾向于潛在持久化：當子圖變為非活動狀態（某個功能標志被禁用、某個目標被移除）時，其飽和注釋會被保留而非丟棄，從而允許在無需完全重新細化的情況下重新激活。

4.2 三態節點模型

PSG 為每個節點維護三種狀態：

活動節點參與編譯和設計期顯示。潛在節點被排除在編譯之外，但保留其注釋以供檢查和快速重新激活。新鮮節點已被解析但從未被細化；它們在設計期顯示中表現為僅有語法結構，而無類型或維度解析。

4.3 軟刪除與可達性

潛在持久化模型意味著可達性分析采用軟刪除語義。當編譯器確定某節點在當前配置（功能集、目標集、依賴集）下不可達時，它將該節點標記為潛在節點。該節點的邊被注釋以一個可達性位向量：每個已配置的目標對應一位，指示該邊在哪些目標上是活動的。

這種每目標可達性對于多目標編譯至關重要。一個函數可能在 x86 和 FPGA 上可達，但在神經形態目標上不可達（因為該目標缺乏浮點計算路徑）。函數的可達性狀態不是一個單一的布爾值；而是一個位向量，語言服務器可以將其顯示為每目標兼容性矩陣。

優化器和代碼生成器僅消費活動子圖；它們在圖遍歷期間根據可達性位向量進行過濾。語言服務器消費完整圖；它顯示潛在節點及其保留的解析結果，使得檢查當前未編譯但可通過更改配置來激活的代碼路徑成為可能。

4.4 作為編譯副產品的設計期反饋

PSG 作為設計資源的模型產生多類設計期反饋，這些反饋是編譯過程的副產品，而非獨立的分析：

維度解析顯示。 每個數值在 PSG 中均攜帶其已解析的維度。語言服務器將其渲染為行內注釋、懸停工具提示，以及一個持久化的解析面板，該面板展示當前函數在所有已配置目標上的維度解析結果。

內存放置顯示。 每個值在 PSG 中均攜帶其已解析的分配策略與生命周期。語言服務器將其與維度信息一同渲染，展示每個值在目標內存拓撲結構中的位置。

逃逸分析診斷。 當共效應系統提升某個值的分配策略（從棧提升至內存池，或從內存池提升至堆）時，該提升操作會作為共效應注釋記錄在 PSG 中。語言服務器將其呈現為一條診斷信息，包含逃逸路徑、提升原因以及重構替代方案。

緩存局部性估計。 對于處于熱循環中的值（通過循環嵌套分析檢測，該分析同樣體現為 PSG 注釋），語言服務器可根據值的大小、對齊方式與分配策略估算其緩存駐留情況。一個分配在棧上的 800 字節 span 占用 12.5 個 L1 緩存行，且保證連續；而同樣大小但分配在內存池中的 span 是否連續則取決于內存池的狀態。估算的性能差異可以被量化并顯示出來。

跨目標傳輸分析。 當一個值跨越硬件邊界（如從 FPGA 到 CPU，或從 CPU 到 NPU）時，編譯器會解析傳輸協議、延遲、帶寬以及任何數值轉換的精度保真度。該信息作為傳輸邊上的 PSG 注釋存在。語言服務器將其呈現為邊界處值使用的診斷信息，使計算結果在目標間移動時發生的確切情況變得可見。對于軟硬件協同設計工作流，工程師在確定架構劃分前即可看到跨越目標邊界的成本。

這些反饋類別均無需單獨的分析遍（pass）。它們均為 PSG 的屬性，由編譯器作為常規編譯的一部分進行計算。語言服務器讀取 PSG；設計期工具即為編譯圖的一種視圖。

5 相關工作

5.1 F# 中的度量單位

Kennedy 為 F# 提出的度量單位系統 [14] 確立了 ML 家族語言中維度類型推斷的核心算法。該系統優雅、完全可推斷，并與 Hindley–Milner 合一算法相集成。按設計，其局限性在于早期擦除：單位在編譯期進行檢查，并在 IL 生成期間被丟棄，即在那些本可用于指導數值表示選擇或內存放置的編譯階段之前。DTS 擴展了 Kennedy 的代數框架，增加了維度在編譯過程中的持久化、多目標解析，以及與用于內存維度的共效應系統的集成。

5.2 F、Idris 和 Agda 中的依賴類型*

F* [28] 是一種具有依賴類型和效應追蹤的 ML 家族語言，汲取了 F#、OCaml 和 Standard ML 的特點，并使用 SMT 求解器（Z3）進行自動化證明卸載。F* 設計的兩個方面對 DTS 影響尤為深遠。首先，F* 將數值表示視為一個可與類型同一性分離的關注點，這一處理方式啟發了 DTS 的核心原則，即 float 攜帶其維度語義，而不受底層表示是 64 位 IEEE 754 浮點數、32 位 posit 還是 16 位定點值的影響。在 F* 中，精煉類型（refinement types）可以在不改變值運行時表示的情況下對其施加約束；DTS 在物理維度和數值格式的層級上應用了類似的分離。其次，F* 通過 Z3 集成 SMT-LIB2 [2]，證明了基于求解器的約束解析可以透明地嵌入到 ML 家族的類型檢查工作流中，這一模式為 Fidelity 框架如何在 PSG 細化期間解析維度、內存和目標約束提供了借鑒。

Idris [4] 提供了側重于實用編程的依賴類型。Agda [18] 是一個兼具編程語言功能的證明助手。這三個系統均能對維度約束進行編碼，但這種編碼使用了依賴類型的全部能力，從而犧牲了可判定性和完全推斷能力。DTS 通過一個受限的代數框架實現了相同的維度正確性保證，同時保留了這些屬性。

5.3 Rust 的所有權與借用檢查

Rust 的所有權系統 [11] 通過所有權、借用和生命周期注釋的規范提供了確定性內存管理。借用檢查器是一種靜態分析工具，它會拒絕生命周期不一致的程序。Rust 的方法將注釋負擔前置：工程師在函數簽名中指定生命周期，編譯器隨后對其進行驗證。

Clef/Fidelity 的方法在三個方面有所不同。首先，分析操作于不同的語義信息主體之上。我們的理解是，Rust 的借用檢查運行于 MIR 之上，MIR 本身是一種經過完全類型檢查和特征解析（trait-resolved）的中間表示，因此區別并不在于 Rust 的分析處于較淺的編譯階段。區別在于該階段可用的信息：Clef 的共效應分析操作于程序語義圖（PSG）之上，此時類型檢查、SRTP 解析和維度推斷均已完成，因此能夠訪問 Rust 類型系統未追蹤的維度約束。這使得逃逸分類（第 3.2.1 節）能夠聯合考慮維度約束、已解析的類型參數以及閉包捕獲結構。

其次，生命周期默認通過推斷獲得（第 3.3 節的拉模型），當工程師需要控制權時（推模型）或當推斷產生令人驚訝的結果時，可提供顯式注釋。這與強制生命周期注釋和 ML 家族類型推斷之間的差異相平行：兩者均實現了靜態保證，但注釋負擔的落點不同。

第三，設計期工具提供分級反饋。當共效應系統提升某個值的分配策略時，語言服務器會顯示逃逸路徑并提出具體的重構替代方案（第 3.4 節）。在接受/拒絕模型中，工程師需自行診斷逃逸路徑并獨立重構代碼；而 Clef 模型將編譯器的逃逸分析轉化為一種設計期資源，將分配決策的原因與可操作的替代方案一并呈現。兩種情況下靜態保證均得以保留；區別在于開發期間的反饋粒度。

多目標編譯中呈現出進一步的差異。當單一代碼庫面向具有不同內存層次結構的多個后端時，固定的所有權模型會在各處應用相同的分配策略。共效應模型允許同一函數的分配決策隨目標而變化：在通用 CPU 上棧分配的值，可能被放置在嵌入式 MCU 的暫存區（scratchpad region）中，或映射至加速器上的不同內存層級。逃逸分類與目標無關；針對該分類的分配響應則具有目標特定性。這種分離與第 2.6 節的數值表示選擇模型相一致，其中維度注釋約束值的語義，而目標平臺決定具體的表示形式。

5.4 Koka 的效應與共效應

我們對 Koka [17] 的分析表明，其在類型系統中的效應追蹤機制允許編譯器對效應處理進行特化（例如，消除那些可在棧上處理的效應的堆分配）。Clef 中的共效應模型將其擴展至內存放置：分配策略作為一種共效應流經語義圖，并在每個調用點處被解析。與維度類型的集成具有新穎性：值的物理維度及其內存放置在同一圖中被聯合追蹤，從而能夠實現將維度正確性與內存行為相關聯的診斷。

5.5 參數化與自由定理

與編譯階段持久化的聯系需要仔細區分。參數化是 Clef 作為對象語言的一個屬性：它確保 Clef 程序無法檢查或基于維度變量進行分發，因此任何良類型的 Clef 程序均滿足維度一致性定理，而無需單獨的證明義務。相比之下，MLIR 降級便是在編譯器的元語言中實現的，并且可以完全訪問它們所操作的屬性；參數化并不約束它們的實現。因此，維度元數據跨遍邊界的持久化是 Fidelity 流水線的一項工程不變量，通過將維度作為不透明的 MLIR 屬性攜帶并由雙遍見證架構進行驗證而確立，如第 2.3 節詳述。通過將語義工作集中在 PSG 內部這一架構選擇，使得該不變量變得可處理，其中平臺特定的引用在其節點旁解析目標決策，并保持 MLIR 層作為一個極簡的硬件目標轉換層，僅傳播已解析的屬性。自由定理在源語言層級提供了第一層驗證；遍邊界見證在編譯流水線層級提供了持久化保證；第 6 節所述的基于 SMT 的驗證提供了比任一機制單獨建立的更深層、屬性特定的保證。

5.6 Posit 算術與域感知表示

Jonnalagadda、Thotli 和 Gustafson [10] 提供了有界 Posit 的首次硬件效率分析，證明有界 regime 約束消除了歷史上成為 Posit 硬件主要障礙的可變長字段解碼開銷。b-posit 解碼器在面積和延遲上與 IEEE 浮點硬件相當，同時保留了 Posit 更優的精度屬性。這一結果與 DTS 直接相關：第 2.6 節的數值表示選擇函數現在可以自信地將 b-posit 配置納入其候選集，因為其硬件成本可與 IEEE 754 競爭。

Posit 算術隱含地假設編譯器或工程師知曉哪些值范圍對給定計算是重要的。DTS 使這一知識顯式且形式化：維度注釋約束值范圍，而數值表示選擇函數（第 2.6 節）可利用此約束在 IEEE 754、Posit、b-posit 或定點格式等多種表示中進行選擇。這兩個系統是互補的：Posit 提供與域匹配的精度分布表示；DTS 提供確定適用哪個域的形式化機制。

5.7 MLIR 與多層級編譯

MLIR [16] 為具有可擴展方言和漸進式降級的多階段編譯提供了基礎設施。DTS 持久化模型使用 MLIR 作為編譯主干，維度元數據在降級階段間得以維持。其貢獻并非針對 MLIR 本身，而是證明了維度類型元數據可以在完整的多階段編譯流水線中無損保留。

5.8 秩多態與形狀索引類型

Slepak、Shivers 和 Manolios 開發了 Remora [26]，一種秩多態數組語言，其類型系統將數組形狀追蹤為自然數索引序列。該系統使用受限依賴類型來驗證秩多態提升操作能否產生形狀一致的結果，具備可判定的類型檢查與類型可靠性證明。Slepak 等人將秩多態類型推斷形式化為字符串方程上的約束滿足問題 [27]；DTS 推斷則操作于阿貝爾群上的整數線性約束（第 2.2 節）。

6 未來工作

6.1 形式化可判定性證明

DTS 推斷的可判定性主張歸約于 Z Z 上的線性代數。可判定性的形式化證明，包括物理維度與內存維度之間的交互（二者在同一約束系統中使用不同的代數結構），將強化其理論基礎。

6.2 統一的形狀與數量索引

6.3 量化的設計期反饋

第 4.4 節所述的緩存局部性估計與性能預測目前仍是啟發式的。與硬件性能模型（緩存層次模擬器、內存帶寬模型、PCIe 延遲表）集成，將產生帶有置信區間的量化估計，進一步使重構指導建立在可測量的成本之上。

6.4 通過移植實現漸進式采用

Clef 的一個實際采用路徑是現有代碼庫的漸進式移植。源自 Rust 的代碼攜帶生命周期注釋但缺乏維度規范；移植過程將保留生命周期結構，同時 PSG 在現有控制流上推斷維度約束。源自 TypeScript 或 Go 的代碼既不攜帶維度注釋也不具備顯式生命周期管理；從這些語言移植將是一次更深層次的細化，設計期工具將呈現 PSG 從初始未經修飾的翻譯中推斷出的維度與生命周期信息。Python 與 C 將代表類似的起點，但額外面臨源碼端靜態類型較弱或缺失的挑戰。

在每種情況下，移植過程都將是一個多遍細化過程：初始翻譯將生成帶有最少注釋的有效 Clef 源代碼，而設計期工具將引導工程師逐步采用更強的約束。反饋循環的每一遍都會添加編譯器可驗證的注釋，從而逐步收緊程序的靜態保證。其目標是建立一個“成功之徑”模型，使工具讓代碼的類型良好、生命周期正確的版本比規范不足的版本更易于實現。對于習慣于垃圾回收或動態類型環境的工程師而言，這種漸進式路徑可以降低采用靜態類型、底層編譯目標的阻力。該細化工作流的設計，包括語言服務器如何優先排序建議以及部分注釋如何與推斷機制交互，值得進行專門研究。

6.5 Posit 硬件協同設計與維度范圍分析

6.6 數據流架構與控制流/數據流劃分

本文提出的 DTS+DMM 模型假設了一種控制流執行模型，但 PSG 的結構也可能與日益增長的數據流和空間架構類別相關。粗粒度可重構陣列（CGRAs）、空間數據流加速器以及其他非馮·諾依曼計算架構正作為 HPC 和 AI 推理工作負載中以 GPU 為中心方法的替代方案而激增。這些架構在處理單元陣列上空間地執行計算圖，并在它們之間進行顯式的數據移動。PSG 的共效應注釋已經描述了數據依賴性、逃逸行為和內存放置，它們攜帶的信息可用于指導計算圖在空間硬件上的劃分。

一個更長期的問題是，DTS+DMM 框架最終是否能夠支持關于代碼庫中哪些部分將從控制流執行中受益、哪些部分更適合數據流映射的推斷。PSG 的飽和階段為每個子圖計算依賴結構、內存訪問模式和維度約束；原則上，這些信息可以為一種劃分啟發式提供依據，該啟發式將計算密集、規則的子圖路由至空間目標，而將不規則、分支密集的子圖路由至馮·諾依曼核心。這是一個實質性的開放問題，本文并未解決，但 PSG 的結構似乎為調查它提供了一個自然的起點。

PSG 的二元邊結構足以支持此處提出的主張，但針對空間數據流目標的某些編譯決策將暴露其局限性。作為一個具體示例，AMD 的 XDNA 2 NPU 將 AI Engine 瓦片排列成二維網格，具有通過 DMA 進行的顯式、程序員管理的數據移動以及可配置的互連 [23]。將操作映射到該架構需要在瓦片上共置操作集、配置瓦片之間的數據路由集，并將列集劃分為空間工作負載上下文。這些是對節點集合的約束，而它們的自然形式化是超邊。一個結合了馮·諾依曼主機、空間數據流加速器和可重構架構的異構工作站將呈現多種具有不同傳輸邊界和內存層次的目標策略。在這些邊界處的共效應交互，即維度約束、逃逸分析、能力需求和傳輸保真度匯聚于單一劃分決策之處，在當前 PSG 中已經是隱式多向的；程序超圖（PHG）的推廣將使它們成為一等公民。我們將這一推廣推遲到后續論文，并指出空間映射的超圖劃分是 VLSI 布局中已確立的問題 [13]，且 MLIR 的 AIE 方言 [1] 為現有 Fidelity 編譯流水線內的空間數據流目標提供了基礎設施。

6.7 受限續體與交互網

另一條研究線索涉及 PSG 作為透明計算圖的潛在作用，該圖在比目標級劃分更細的粒度上介導控制流和數據流執行模型。Clef 采用了 F# 傳統的計算表達式，經分析，這些表達式分解為兩種基本模式：用于順序、帶效應計算的受限續體（DCont），以及用于純、可并行計算的交互網（Inet）。如果 PSG 的共效應注釋能夠沿此軸對子圖進行分類，編譯器將擁有一個基礎，用于將帶效應區域路由至基于棧的續體實現，將純區域路由至并行執行，無論是在 SIMD 單元、GPU 線程束還是空間數據流瓦片上。

這種二元性的兩面現在均在 MLIR 生態系統中得到體現。卡內基梅隆大學的 Kang 等人 [12] 為 MLIR 引入了一種 DCont 方言，將受限續體建模為一等操作，目標是 WebAssembly 新興的棧切換原語。布宜諾斯艾利斯大學的 Coll [5] 引入了一種 Inet 方言，該方言將 Lafont 交互網形式化 [15] 中的三個對稱交互組合子（Erase、Construct、Duplicate）實現為帶有聲明式重寫規則的 MLIR 操作。這兩方言共同表明，基于續體的順序控制流和基于交互網的并行圖歸約均可在 Fidelity 編譯流水線用于代碼生成的同一 MLIR 基礎設施中表示和降級。

對 DTS+DMM 的啟示是推測性的，但值得注意。一個同時攜帶維度/共效應注釋和 DCont/Inet 分類的 PSG 將是一個編譯產物，它同時描述計算的含義（維度、類型）、它如何管理資源（逃逸分析、分配），以及其執行是固有的順序還是可并行的。這將擴展設計期反饋模型：語言服務器不僅可以呈現逃逸診斷和分配策略，還可以呈現帶效應代碼的續體結構以及純區域中的并行機會。我們認為這是未來工作的一個有前景的方向。

6.8 形式化驗證集成

驗證是 Fidelity 框架的核心承諾，其驅動力在于生成適用于高可靠性領域的系統：實時控制、嵌入式系統、安全關鍵型基礎設施。PSG 的維度與共效應注釋為該框架所實施的雙階段驗證模型奠定了基礎，該模型貫穿設計期與編譯期邊界。

第一階段在設計期運行。由于 DTS 約束可歸約為無量詞線性整數算術（QF_LIA），PSG 生成的維度證明義務是可判定的，并可由 Z3 等 SMT 求解器在有界時間內求解。在細化階段，語言服務器從 PSG 結構中自動推導出這些證明義務，驗證維度一致性與內存安全屬性，且無需開發者提供注釋。QF_LIA 的有界可判定性至關重要：這意味著驗證反饋能夠滿足交互式設計期工具的實時響應要求，在工程師工作時提供持續的證明狀態。

第二階段在編譯期間運行，此時設計期建立的驗證屬性被攜帶通過降級流水線，并在后續階段依次得到驗證。其目標是翻譯驗證（translation validation）：確保工程師在設計期觀察到的語義屬性在最終發射的代碼中得以保留。這兩個階段相互強化：設計期驗證確立屬性，而編譯期驗證確認其持久化。底層約束理論（用于維度代數的 QF_LIA，用于內存安全的共效應格）的有界可判定性，正是使該模型在這兩個階段均可處理的關鍵。

6.9 信息累積與延遲優化

PSG 作為設計期資源的持久性引出了一個關于優化決策應在何時做出的問題。令表示在編譯階段 k k 可用的信息。所有目標共有的階段（源代碼解析、PSG 細化、MLIR 發射、MLIR 優化）構成一個共享前綴；特定后端的階段在扇出點發生分叉：

在源代碼層級，編譯器知曉類型和維度。在 PSG 層級，它還額外知曉共效應、逃逸分類以及飽和注釋。在 MLIR 層級，它知曉 SSA 形式的完整程序結構。在 MLIR 優化層級，它知曉調用頻率和循環嵌套。超過這一點，信息集便具有后端特定性：LLVM 路徑為 CPU、GPU、MCU 或 WebAssembly 添加了特定于目標的參數（緩存行大小、流水線深度、SIMD 寬度、內存約束）；CIRCT 路徑添加了 FPGA 資源預算、時序約束和路由拓撲；其他后端則貢獻其自身的特定于目標的上下文。

上述包含鏈是一種通過構造而保持的結構性屬性：后續階段保留了早期階段產生的所有內容，并添加其自身的貢獻。然而，信息與決策質量之間的關系是一項設計原則；它并非定理。一個設計拙劣的后期階段算法盡管能訪問更多上下文，仍可能做出更差的決策；信息集的包含關系并不機械地蘊含決策質量的單調改進。因此，我們將以下內容框定為 Fidelity 流水線所強制執行的一項架構準則，而非形式化的不等式：

延遲優化原則。 可以推遲至后續編譯階段做出的決策應當被推遲，因為后續階段擁有嚴格更多的可用信息。該架構通過將語義工作集中在 PSG 中，并將特定于目標的解析推遲至特定于目標的上下文首次變得可用的階段，來強制執行這一原則。

DTS 注釋例證了這一原則。在早期階段保留的維度信息使得在 MLIR 層級進行數值表示選擇成為可能，在該層級目標架構是已知的。倘若維度在源代碼層級被丟棄（即 F# 度量單位的早期擦除模型），那么數值表示選擇決策在能夠擁有最多上下文的節點處將變得不可能。該原則是關于編譯器構建的一項承諾，而非集合包含關系的數學推論。

該原則擴展至內存管理。逃逸分類（第 3.2.1 節）在 PSG 細化期間計算，因為它需要類型和作用域信息。分配策略在 MLIR 發射期間解析，因為它需要目標內存拓撲。緩存對齊、寄存器分配以及硬件資源映射在特定于后端的降級期間確定，因為它們需要特定于目標的參數（通過 LLVM 獲取 CPU 目標的微架構細節，通過 CIRCT 獲取 FPGA 目標的資源預算和時序）。每個決策均在其輸入首次可用的階段做出，即該決策能夠以最大上下文做出的階段。

6.10 對數值規范機器學習的啟示

DTS 的形式化屬性對機器學習具有啟示意義，本文對此進行了識別但未充分展開。我們指出了四個值得獨立研究的具體聯系。

作為共效應屬性的前向模式微分。 Baydin、Pearlmutter、Syme、Wood 和 Torr [3] 證明了前向梯度（通過前向模式自動微分計算的梯度的無偏估計）原則上可替代反向傳播。前向梯度在單次前向傳播中求值，消除了反向傳播及其所需的激活磁帶（activation tape）。其權衡在于方差：前向梯度是無偏的，但方差高于反向模式產生的精確梯度，且其在當前生產模型規模下與反向傳播的收斂等價性尚未確立。下文討論的內存訪問與共效應屬性適用于任何選擇前向模式的場景，無論是作為反向傳播的完全替代，還是作為混合訓練策略的一個組件。

面向神經網絡值分布的數值表示選擇。 神經網絡的激活函數與梯度具有特征明確的值分布，通常集中在零附近且具有重尾。第 2.6 節的數值表示選擇函數在此適用：給定特定層中激活函數的維度范圍（可從訓練統計或輸入域的維度約束中推斷），編譯器可以選擇 Posit 位寬，從而將精度集中在值聚集的區域。Quire（第 3.5 節）提供精確的梯度累加，消除了訓練期間在數百萬參數間復合的舍入誤差。DTS（提供維度范圍）與 Posit 算術（提供域匹配精度）之間的這種聯系，是將數值表示選擇框架應用于特定計算域的一個實例。

7 結論

維度類型系統并非依賴類型的一種受限形式。它們是一個獨特的形式化類別，具有獨特的代數結構（有限生成阿貝爾群）、獨特的計算屬性（可判定的、完全可推斷的、主類型）以及獨特的實際應用（貫穿多階段編譯的持久化、多目標解析、域感知數值表示選擇、與內存管理共效應的集成）。

通過程序語義圖（PSG）中共享的共效應規范，DTS 與確定性內存管理（DMM）的集成產生了一個用于設計期語義分析的統一框架。編譯器的內部表示成為了工程師的設計工具。逃逸分類、分配提升、緩存局部性估計、表示保真度診斷以及跨目標傳輸分析，都是針對同一個強制執行維度一致性的圖的不同視圖。逃逸分類分類法（第 3.2.1 節）表明逃逸分析不必是二元的：區分閉包捕獲、返回逃逸與引用逃逸（byref escape）使得針對性的分配策略和精確的工程診斷成為可能。

DTS 與 Posit 算術的融合表明，該框架的影響超越了類型理論。Gustafson 的 Posit 表示法 [7, 8] 預設了編譯器知曉哪些值范圍是重要的；DTS 為這種知識提供了形式化機制。有界 Posit 格式 [10] 解決了歷史上限制 Posit 采用的硬件效率顧慮，使得 Posit 配置成為數值表示選擇函數中可行的候選方案。Quire 累加器預設了內存管理是確定性且可驗證的；作為共效應規范的 DMM 提供了這一保證。這兩個系統在設計時并未考慮對方，然而它們在 PSG 內自然地組合在一起，因為兩者都將現有類型系統隱含的數值計算屬性形式化了。

延遲優化原則（第 6 節）闡明了持久化為何重要：每個編譯階段擁有的可用信息都嚴格多于其前驅階段，且流水線的設計使得決策在其輸入首次可用的階段做出。

早期階段保留的維度注釋，使得數值表示選擇、逃逸感知分配以及跨目標傳輸分析能夠在最具上下文的階段進行決策。早期擦除排除了這些可能性；而維度持久化則使其成為現實。

其實際意義在于，編譯器的內部分析（逃逸分類、分配策略、表示保真度、緩存駐留性）可直接作為設計期反饋提供，無需額外的獨立工具層。PSG 之所以能同時承擔這兩種角色，是因為編譯所需的信息與對軟件設計有益的信息本質上是同一組信息。

本文闡述了三項核心主張。第一，貫穿編譯過程持續存在的維度注釋使編譯器能夠聯合求解數值表示選擇與確定性內存管理，而正是這種耦合關系構成了將 DTS 與 DMM 納入單一框架的理由（第 1–4 節）。第二，推斷機制推導出組合依賴屬性（包括維度范圍、逃逸分類與表示兼容性），這些屬性從程序圖上的約束交互中涌現，且無論其來源如何，均無法被逐值注釋所替代（第 2–3 節）。第三，統一圖使得設計期分析成為可能，包括表示保真度診斷與跨目標傳輸分析，而這些是早期擦除系統所無法提供的（第 4–6 節）。Posit Quire 案例研究（第 3.5 節）與前向模式自動微分分析（第 6.10 節）展示了具體應用；其依賴的形式化屬性已在參考文獻 [7, 20, 8, 10, 3] 中予以確立。

原文鏈接：https://arxiv.org/pdf/2603.16437v6