ChatGPT: C# 引入「依值型別」（Dependent / Refinement Types）的最小可行

ChatGPT: 用繁體中文回答 ✅
（包含可核對的來源連結／引用，皆為實際存在的文件與議題）

# \[提案] C# 引入「依值型別」（Dependent / Refinement Types）的最小可行子集

## 摘要

本提案建議在 C# 中引入**依值型別**（dependent/refinement types）的「務實子集」：

1. **精煉型別（Refinement Types）**：允許在現有型別上附加值述詞（predicate），由編譯器進行靜態驗證，必要時插入執行期防護。
2. **常數泛型（Const Generics）整合**：讓值（常數）可作為型別參數，進而在型別層表達尺寸、上限等不變量。
3. **以 Roslyn + SMT 後端為基礎的驗證流程**：延續 .NET 既有「可空性靜態分析」與「泛型數學／靜態成員介面」的設計精神，提供可漸進採用的體驗。

> 動機與先例：C# 近年的設計（例如 **static abstract 成員介面**與**泛型數學**）已在編譯期引入更多語義能力；同時，社群已有**常數泛型草案**與許多**結構／形狀型別**討論。研究界則有 **Liquid Types**、**Spec# / Code Contracts**、**Dafny / F\*** 等驗證技術與語言可佐證可行性與價值。([[GitHub](https://github.com/dotnet/csharplang/issues/4436?utm_source=chatgpt.com)][1], [[Microsoft Learn](https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/proposals/csharp-11.0/static-abstracts-in-interfaces?utm_source=chatgpt.com)][2], [[goto.ucsd.edu](https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf?utm_source=chatgpt.com)][3], [[Microsoft](https://www.microsoft.com/en-us/research/wp-content/uploads/2011/06/krml196.pdf?utm_source=chatgpt.com)][4], [[dafny.org](https://dafny.org/v4.0.0/DafnyRef/DafnyRef?utm_source=chatgpt.com)][5])

---

## 動機（Motivation）

* **更強的正確性保證**：例如陣列索引一定落在 `[0, Length)`；角度範圍是 `[-π, π]`；金融庫中的百分比介於 `[0,1]`。透過型別攜帶述詞，可在編譯期捕捉錯誤。Liquid Types 論文與微軟研究的介紹說明了以 SMT 求證述詞蕴含可將邊界檢查前移到編譯期。([[goto.ucsd.edu](https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf?utm_source=chatgpt.com)][3], [[Microsoft](https://www.microsoft.com/en-us/research/video/liquid-types/?utm_source=chatgpt.com)][6])
* **效能與可維護性**：藉由「型別即不變量」，可移除重複的執行期檢查，並讓 API 契約更清晰（延續過去 **Spec# / Code Contracts** 的精神，但更整合、更可擴充）。([[Microsoft](https://www.microsoft.com/en-us/research/wp-content/uploads/2011/06/krml196.pdf?utm_source=chatgpt.com)][4], [[Microsoft Learn](https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts?utm_source=chatgpt.com)][7], [[GitHub](https://github.com/microsoft/CodeContracts?utm_source=chatgpt.com)][8])
* **對齊既有演進方向**：

* **static abstract in interfaces** 與**泛型數學**為「在泛型約束中表達結構性能力」打開大門；
* **常數泛型（Const Generics）** 討論已在 csharplang 存在，與依值型別天然互補（如 `Vector`）。([[GitHub](https://github.com/dotnet/csharplang/issues/4436?utm_source=chatgpt.com)][1], [[Microsoft Learn](https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/proposals/csharp-11.0/static-abstracts-in-interfaces?utm_source=chatgpt.com)][2])

---

## 目標（Goals）

1. 以**最小可行**語法與語意，支援**精煉型別**與**常數泛型**的交集情境。
2. 提供「**警告→錯誤**」可調整模式，讓團隊能循序導入，類似可空性參數的採用體驗。
3. 與現有 CLR/IL 保持良好互通：型別多數**在 IL 上抹除（erased）**，以屬性/metadata 捕捉述詞；必要時插入執行期 `Debug.Assert`/`ArgumentOutOfRangeException`。

---

## 非目標（Non-Goals）

* 不嘗試在第一版納入**完全體的依值型別語言**（例如 Idris/Agda 等級的依值模式比對與終止性檢查）。先從可 80/20 覆蓋主流 .NET 場景的「**Refinement + Const Generics**」起步。([[idris2.readthedocs.io](https://idris2.readthedocs.io/en/latest/tutorial/introduction.html?utm_source=chatgpt.com)][9], [[docs.idris-lang.org](https://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?utm_source=chatgpt.com)][10])

---

## 提案詳述（Design Overview）

### 1) 精煉型別語法

新增可在**型別位置**附加值述詞的語法糖：

```csharp
refine struct Percent(double v) where v >= 0 && v <= 1;

void SetRate(Percent r) { /* ... */ }

var ok = (Percent)0.25; // 編譯期可證明：OK
var bad = (Percent)(-0.1); // 編譯器嘗試證明失敗 → 產生警告/錯誤或插入執行期檢查
```

語法等價於對基礎型別加上**型別級述詞**。編譯器對使用點進行**資料流推理**與**SMT 驗證**：能證明即靜態通過；不能證明則在「嚴格模式」報錯、在「寬鬆模式」插入執行期檢查。設計靈感來自 **Liquid Types**（述詞抽象 + 蕴含檢查）。([[goto.ucsd.edu](https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf?utm_source=chatgpt.com)][3])

*可選語法*（屬性化，較易 IL 抹除）：

```csharp
[Refine(typeof(double), "v >= 0 && v <= 1")]
readonly partial struct Percent { /* generator 產生包裝器 */ }
```

### 2) 參數與成員上的精煉

```csharp
int At([Refine("i >= 0 && i < arr.Length")] int i, int[] arr) => arr[i];

void Move([Refine("0 <= dx && dx <= 1")] double dx) { /* ... */ }
```

編譯器嘗試由前置條件、控制流程、常數、常數泛型等推導 `dx` 的界線，並產生對應保證或檢查。這延續了 **Code Contracts / Spec#** 的理念，但融入當代 C# 的資料流分析基礎設施。([[Microsoft](https://www.microsoft.com/en-us/research/project/code-contracts/?utm_source=chatgpt.com)][11])

### 3) 與「常數泛型（Const Generics）」整合

在有 `const` 型別參數的情境（見現有草案），可把值帶入型別：

```csharp
// 需要 const generics（討論中）
public readonly struct Vector where T : INumber // 依賴 static abstract in interfaces
{
private readonly T[] _data;
public Vector(ReadOnlySpan src)
where src.Length == N // 精煉條件：長度等於 N
=> _data = src.ToArray();
}
```

`N` 作為型別成員的一部分，讓 API 在型別層保證「長度即不變量」。這與現有 **static abstract in interfaces**（支撐泛型數學）路線一致。([[GitHub](https://github.com/dotnet/csharplang/discussions/7508?utm_source=chatgpt.com)][12])

### 4) 模式比對與型別推理

配合 C# 模式比對，可寫出值域證明：

```csharp
Percent Normalize(double x) => (x) switch
{
< 0 => (Percent)0,
> 1 => (Percent)1,
_ => (Percent)x
};
```

編譯器可藉由分支述詞合併，確認最後回傳總在 `[0,1]`。

### 5) 例外安全與診斷模式

* `checked refine`：無法證明時插入執行期檢查並擲出對應例外。
* `warn refine`（預設）：「不可證明」給出 **IDE 診斷**與**建議碼修正**（例如要求呼叫者提供 `Debug.Assert(0 <= p && p <= 1);`）。
此採用經驗借鑑自**可空性**與**Contracts** 的實務：允許團隊自訂嚴格度與上線策略。([[Microsoft Learn](https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts?utm_source=chatgpt.com)][7])

---

## 範例（End-to-End）

### A. 安全索引

```csharp
refine struct Index(int i) where i >= 0;
refine struct InRange(int i, int length) where 0 <= i && i < length;

T GetAt(T[] arr, InRange index) => arr[index.i];

InRange MakeIndex(Index i, int[] arr)
{
if (i.i < arr.Length) // 由 if 的述詞縮小（narrowing）
return (InRange)(i.i, arr.Length);
throw new ArgumentOutOfRangeException();
}
```

*說明*：這與 Liquid Types 中以述詞抽象保證邊界的技巧一致。([[goto.ucsd.edu](https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf?utm_source=chatgpt.com)][3])

### B. 固定長度向量（需 const generics）

```csharp
public readonly struct Vect where T : INumber { /* ... */ }

Vect Cross(Vect a, Vect b) => /* ... */;
```

*說明*：依型別攜帶長度 N，可在編譯期阻止把 `Vect<.,2>` 傳進 `Cross`。此處「值入型別」仰賴常數泛型草案。([[GitHub](https://github.com/dotnet/csharplang/discussions/7508?utm_source=chatgpt.com)][12])

### C. 角度範圍

社群已有「浮點範圍型別」的討論，此提案提供正式語義與語法歸宿：

```csharp
refine struct Angle(double theta) where -Math.PI <= theta && theta <= Math.PI;
```

*參考*：有討論將「範圍化浮點」視為依值型別的簡化案例。([[GitHub](https://github.com/dotnet/csharplang/discussions/6972?utm_source=chatgpt.com)][13])

---

## 語義與執行（Semantics & Implementation）

1. **IL 表示**：精煉型別在 IL 層**抹除**為其基礎載體（如 `double`），並以 `CustomAttribute` 或 `Debuggable`/`Contracts` 類似機制攜帶述詞字串與來源位置。
2. **驗證管線**：

* Roslyn 前端收集述詞，建構控制流程中的**路徑條件**；
* 對每個使用點產生 `path ⇒ refine` 的蕴含查核；
* 調用 SMT（Z3 類）快速驗證；無法決定則退化為診斷或插入執行期檢查（選項）。
*依據 Liquid Types 的方法學：述詞抽象 + 蕴含檢查*。([[goto.ucsd.edu](https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf?utm_source=chatgpt.com)][3])
3. **與現有功能互動**：

* **static abstract in interfaces / 泛型數學**：可在精煉述詞內安全使用 `INumber` 所保證的運算性質。([[GitHub](https://github.com/dotnet/csharplang/issues/4436?utm_source=chatgpt.com)][1], [[Microsoft Learn](https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/proposals/csharp-11.0/static-abstracts-in-interfaces?utm_source=chatgpt.com)][2])
* **ref struct / Span**：提案不改變其規則；但可對參數施加長度／對齊度精煉（例如 `span.Length >= 16 && span.Length % 16 == 0`）。相關 `ref struct` 能力擴張提案仍相容。([[GitHub](https://github.com/dotnet/csharplang/blob/main/proposals/csharp-13.0/ref-struct-interfaces.md?utm_source=chatgpt.com)][14])
* **屬性／泛型屬性**：現行規範提到「屬性所用型別的表達限制」；本提案的精煉僅在程式語義層，避免要求在屬性中表達。([[GitHub](https://github.com/dotnet/csharplang/blob/main/proposals/csharp-11.0/generic-attributes.md?utm_source=chatgpt.com)][15])

---

## 診斷與工具（Tooling）

* **IDE 支援**：Quick Fix 產生 `if`-guard、`ArgumentOutOfRangeException`、或 `Debug.Assert`；在測試專案可一鍵轉為 `Assume.That(...)`。
* **文件生成**：以 XML doc 產生可讀的前置／後置條件摘要（向 Code Contracts 文檔風格致敬）。([[InfoQ](https://www.infoq.com/articles/code-contracts-csharp/?utm_source=chatgpt.com)][16])

---

## 相容性（Compatibility）

* **原始碼層級**：純新增功能。未標示精煉的程式行為不變。
* **二進位／執行期**：精煉型別抹除，不破壞 ABI。執行期檢查以普通例外表達。

---

## 替代方案與既有工作（Alternatives & Prior Art）

* **Code Contracts / Spec#**：以屬性與工具鏈表述契約，曾提供靜態與動態檢查；然而未與語言核心合一，且 .NET 5+ 之後不再官方支援。本提案將其精神轉化為**語言級型別不變量**。([[Microsoft Learn](https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts?utm_source=chatgpt.com)][7], [[GitHub](https://github.com/microsoft/CodeContracts?utm_source=chatgpt.com)][8], [[Microsoft](https://www.microsoft.com/en-us/research/wp-content/uploads/2011/06/krml196.pdf?utm_source=chatgpt.com)][4])
* **Liquid Types / Refinement Types**：學術與實務上成熟，證明可以局部蕴含 + 子型別檢查做到可擴充的依值推理。([[goto.ucsd.edu](https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf?utm_source=chatgpt.com)][3], [[Microsoft](https://www.microsoft.com/en-us/research/video/liquid-types/?utm_source=chatgpt.com)][6])
* **Dafny / F\***：完整驗證語言展示了依值／精煉在大型程式正確性上的價值；C# 可採「務實子集」融入主流程。([[dafny.org](https://dafny.org/v4.0.0/DafnyRef/DafnyRef?utm_source=chatgpt.com)][5], [[GitHub](https://github.com/FStarLang/FStar/issues/196?utm_source=chatgpt.com)][17])
* **常數泛型（討論中）**：若該提案先落地，則本提案的「值入型別」能力將更完整。([[GitHub](https://github.com/dotnet/csharplang/discussions/7508?utm_source=chatgpt.com)][12])

---

## 可能疑慮（Drawbacks / Risks）

* **學習曲線**：研究顯示 Liquid/Refinement 類技術在可用性上需良好工具與教學。需以強 IDE 經驗化解。([[ResearchGate](https://www.researchgate.net/publication/392671846_Usability_Barriers_for_Liquid_Types?utm_source=chatgpt.com)][18])
* **驗證不決定性**：一般以「時間上限 + 退回執行期檢查」處理，並允許團隊調整嚴格度。
* **FP 生態差異**：不追求 Idris/Agda 的完整功能（如終止性檢查與依值模式比對），避免複雜度逾越主流使用者。([[docs.idris-lang.org](https://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?utm_source=chatgpt.com)][10])

---

## 開放議題（Open Questions）

1. **述詞語言的邊界**：是否限定為線性算術與簡單陣列長度、`Count` 等可決定子集？
2. **SMT 依賴與建置效能**：是否以可插拔的驗證後端與快取策略緩解？
3. **與模式比對的更深整合**：是否允許由 `when` 子句直接產生型別精煉窄化？
4. **錯誤等級策略**：是否預設為「警告」並提供 `#pragma`/`` 類似的 csproj 切換？

---

## 範本規格（Sketch Spec）

**語法**（簡化）

```
RefineTypeDecl
: 'refine' 'struct' Identifier '(' UnderlyingType Id ')'
'where' BooleanExpr ';'

RefineParam
: Attribute? 'Refine' '(' StringPredicate ')'
```

**型別檢查規則**

* `T{φ}` 視為 `T` 的**子型別**，若流程條件 `Γ` 可證明 `Γ ⊢ φ`，則允許從 `T` 隱式轉入 `T{φ}`。
* 反之需要 explicit cast（產生診斷；在 `checked refine` 模式插入執行期檢查）。
* 常數泛型 `const int N` 可在述詞中當常數使用；`where src.Length == N` 屬**可判定**等式。

**IL 抹除**

* `T{φ}` → `T`；述詞以 `CustomAttribute` 或 sidecar metadata 形式存在，以供靜態分析與 IDE。

---

## 實作路線（Implementation Plan）

1. **Roslyn 原型**：加入 `refine` 語法、Flow Analysis 擴充、SMT stub；
2. **最小述詞子集**：整數/浮點比較、`Length/Count`、四則運算、邏輯連接；
3. **IDE 體驗**：快速修正與診斷；
4. **與 const generics 原型串接**：示範 `Vector`、`Matrix`；
5. **文件化與教學**：比照可空參考型別的 Adoption Guide。

---

## 相關連結（References）

* Static abstract members in interfaces（已納入 C# 11）與官方草案。([[GitHub](https://github.com/dotnet/csharplang/issues/4436?utm_source=chatgpt.com)][1], [[Microsoft Learn](https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/proposals/csharp-11.0/static-abstracts-in-interfaces?utm_source=chatgpt.com)][2])
* 常數泛型（草案、runtime issue）。([[GitHub](https://github.com/dotnet/csharplang/discussions/7508?utm_source=chatgpt.com)][12])
* Liquid Types（論文與微軟研究介紹）。([[goto.ucsd.edu](https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf?utm_source=chatgpt.com)][3], [[Microsoft](https://www.microsoft.com/en-us/research/video/liquid-types/?utm_source=chatgpt.com)][6])
* Spec#／Code Contracts（歷史與現況）。([[Microsoft](https://www.microsoft.com/en-us/research/wp-content/uploads/2011/06/krml196.pdf?utm_source=chatgpt.com)][4], [[Microsoft Learn](https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts?utm_source=chatgpt.com)][7], [[GitHub](https://github.com/microsoft/CodeContracts?utm_source=chatgpt.com)][8])
* 「浮點帶範圍」作為依值型別的簡化案例（社群討論）。([[GitHub](https://github.com/dotnet/csharplang/discussions/6972?utm_source=chatgpt.com)][13])
* ref struct 能力擴張提案（C# 13）。([[GitHub](https://github.com/dotnet/csharplang/blob/main/proposals/csharp-13.0/ref-struct-interfaces.md?utm_source=chatgpt.com)][14])
* csharplang 問題／里程碑索引（便於後續掛鉤與歸檔）。([[GitHub](https://github.com/dotnet/csharplang/milestones?utm_source=chatgpt.com)][19])

---

## 尾註

* 本提案重點在**讓 C# 以最小變動獲得 80% 的依值型別益處**，並與現有提案（特別是**常數泛型**與**泛型數學**）互補。
* 建議先以 **Refinement Types + 可選執行期檢查** 上線，並在後續迭代逐步擴大述詞語言與驗證能力。

— 完 —

[1]: https://github.com/dotnet/csharplang/issues/4436?utm_source=chatgpt.com "[Proposal]: Static abstract members in interfaces #4436"
[2]: https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/proposals/csharp-11.0/static-abstracts-in-interfaces?utm_source=chatgpt.com "Static abstract members in interfaces - C#"
[3]: https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf?utm_source=chatgpt.com "Liquid Types"
[4]: https://www.microsoft.com/en-us/research/wp-content/uploads/2011/06/krml196.pdf?utm_source=chatgpt.com "Specification and Verification: The Spec# Experience"
[5]: https://dafny.org/v4.0.0/DafnyRef/DafnyRef?utm_source=chatgpt.com "Dafny Reference Manual"
[6]: https://www.microsoft.com/en-us/research/video/liquid-types/?utm_source=chatgpt.com "Liquid Types"
[7]: https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts?utm_source=chatgpt.com "Code Contracts - .NET Framework"
[8]: https://github.com/microsoft/CodeContracts?utm_source=chatgpt.com "Source code for the CodeContracts tools for .NET"
[9]: https://idris2.readthedocs.io/en/latest/tutorial/introduction.html?utm_source=chatgpt.com "Introduction — Idris2 0.0 documentation - Read the Docs"
[10]: https://docs.idris-lang.org/en/latest/tutorial/typesfuns.html?utm_source=chatgpt.com "Types and Functions — Idris 1.3.3 documentation"
[11]: https://www.microsoft.com/en-us/research/project/code-contracts/?utm_source=chatgpt.com "Code Contracts - Microsoft Research"
[12]: https://github.com/dotnet/csharplang/discussions/7508?utm_source=chatgpt.com "[Draft Proposal]: Const Generics #7508 - dotnet csharplang"
[13]: https://github.com/dotnet/csharplang/discussions/6972?utm_source=chatgpt.com "Proposal: Floats with Ranges #6972"
[14]: https://github.com/dotnet/csharplang/blob/main/proposals/csharp-13.0/ref-struct-interfaces.md?utm_source=chatgpt.com "csharplang/proposals/csharp-13.0/ref-struct-interfaces.md ... - GitHub"
[15]: https://github.com/dotnet/csharplang/blob/main/proposals/csharp-11.0/generic-attributes.md?utm_source=chatgpt.com "csharplang/proposals/csharp-11.0/generic-attributes.md at ..."
[16]: https://www.infoq.com/articles/code-contracts-csharp/?utm_source=chatgpt.com "Code Contracts in C# - InfoQ"
[17]: https://github.com/FStarLang/FStar/issues/196?utm_source=chatgpt.com "F* vs. Dafny · Issue #196 · FStarLang/FStar"
[18]: https://www.researchgate.net/publication/392671846_Usability_Barriers_for_Liquid_Types?utm_source=chatgpt.com "Usability Barriers for Liquid Types | Request PDF"
[19]: https://github.com/dotnet/csharplang/milestones?utm_source=chatgpt.com "Milestone Index - GitHub"