在做物理或工程上的算術時，我們常常會在單位上出錯：把公尺加到秒上、把公斤乘進長度卻沒有標記，或是次方算錯，最後得到一個「數字看起來合理」但單位錯亂的結果。這些錯誤在紙筆運算時不容易被察覺，發現的時候往往已經是好幾步之後，回頭檢查非常的麻煩

能不能讓工具替我們把關呢？如果單位本身就是型別的一部分，編譯器就能在我們把不相容的東西硬湊在一起時直接拒絕。我們可以用 Agda 來規範出這樣的一個系統

用 Agda 實現單位正確的算術 [ag-OW40]

{-# OPTIONS --safe --without-K #-}
module ag-OW40 where

open import MLTT.Spartan hiding (_+_)
open import MLTT.Negation
open import MLTT.List
open import MGS.MLTT using (has-decidable-equality)
open import Integers.Type
open import Integers.Addition
open import Integers.Multiplication

首先我們建立一些單位

data Unit : 𝓤₀ ̇ where
  Meter Kilogram Second : Unit

單位的相等是可判定的

Unit-≟ : has-decidable-equality Unit
Unit-≟ Meter    Meter    = inl refl
Unit-≟ Kilogram Kilogram = inl refl
Unit-≟ Second   Second   = inl refl
Unit-≟ Meter    Kilogram = inr (λ ())
Unit-≟ Meter    Second   = inr (λ ())
Unit-≟ Kilogram Meter    = inr (λ ())
Unit-≟ Kilogram Second   = inr (λ ())
Unit-≟ Second   Meter    = inr (λ ())
Unit-≟ Second   Kilogram = inr (λ ())

整數的相等也是可判定的，TypeTopology 已經有 ℤ-is-discrete，這裡我們給它一個新名字，好跟 Unit-≟ 慣例相符

ℤ-≟ : has-decidable-equality ℤ
ℤ-≟ = ℤ-is-discrete

完整的單位簽名由一系列單位與整數組成，整數用來表示該單位的次方，比如公尺的 3 次方就是 [(Meter , pos 3)]

Units : 𝓤₀ ̇
Units = List (Unit × ℤ)

現在讓任何型別 T 都可以附帶單位，但 runtime 只存放 T

data _with-unit_ (T : 𝓤 ̇ ) (us : Units) : 𝓤 ̇ where
  Box : T → T with-unit us

接下來我們要對單位進行乘法，方法就是同單位的次方抵銷。這個合併演算法可以大致描述成

要是紀錄的單位相同，就進行相加並放回清單。除非相加結果為 pos 0（也就是次方為 0），這時候就直接從清單中消去
否則就繼續向後尋找可能的合併目標
要是都找不到，就把自己插在最後面

*-unit : Units → Units → Units
*-unit us₁ us₂ = foldr step us₁ us₂
  where
  step : Unit × ℤ → Units → Units
  step (u , n) []             = (u , n) ∷ []
  step (u , n) ((v , m) ∷ xs) with Unit-≟ u v
  ... | inr _ = (v , m) ∷ step (u , n) xs
  ... | inl _ with ℤ-≟ (n + m) (pos 0)
  ...   | inl _ = xs
  ...   | inr _ = (u , n + m) ∷ xs

現在開始實現帶有單位的整數運算。相加只能跟同單位的數一起，所以打從一開始沒辦法寫錯把不同單位的數字加在一起

_+̇_ : {us : Units} → ℤ with-unit us → ℤ with-unit us → ℤ with-unit us
Box v₁ +̇ Box v₂ = Box (v₁ + v₂)
infixl 40 _+̇_

乘法涉及到單位的相乘（正確的處理次方抵銷問題）

_×̇_ : {us₁ us₂ : Units}
      → ℤ with-unit us₁
      → ℤ with-unit us₂
      → ℤ with-unit (*-unit us₁ us₂)
Box v₁ ×̇ Box v₂ = Box (v₁ * v₂)
infixl 40 _×̇_

最後來看一些範例，這裏把 3s + 3s 所以得到 6s

test-3s+3s : ℤ with-unit [(Second , pos 1)]
test-3s+3s = s +̇ s
  where
    s : ℤ with-unit [(Second , pos 1)]
    s = Box (pos 3)
is-6s : test-3s+3s ＝ Box (pos 6)
is-6s = refl

這裏把 7m³/(kg·s²) 乘上 2s，所以得到 14m³/(kg·s)

test-7m³/kg·s²×2s : ℤ with-unit ((Meter , pos 3) ∷ (Kilogram , negsucc 0) ∷ (Second , negsucc 0) ∷ [])
test-7m³/kg·s²×2s = g ×̇ s
  where
    g : ℤ with-unit ((Meter , pos 3) ∷ (Kilogram , negsucc 0) ∷ (Second , negsucc 1) ∷ [])
    g = Box (pos 7)
    s : ℤ with-unit [(Second , pos 1)]
    s = Box (pos 2)
is-14m³/kg·s : test-7m³/kg·s²×2s ＝ Box (pos 14)
is-14m³/kg·s = refl

不是具體的值當然也可以應用這套系統

test-*-abstract :
  ℤ with-unit ((Meter , pos 4) ∷ (Kilogram , negsucc 0) ∷ (Second , negsucc 1) ∷ [])
  → ℤ with-unit [(Second , pos 1)]
  → ℤ with-unit ((Meter , pos 4) ∷ (Kilogram , negsucc 0) ∷ (Second , negsucc 0) ∷ [])
test-*-abstract a b = a ×̇ b

Layering 系統 [local-0]

其實上面的概念來自 Software Design for Flexibility，書中把這個技巧稱之為 layering。書中的程式長得像這樣：

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

用我們熟悉的系統表示：

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

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

書中的系統的缺點是難以驗證，要是 layering 的儲存單元沒有正確操作呢？相比於依賴型別論的檢驗，手工制作這樣的系統更難被相信沒有疏失。但除了用 Agda（或類似的語言），還有什麼辦法可以讓我們相信規範的正確性呢？

我在 2022 年的時候認為採用 cartesian product 存下所有輸入，組合 AST 時驗證等到最後才計算很不合理。但其實這應該是在沒有高複雜度的型別系統時應該採取的設計（其實就是某種直譯器模式變種）。像這樣臨時附加上的型別系統通常足夠小，足以通過原始碼直接判斷正確性，又不需要因此採用其他語言。所以採用這樣的方法除了稍微不直覺跟一點 runtime 開銷，在正確性很重要時也沒什麼。不過反過來說 layering 系統一般來說都需要額外付出 runtime 檢查開銷，所以除非確定正確性是必要條件，否則這大概也不會是好的實現方法

到這裡你應該已經可以想出在自己最熟悉的語言裡面要怎麼寫出類似的程式，因為 layering 的概念其實並不陌生，在不同的程式語言裡面有諸多實現不同種類的限制的方法。最常見的一種就是 type system，其他像是 eBPF 的 logging 與 process 分開也能算是這樣的工具，甚至是最簡單的 assertion 也能幫助我們進一步對程式做更多的推斷