# 星之一角

What have you found for these years?

## 2011-05-05

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

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!

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).

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

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.

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
and GHC will not complain about the inner `Succ` being applied
to `undefined`.

check, 要 type checker 檢查這件事，則會陷入 halting problem;

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` 我們還是會

Hussling Haskell types into Hasse diagrams

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 [⊥, ⊥, ⊥, ⊥, ⊥].

isomorphic 的，也就是說，5 事實上就是 [(), (), (), (), ()], 也就是
Succ (Succ (Succ (Succ (Succ Zero)))). 但事實上，因為 non-strict 的

[0] 講個題外話，comment 裡有一個人，誤把作者當成初學者，不禁

RTFA, 要嘛是像我一樣完全不懂他在說什麼，要嘛就是沒有連其他文章

*

pair programming清談... 有時候自己會有莫名其妙的盲點，這時候

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

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