作者godfat (godfat 真常)
看板PLT
标题Re: [问题] 程式语言大部分是 Turing Complete 的吗？
时间Thu Jun 25 23:18:20 2009
※ 引述《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)