交代

對了，我之前說寫完 relational derivation 後要寫 dependent types，可是後來發現如果不用 Agda 要用 imperative languages 當例子的話，就等於是自己發明型別系統了，工程浩大。前一陣子曾稍微描述我想在 compiler final project 試作的 "Dependent C"，就湊合著看一看吧 XD。如果真的要把 array bounds checking 做成 Dependent C 的樣子，應該不會用全自動檢查的方式（scm 老師上次給我們看一篇最近的 paper，專門做自動化的 array bounds check elimination，那些 typing rules 簡直是變態 XD），而會要求程式員在必要的地方提供證明，然後像 pointer indirection 的問題和 a[b[i]] 這種狀況說不定都得做點簡化。

還是舉一些實際例子簡單講我想做什麼好了。如果我們寫

#define N 10
int a[N];
for (i = 0; i < N; ++i)
  a[i] = 0;

那我們知道在迴圈內存取 a[i] 絕對不會超出邊界。相對地，如果我們寫

for (i = 0; i < N; ++i)
  a[i] += a[i + 1];

那麼存取 a[i + 1] 就是不可靠的，因為在迴圈內我們有 i <= N - 1，而有 i + 1 <= N，可能超出邊界。一種方式是讓編譯器自行推斷，但這還算是 research topic。為了減少編譯器的負擔（i.e., 編譯器撰寫者的負擔 XD），我們可以要求存取 a[i + 1] 以前，程式員必須提供 0 <= i + 1 && i + 1 <= N - 1 的證明。我猜大概就是把 Hoare logic 寫在 C code 裡面吧，整套機制和語法還要再設計。

又例如我想寫一個 vector addition function：

int* vec_add(int* p, int* q, size_t n) {
  int i;
  for (i = 0; i < n; ++i)
    p[i] += q[i];
  return p;
}

這段 code 有陷阱：p 或 q 可能是 NULL，或是兩者之一未指向 n 個以上的 ints。（其實有第二個條件就夠了 ─ 第一個條件蘊含第二個條件。）有了 dependent types，我們就可以在型別上要求傳進來的 pointers 必須指向至少有 n 個元素的 arrays。

講稍微深入一點好了。正式一點看的話，我們可以把一個型別看成 first-order logic proposition，具有這個型別的值就是對這個 proposition 的一個證明。先假設只做最簡單的 existential-quantified propositions。例如一般的 int* 可以對應到 "∃p : int*. ⊤"（⊤ 是恆真的 proposition），要證明這個 proposition，只要隨便提供任何一個 int* 就行了。而在 vec_add 裡面，我們想要的型別可以對應到 "∃p : int*. LENGTH(p) ≥ n"。下稱 existential quantifier 裡面的 proposition 為 P。P 相依於 p 和 n 的值（i.e., p and n occur free in P），因此整個 type 是個 dependent type。想通過型別檢驗，使用這個函式的程式就必須（在編譯期）證明他提供的引數確實滿足 P。這樣甚至可以增進一點點的效能，因為 vec_add 不需要做執行期檢查。這層邏輯與程式之間的關連（propositions as types; proofs as programs）就是 Curry-Howard isomorphism。（此處我們是非正式地使用這個概念，當程式以各種 lambda calculi 呈現的時候，就會分別和各種邏輯演繹系統有正式的對映。）

等〈Derivation-Carrying Code using Dependent Types〉出現以後（是要等上了才能放？），也可以看看（至少）簡介的部份。scm 老師和 Patrik Jansson 把論文修得好感人、好好看，不看可惜 XD。

--
結果不小心寫到把 Curry-Howard 都請出來了 XD。

---

變數宣告上，把 first-order logic formula 稍微改一下，效果好像不錯耶。像 vec_add 可能就寫成

int* vec_add(int* p . LENGTH(p) >= n,
             int* q . LENGTH(q) >= n,
             int n) . return == p;

這看起來很好解析（parse），而且我覺得符號看起來還不錯 XD。

--
有人要一起玩嗎？XD 如果學期初就把賺人熱淚的 proposal 交上去，老師說不定會很感動地答應 XD。

---

把 Dependent C 的議題大概整理一遍：

• 相容性：回溯相容於 C89（C99 可能太辛苦；如果合作者想做別的語言也可以，但必須是 statically-checked language，否則沒什麼意義）；
• 安全性：可以在編譯期確保不會發生 array index out of bounds 或 deference of null pointers，更有野心的話可以做更多；
• 執行效率：最完美的狀況是所有檢查都在編譯期完成，真的沒辦法才安插 runtime check；
• 表達力：能表達的函式介面契約更加豐富，一樣愈有野心的話可以愈豐富，例如從介面上保證 qsort 一定會排序；
• 乾淨：語法要夠漂亮，而且不要讓程式碼被 proof code 淹沒（後者可能和「所有檢查都在編譯期完成」的目標相衝突）。

--
然後如果有人可以寫 x86 assembly 的 (optimising) code generator 就太棒了 XD。

---

如果有人想一起做，請務必留言或寄信或告知 thirddawn 喔！先說好：就算湊到人，老師也不一定會同意；而且假設老師同意了，這應該就是整個學期的事，要（嚴重）超前課程進度，然後我猜平常的作業還是要照做（除非老師特別仁慈），或許還得冒點「拚一學期拚不出好成果」的風險。

--
總之條件惡劣、環境嚴苛就對了 XD。