Go 的 interface [tt-000M]

2023-09-23

Go 語言的 interface，範例如下

type Abser interface {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               Abs() float64
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       }

其中的 Abs() float64 可以被改寫成抽象語法 Abs : () -> float64。因此一個 interface $A$ 有一組與其關聯的一系列簽名 $\hat P$ 。並且，對 Go 而言下列的兩個 interface 並沒有差異

type A interface {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               F(C) D
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       type B interface {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               F(C) D
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       }

因此我們可以更進一步認為 Go 的一個 interface $A$ 可以完全由其簽名 $\hat P$ 替換。

Java 的 interface 與 bounded polymorphism (bounded quantification) [tt-000N]

2023-09-23

在 Java 之中可以定義 interface，範例如下

interface Comparable {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         int compareTo(T other);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       }

相較於 [Go 中不用明確宣告](tt-000D)，在 Java 中實現 interface I 需要寫成 class T extends I，因此雖然 Java 的 interface $A$ 也有其相關的一組簽名 $\hat P$ ，但兩個有同樣簽名 $\hat P$ 的 interface 不是同一個型別。

而在 Java 中 bounded polymorphism 指的是以下的 interface 使用方法：

<S extends Comparable> S min(S a, S b)

這會使得沒有明確宣告實現 Comparable 的型別無法被傳為 min 的引數。

問題所在 [tt-000O]

2023-09-23

現在考慮一個簽名

f : (S \le A) \Rightarrow S \times S \to S

在 Java 裡面可以確實保證兩個參數跟回傳的型別都是同一個。在 Go 裡面這個簽名就只能寫成

f : \hat P \times \hat P \to \hat P

而兩個參數跟回傳的型別不一定相同。現在我們就會發現乍看之下 interface 對類型的約束跟多型一樣可以被多個不同的型別滿足，但事實上根本就是不同的東西。

interface 是一種子類型關係，換句話說當 $T$ 實現 $A$ 我們就說 $T \le A$ ，在每個要求 $A$ 的位置都可以用 $T$ 取代。

多型的本體是一個型別等級的參數！在語意學上，上面的簽名可以改寫成 $f : \Lambda S. S \times S \to S$ ，當你寫下

f \; k

的時候，乍看之下是一個完整的呼叫。實際上編譯器會先推導 $k$ 的類型，記作 $\uparrow k$ ，譬如假設 $k : C$ 則 $\uparrow k = C$ ，這時候就可以做型別替換 $(\Lambda S. S \times S \to S) C$ 得出 $C \times C \to C$ 。因此真正的呼叫程式碼是

f \; [C] \; k

子類型規則並不能取代替換這個語意。在 Java 的 $f : (S \le A) \Rightarrow S \times S \to S$ 規則下，僅是多檢查了 $C \le A$ 是否為真，子類型與多型仍然是不同的規則。