用依值型別規範 layering 系統

layering 的概念其實並不陌生，在不同的程式語言裡面有諸多實現不同類型的限制的方式。最常見的一種就是 type system，其他像是 eBPF 的 logging 與 process 分開也能算是這樣的工具，甚至是最簡單的 assertion 也能幫助我們進一步對程式做更多的推斷。

1. Software Design for Flexibility

在這本書的第六章用比較彈性的方式建立了 layering 的統一系統，例如說重力可以寫成

(define G
  (layered-datum 6.67408e-11
    unit-layer (unit 'meter 3 'kilogram -1 'second -2)))

上面的單位 unit 數字都是指數的意思，用我們熟悉的系統表示就會像下面這樣

\[ \frac {m^3} {kg \cdot s^2} \]

這裡 unit 會針對同樣的運算做修改，例如乘法就有下面的運算特性。

(* (unit 'meter 3 'kilogram -1 'second -2)
   (unit 'second 1))
   ->
   (unit 'meter 3 'kilogram -1 'second -1)

書中採用的技術對大部分語言來說都是適用的，只要能表達附註屬性在資料上就可以了。 OOP 語言可能就會定義一個專有的 class 表示 *layered data*。這裡用標記的方式的優勢也一覽無遺，畢竟大部分語言的型別系統通常是沒有這麼強力的能力去做這麼複雜的限制。

2. 用型別論規範

但書中的系統還是有難以驗證的缺點，要是 layering 的規則沒有被遵守呢？相較於型別論受過檢驗，這種手工的系統比較難被相信。但是就像剛才說的，大部分的語言的型別系統其實也很難做這麼複雜的規範，這裡計算的資料也不具有 cartesian product 這種資訊無損的特性。要是每個計算都要存 n 個輸入（即採用 cartesian product 存下所有輸入），最後才做計算也不太合理。

所以這裡就需要更複雜的，可以依賴值去編碼型別的 dependent type 出場了。用型別系統的好處顯而易見，正確的轉換被型別保證，不用擔心寫出的限制其實沒有被遵循。下面是簡單的案例

\func test-*-1 : LayeredData Int ((Meter X 3) :: (Kilogram X -1) :: (Second X -1) :: nil)
  => g v-* s
  \where
    \func g : LayeredData Int ((Meter X 3) :: (Kilogram X -1) :: (Second X -2) :: nil) => Box 7
    \func s : LayeredData Int ((Second X 1) :: nil) => Box 2

\func test-*-2 (g : LayeredData Int ((Meter X 3) :: (Kilogram X -1) :: (Second X -2) :: nil))
             (s : LayeredData Int ((Second X 1) :: nil))
  : LayeredData Int ((Meter X 3) :: (Kilogram X -1) :: (Second X -1) :: nil)
  | g, s => g v-* s

\func test-+ => s v-+ s
  \where
    \func s : LayeredData Int ((Second X 1) :: nil) => Box 3

總而言之，可以看到利用成熟的型別系統，我們一樣可以封裝各式各樣我們有興趣的資料用來做運算檢查。要是上面的 test-*-1=、=test-*-2 或是 test-+ 的型別有任何一個地方寫錯，都會被 type checker 找出來，從而變成能夠被機器檢查正確性的程式。

2.1. 完整實作

首先要看實作合併底下的值的計算部分，其實就是普通的 + 跟 =*=，但是其型別部分則是

加法要求單位相等
乘法要求調用 unit-* 來重新計算單位

-- 這裡要求了單位必須一樣才能運算
\func \infix 6 v-+ {us : Units} (a b : LayeredData Int us) : LayeredData Int us
  | Box v1, Box v2 => Box (v1 + v2)
-- 關鍵就在這裡推論兩個單位出來之後用 `unit-*` 得出新的單位
\func \infix 6 v-* {us1 us2 : Units} (a : LayeredData Int us1) (b : LayeredData Int us2)
  : LayeredData Int (unit-* us1 us2)
  | Box v1, Box v2 => Box (v1 * v2)

接著則是關鍵的單位運算系統，這裡因為一些弔詭的問題，不得把 fold 寫成非常特定用途的程式。但總之解決之後，也得到了可以通過檢查的程式。可以看到乘法的單位合併演算法非常簡單

要是紀錄的單位相同，就進行相加。
否則就繼續向後尋找可能的合併目標
要是都找不到，就把自己插在最後面

\data Unit
  | Meter
  | Kilogram
  | Second
\func unit=? (u1 u2 : Unit) : Bool
  | Meter, Meter => true
  | Kilogram, Kilogram => true
  | Second, Second => true
  | _, _ => false

\type Units => List (Pair Unit Int)
\func fold (f : (Pair Unit Int) -> Units -> Units) (b : Units) (l : Units) : Units
  | _, b, nil => b
  | f, b, :: a l => f a (fold f b l)

\data LayeredData (T : \Set) Units
  | Box T

\func unit-* (us1 us2 : Units) : Units => fold insert us2 us1
  \where
    \func insert (u : Pair Unit Int) (us : Units) : Units
      | (X u u-val), :: (X v v-val) xs => \case unit=? u v \with {
        | true => (u X (u-val + v-val)) :: xs
        | false => (v X v-val) :: insert (u X u-val) xs
      }
      | u, nil => u :: nil

引用的程式庫以及其他輔助程式

\import Arith.Int
\import Data.Bool
\import Data.List
\open IntRing (+, *)

\data Pair (A B : \Set)
  | \infix 7 X A B

3. 結論

雖然用型別規範之後是沒有原本的程式方便，但相應的得到更可信任的程式，恰恰也是 layering 的概念想傳達的關鍵。相較於程式什麼都能做（圖靈完備），程式能被推論更加重要。