本帖最後由 CoNsTaRwU 於 2016-10-16 01:57 PM 編輯
上次討論到用 sets 來表達一些簡單的 types,也提到 function types 的表示法和意義
這次,我想要從 C 語言函數和 types 之間產生的問題來對 types 做更深入的探討
還記得我們上次怎麼用集合來表達 int 類型嗎
int = { m | -32768 ≦ m ≦ 32767 }
好,那我們來看看下面這個 C 語言函數:- 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 中使用
先來一個例子好了:- template <
- int N
- , bool B = (N % 2) == 0
- >
- struct even : public std::integral_constant<int, N>
- {};
- template <int N>
- struct even<N, false>
- ;
複製代碼 在上面這段程式碼中,`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... |