類型的繼承和精煉 —— subtyping

上次討論到用 sets 來表達一些簡單的 types，也提到 function types 的表示法和意義

這次，我想要從 C 語言函數和 types 之間產生的問題來對 types 做更深入的探討

還記得我們上次怎麼用集合來表達 int 類型嗎
    int = { m | -32768 ≦ m ≦ 32767 }

好，那我們來看看下面這個 C 語言函數：

1. int doubleMe (int x) { return x * 2; }

複製代碼

(為了簡潔起見，以後都會用以下方式表示函數宣告定義和呼叫)
函數宣告：
    doubleMe : int → int
(函數名稱中底線代表接受參數的地方，不寫就是接受在函數名稱後方)
函數定義：
    doubleMe x ↦ x * 2
函數呼叫：
    doubleMe x

這個函數表面上看起來好像沒什麼問題，但是要是你還記得 int 類型的定義的話，或許你就會發現

當 doubleMe 16384 的時候，函數的回傳值已經超過 int 中的最大值 32767 了！

這代表了什麼？
doubleMe 竟然回傳了一個不在 int 中的值，但是型態卻還宣告成 int → int？

更精確的說，doubleMe 的值域 (domain) 已經超過了上域 (codomain) 了啊！

這是一件多麼可怕的事情啊！
或許我們應該再看看另一個例子：
    divide_by_ : int → int → int
    divide x by y ↦ x / y

這個函數又有什麼問題？
考慮看看，要是 divide 100 by 0 的時候呢？

devide_by_ 函數怎麼能夠允許一個一定會導致錯誤的值被傳入呢？
而且錯誤的程式碼竟然還能通過編譯！

你或許會想，一定有什麼好辦法能夠解決這個問題的吧！

當然，答案是有的，這個東西就叫做 `refinement type`

想想看，要是我能夠對傳入函數的型別做一些限制的話，事情不就變得簡單多了嗎？

例如：
    divide_by_ : int → nonezero → int
        where nonezero = ∀m : int. { m | m ≠ 0 }
之類的東西

這樣，當我們試圖寫出可能將 0 傳入 divide_by_ 函數的第二個參數的程式碼的時候，編譯器就會告訴我們，bang!! bang!! bang!!! 編譯錯誤！

因為 0 並不屬於 `nonezero` 這個型別，你要馬新增轉型規則，要馬檢查一下程式是哪裡不夠嚴謹吧

大家一定對「繼承」(inheriting) 不陌生吧！
其實 `refinement types` 和 `deriving types` 都是 `subtyping` 的一種

而且「繼承」和「精煉」都有「子型別」和「母型別」的概念

先來看看我們可以怎麼表達「繼承」(<:) ：
    ∀T. ∃U. U <: T ⊨ T ⊆ U

意思是說，要是 U 繼承 T (或是說，U 是 T 的衍生型別 (derived type)) 的話，T 會是 U 的子集合

原因其實很容易理解嘛～

因為在繼承關係中，子型別只能增加成員，不能捨棄成員，所以子型別的成員數量至少會和母型別一樣多

再來，讓我們試著描述看看「精煉」(<r) 吧：
    ∀T. ∃U. U <r T ⊨ ∀m : T, P. U ↔ { m | P }

這句說明了，如果 U 精煉 T 的話，U 對成員的限制將會比 T 多一條 P

換句話說，T 的成員不一定是 U 的成員，而 U 的成員則一定是 T 的成員，所以說，U 的成員最多也只會和 T 一樣多

不知道大家有沒有看出來，「繼承」和「精煉」實際上非常類似：

要是有一個 type T = { m | P } 的話，那麼：

T 的衍生型別 D 其實就是往 m 的地方加東西：
    D = { m, n | P }

T 的精煉型別 R 其實就是往 P 的地方加東西：
    R = { m | P, Q }

而且 D 和 R 都是 T 的子型別 (subtypes)，並且，毫無疑問的，一個 type U 當然能夠同時繼承和精煉 T

再來就是重點啦，我們該如何在 C、C++ 中使用 refinement types 呢？

很遺憾的，我不知道要怎麼在 C 裡使用 refinement types，我猜，或許使用 macro + enum 可以做到，不過我自己沒試過就是了

不過，在目前的 C++ 裡，refinement types 應該可以算是被半支援的

我們在 template metaprogramming 中，是有辦法做出 refinement types 的，不過也僅限於 template metaprogramming 中使用

先來一個例子好了：

1. template <
   
2.   int N
   
3. , bool B = (N % 2) == 0
   
4. >
   
5.   struct even : public std::integral_constant<int, N>
   
6.   {};
   
7. 
   
8. template <int N>
   
9.   struct even<N, false>
   
10.     ;

複製代碼

在上面這段程式碼中，`even` 只接受偶數，要是使用者企圖建立奇數的實例的話，就會遇到 even<奇數> 是 incomplete type 的編譯錯誤訊息

另外，在 <type_traits> 中有很多的 helper meta functions 對於製作 refinement types 都非常好用

例如 std::is_integral 可以判斷一個 type 是否為內建的數字型別，這也可以做為 refine 的依據

另外還有 std::is_class、std::is_pointer、std::is_empty……一大堆的 helper functions，而且還可以配合 std::enable_if 來用喔

(<type_traits> 的 overview: en.cppreference.com/w/cpp/header/type_traits)

啊！對了，也可以用 SFINAE 來當作 refine 的條件喔！用 SFINAE 當條件真的超級酷炫的啦 XD


這篇我們探討了函數射、值域的問題，也用集合來理解了兩種 subtyping

下次我想介紹 type 的 type，或是甚至是 type 的 type 的 type，它實際上的用途，和相關理論

當然，也是如果我還有動力繼續往下寫的話啦 XD...

瀏覽完整內容，請先 註冊 或 登入會員