bottom, bottom, ⊥, ⊥, ⊥...

日前看到這一篇: The Point of Laziness

劈頭就說：

It is not possible in Haskell to define the type of natural numbers, nor
the type of lists of natural numbers (or lists of anything else), nor any
other inductive type!

讓我感到很困惑，最近滿腦子都在想這些事。到現在也還沒什麼肯定的想法，
但我相信如果繼續拖下去，繼續想繼續看的話，大概永遠沒辦法筆記吧 XD

所以就暫時把目前想到的一些東西寫下來。一開始這篇我真的看不太懂，
只覺得他講了很多結論，卻看不到過程。逼不得已，只好連 comment
也一篇篇看。[0]

後來讀到其中一個 comment gasche 提到：

Robert Harper is here referring to the *lifting* behavior of Haskell
data types, where you may have exotic values using ⊥ when you
make for a sum. For example, type `Either a b` has all elements of a,
all elements of b, plus a ⊥ element. So this is not exactly a disjoint
sum (for a precise definition of what he means by “sum”, see the
categorical definitions of sum and product).

雖然我不知道 categorical definitions 是什麼，是指在 category theory
上的定義嗎... 如果是的話，我懷疑我是否能搞懂。總之作者 (Rober Harper) 回答：

More precisely, all types in Haskell are pointed (not necessarily
lifted). But, yes.

接著 Andreas Rossberg 又補充：

To expand on Bob’s reply: his point (and what he complains about in
his post) is that this type in fact does not represent the natural
numbers in a lazy language, because the type is unavoidably
inhabited by additional “values”. For example,

nonnat :: Nat
nonnat = Succ nonnat

Despite the type, this is not a natural number, and inductive principle
don’t apply. Strict semantics, like in ML, precludes such examples.

我不怎麼想再繼續引用下去了，因為後面還有不少。但每一篇都揭發出一些
新的東西，所以還是繼續看下去比較好... Kenneth B 說：

A lot of commenters here seem to think that the definition

data Nat = Zero | Succ !Nat

disallows “nonstandard” inhabitants, but this is obviously false.
The “strictness” annotation in !Nat just requires that the
argument to Succ be in head normal form, not
be fully evaluated. Thus, you can easily define:

loop :: Nat
loop = Succ loop

without running afoul of the “strictness” annotation. Indeed,
you can also define:

bad :: Nat
bad = Succ (Succ undefined)

and GHC will not complain about the inner Succ being applied
to undefined.

看到這裡，好似理解了什麼是 natural number 不是 natural number,
但又不怎麼明白這跟 strictness 有什麼關係。ML 應該也可以寫出這種
程式，應該也不會是 compile time 抓得到的問題？畢竟這好似 termination
check, 要 type checker 檢查這件事，則會陷入 halting problem;
然而如果強迫程式一定要 terminate, 那就不會是 Turing complete,
而且現在想到 Agda 還是會怕 XDD

will87 倒是說出了我的疑問，雖然 Rober Harper 說那是錯的：

In Haskell the strict definition of Nat means that fix Succ
(omega/infinity) is intensionally equal to _|_ (which ML types
do contain as it is a Turing Complete language, i.e. you can
write non-terminating definitions). The values which can inhabit
this type are therefore equivalent to the least fixed point of
its definition and hence are the inductive naturals, and
equivalent to the ML type.

這麼多人問了這麼多次，他總算解釋了更多：

In a lazy language non-termination is a value, whereas in an eager
language it is an effect. In particular, variables in a lazy language
range over computations, including the non-terminating computation,
whereas in a strict language they range only over values. Given a
variable x of type nat, if natural number induction were valid, you
could prove that x is either zero or a successor. This is true for ML,
but false for Haskell, because x could be “bottom”, ie the
non-terminating computation, which is a value. For this reason no
inductive type, not even the Booleans, are definable in Haskell. It is
not a matter of strictness annotations on data declarations, it is a
matter of the most fundamental level of semantics of the entire
language itself.

Umm... 也就是說，在 Haskell 中 const True undefined 我們還是會
得到 True, 就算得到了這個 term, 也不代表裡面的 Nat (undefined)
真的是一個 Nat, 或其實是 ⊥ ? 而在 ML 中，反正 const True undefined
就是 ⊥ 了，所以也不用去考慮 Nat 到底是不是 ⊥ ?

如果是這樣的話，那或許確實可以理解為什麼會想要 strict 而非 non-strict,
畢竟對於程式性質而言，non-strict 有太多可能性，似乎確實變得難以證明
許多？這一點，也可以在 Inside P4 一系列的文章中，看到考慮各種 ⊥,
真的讓情況變得很複雜。

Hussling Haskell types into Hasse diagrams

這篇我大抵上看完了，大概就是在 FLOLAC 08 10 上聽到的 domain theory
那些東西... poset, Hasse diagram, etc, etc. 大抵上我猜是有懂啦 :s
不過最後那段倒是確定不太懂：

We almost recover Nat if we set a to be (), but they’re not quite
isomorphic: every () might actually be a bottom, so while [()] and [⊥]
are equivalent to one, they are different. In fact, we actually want to
set a to the empty type. Then we would write 5 as [⊥, ⊥, ⊥, ⊥, ⊥].

啊啊啊，寫到這裡，重新讀幾次，卻發現自己好像懂了。這邊應該是在說，
如果我們讓 List a 的 a 是 Unit 的話，就可以讓 List Unit 跟 Nat 是
isomorphic 的，也就是說，5 事實上就是 [(), (), (), (), ()], 也就是
Succ (Succ (Succ (Succ (Succ Zero)))). 但事實上，因為 non-strict 的
關係，Unit 的 value 其實不只是 (), 也可能是 ⊥. 因此我們真正希望跟 Nat
是 isomorphic 的是 List Empty 而非 List Unit 了...

看來我可以安心繼續看 Gin and monotonic 了。除此之外，
還有另一篇 How I Learned to Stop Worrying and Love the ⊥

[0] 講個題外話，comment 裡有一個人，誤把作者當成初學者，不禁
開始讓我想，是什麼情況下，會導致這種錯誤的結論。大概要嘛是沒有
RTFA, 要嘛是像我一樣完全不懂他在說什麼，要嘛就是沒有連其他文章
也順便一起讀讀吧...

不過這或許也證明一件事，東西寫得太刺激，總是會吸引到一些搞不清楚
狀況的人吧？或是說，寫得隱晦一點，例如不講結論，這樣搞不清楚狀況
的人就不會搞錯狀況，就只停留在搞不清楚的階段...

*

這真的是個很漫長的路！太多太多東西現在想起來好像很單純，可是我真的
是花了很多很多時間，才慢慢對這些東西有所體會。搞到最後，真的會不知道
到底什麼東西是讓自己搞懂的關鍵，每一點自己看到的東西，自己體會到的
東西，都是拼圖的一小片。能快速理解，也只是因為過去知道或是看過類似的
東西，因此可以從半路開始爬，或是從岔路走過來，而非從頭開始走。

也就是說，其實自己也不見得真的那麼笨啦，只是浸淫的時間不夠吧...

今天聽穆老師講的東西，自己是都早已聽到爛了，不過多聽幾次好像又多有
所會。而聽自己已經懂的東西，則能有餘裕邊聽邊思索，如果要跟人解釋，
用什麼樣的解釋，用什麼樣的類比，用什麼樣的象徵來表達會比較容易懂。
多想這些其實也有助於理解和想像。

還有與 jaiyalas 聊天的過程中，點醒了我... 什麼東西忘記了 Orz
也太快就變成拼圖中的一片了吧 :s 但說真的，討論這些倒也有點像是
pair programming清談... 有時候自己會有莫名其妙的盲點，這時候
就需要旁人來戳破。

---

p.s. Existential Type 裡很多文章都讓我陷入思索，
而 Inside P4 裡的文章都寫得很清楚，還附有趣的圖解。

另外會想到的則是 Learn You a Haskell for Great Good!
雖然風格不同，但有時候我不知不覺會把他們連在一起。
這本書我覺得讀起來相當愉悅，不過這以後再說吧，值得
特別拿來說。

---

p.s.2 我好想學插圖風啊 XDD 有閒的話試試看弄個 simple and clean 的風格吧！