用 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

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

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

*-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 )
  ...   | 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  _+̇_

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

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

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

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

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

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

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

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