※ 引述《noctem (noctem)》之銘言：
: 不過你說的是 C\Java 是不是一致的。這倒是沒細想過。
: 一般「不一致」的意思是所有 type (proposition) 都
: 有一個 term (proof), 連 bottom (false) 都有 term.
: 但
: 1. 不知道 C\Java 的 type 裡面有沒有 bottom 這種說法。
一般而言是把 void 當成 bottom, 不過當然性質上應該是差滿多的...
至少這件事是沒辦法做的：
void undef(){}
int i = undef(); // type error
而就像 Haskell 可以：
undef = undef
f :: Int
f = undef
剛剛試 Scala 也可以：
def undef: Nothing = undef // 需要明白表示 Nothing (bottom)
val i = undef
另外我總算找到當初在講 C++ None 的討論：
Subject: [Proposal] noreturn_t
http://groups.google.com/group/comp.std.c++/browse_thread/thread/
1e6093a60facd084/
如果以 Andrei Alexandrescu 所定義 None 的話：
struct None{
None(){ throw "can't happen"; }
None(const None&){}
template <class T>
operator T&() const{ // 這是自動型別轉換，這樣寫就是能轉成任何 type
throw "can't happen";
return *this;
}
};
那倒是真的可以這樣做了：
None undef(){}
int i = undef();
這樣程式會立即有 exception, 而不是卡住。不過改成 while(true); 也行..
（Haskell 的 undefined 大概就類似這邊的 None 吧？）
不過我不是很懂這件事跟 bottom 有 term 有什麼關係..?
像 None 這樣算是 bottom 有 term 嗎？
*
以下可能有點離題了，順便把上面那篇討論的一些事提一提：
製作 None 的理由，包含主旨的 noreturn_t, 大概是想表達程式不可能
可以執行到那個地方，比方說某個 function 一定需要造成程式中斷：
void graceful_exit(){
exit(0);
}
但如果 exit(0); 什麼事都沒發生咧？如果改成：
None graceful_exit(){
exit(0);
}
這樣如果 exit(0); 什麼事都沒發生，None 就會產生，而 None 產生就如同上面
所定義，會產生 exception, 於是整個程式就爛掉了，而不是「什麼事都沒發生」
另一方面則是關於 ternary operator, 像是：
int i = condition ? something() : undef();
或是更激進的：
int i = something() || undef();
這樣很多事情就可以由 statement 改寫成 expression 了。
: 2. 另外，在 Haskell 裡
: undef = undef
: 可以有任何 type. 在 C/Java 裡有這種可以有任何
: type 的程式嗎？
Java 我猜大概做不到吧，C 可能用 macro + type cast..?
不過再怎麼樣我想也都是模擬的，可能會哪裡不完整，不是很清楚...
==
noreturn_t/None 那篇看日期是三年前的討論，那時我只隱隱約約覺得
好像看到什麼地圖可以畫出來，但又不知道是什麼，看來現在多懂很多了 @@
這都要感謝穆老師 XDXD
--
Nobody can take anything away from him.
Nor can anyone give anything to him.
What came from the sea,
has returned to the sea.
Chrono Cross
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 220.135.28.18
※ 編輯: godfat 來自: 220.135.28.18 (06/25 23:19)