隱式編程：coherence 與 stability 屬性

這篇是 COCHIS: Stable and coherent implicits 的筆記

隱式編程機制是指，使用型別指導的推導能力，在使用者不提供完整資訊的情況下給出程式語意的技術。比如 Haskell 的 type class、Rust 的 trait 等。合成的過程叫做 resolution。

Haskell 的 type class 的一個重要特徵是給定的類型只會有一個 instance 符合。coherence 在這個意義下指的是，給出的程式語意是唯一的，也就是說對某段合法程式碼，不會合成出超過一個語意。

比如説 Haskell 會拒絕 show (read "3") == "3" 這段程式碼，因為根據 type class resolution 有很多種可能性（show : α -> String 跟 read : String -> α）

選了 α := Float 那結果是 False，因為 show (read "3") == "3.0"
選了 α := Int 那結果是 True
選了 α := Char 那結果是 True

所以這種會導致有多種語意出現的程式就需要被拒絕。

Haskell 的 overlapping instances 技術是對上述問題的一種推廣（使我們可以接受更多程式），比如說

class Trans α where trans :: α → α
instance Trans α where trans x = x
instance Trans Int where trans x = x + 1

對於程式 trans 3 應該要決定出什麼結果？Overlapping 的決定是，因為 α := Int 比沒有決定更特定，因此選 instance Trans Int。然而，也有 overlapping 策略也無法決定的情況，比如下面比較刻意的

class C α β where
  m :: α → β → Bool
instance C Bool α where
  mx y = x
instance C α Bool where
  mx y = y

對程式 m True False 兩個 instances 都一樣特定，沒辦法決定，因此這段程式碼也必須被拒絕。

Stability 是跟 coherence 高度相關的屬性。不正式的說，stable 是指 type variables 的實例化與否不影響 resolution 的結果。但 overlapping 技術會影響這個結果，比如

bad :: α → α
bad x = trans x

就是一個 unstable 的定義。如果寫成 Trans α => α → α 就不一樣了，這表示 α 交由呼叫 bad 的地方決定，但這裡則是必須在定義處馬上決定，如果 Haskell 接受這段定義，那可能會選擇第一個 instance Trans，導致 bad 3 是 3 而 trans 3 是 4。雖然 bad x := trans x 是定義等價。

也可以參考 https://blog.ezyang.com/2014/07/type-classes-confluence-coherence-global-uniqueness/ 的案例跟論點。