Phantom of Haskell

Phantom types 是指某個在 type constructor 上的 type parameter 而且沒有被任何該 type 的 data constructors 用到。 例如說:

對 type (constructor) T0 來說,a 是個一般的 parameter;而 n,因為沒有被 C0 用到,所以就被叫做 phantom types (幻影型別? 貌似有點二.. XD)。

Motivative Problem

為了建立初步的直覺,先讓我們把其他的 parameter 都先丟一邊。來看一個單純的情況:

T1 是一個用 IntString 聯集而成的 type。但是我們在 type level 丟掉了「當初這個 T1 到底是用 Int 還是 String 做出來的」這個資訊。所以我們就可以做出一些奇怪的事情,例如說我們可以寫出一個 T1 的加法:

如果今天我們的目的是「對任意的 IntString 我都要能加起來」的話,那其實這個就可以運作的非常好。 事實上,這樣的彈性其實有時候還蠻有用的。不過,問題在於,當我們需要加以限制時就爆炸了。 例如說我只希望我的加法只有在吃到兩個“同一種東西”時才會以定義, 這樣的情況下,T1 那樣的定義方式其實就不適用了。

這種情況我們就可以加上一個 phantom type 來當做某種 label 去補強那個遺失的資訊。

現在,我們的 (+) 就不可能能把 IntString 給相加起來了!

上述的例子當然可以 generalized 成 polymorphic 版。

這樣我們好像不會在 type level 丟掉關於 ab 是誰的資訊, 但是其實問題還是一樣。 以上面那個例子來說,當我們拿到一個 x :: Tp Int String 的時候, 除非我們把 x 打開 (也就是對 x 做 patten matching), 否則我們還是不知道這個 x 到底裡面裝的是什麼。

Digging Deeper

上面的問題大概會是看到 phantom types 時最常見的入門範例。 但是,其實光時那樣的理解似乎並沒有讓我們比較好過。 尤其是,只是簡單看過上面的說明, 我們常常還是很難馬上反應過來到底 phantom types 要怎麼用。 所以,也許,也許我們可以試著把上面的看法反過來理解。

首先,我們可以知道說,data T a b 其實是說,

給定某個 a 還有某個 b,我們可以決定出一個 type T a b

但是,有時候 T a b 可能會太大以致於不夠符合我們的需求, 或者說,我們只想要“使用” T a b 當中的某一部分就好。 所以我們會想要有個方法去把 T a b 分成若干個 types 的聯集, 並且從其中挑出我們要的那一個小 type 就好了。 這個方法,就是在 type level 多加上某些「額外的資訊」 來讓我們指定說我們要的是 T a b 中的哪一部分。 有趣的地方是,因為我們加上的是額外的資訊, 所以其實這個資訊在真正建立資料的時候是不會用到的。

舉例來說,我們可以定義向量如下:

a 被決定時,我們就有一個 Vector a 用以描述內容值是 a 的向量資料結構。 不過不過,考慮到我們最常用的向量都是 2D 或 3D 向量, 如果我們可以明確的描述什麼是 2D 和 3D 向量就太好了! 所以我們重新定義了下面這樣的東西:

然後我們就可以寫出 2D 或 3D 限定的向量運算函數。例如說

這裡的核心機制就是 data Vector a n 中的那個 n, 它代表了我們這個 Vector 的維度 (維度本身是 newtype 去定義的)。 而 n ,就是一個 phantom types

小結

phantom types 可以簡單地當做是一種 type level 上的 label,就像最一開始的例子一樣。 我們可以讓它的意義非常的複雜以滿足我們定義函數時的各種神奇需求。 甚至某個程度可以用來強制設定我們的資料結構被使用的方式,尤其是我們提供 lib 給別人用的時候。 例如說我們可以寫出一組資料結構和函數來專門處理各種非空字串相關的操作:

但是像 vector 這個例子中這樣的 phantom types, 其實相比之下又稍稍更複雜一點。 我們在 vector 的例子中的 2D 和 3D 是用 newtype 建立而成, 說穿了其實和上面的 data Gooddata Bad 半斤八倆。 更好的作法是把自然數拉到 type level 上面, 然後用 type level natural number 去描述那個維度。

這樣我們的 2DVector a 就會寫成 Vector a (Succ (Succ Zero))。 就是我們一般說的 indexing

[Tags: haskell, types]