[Haskell-beginners] Empty type

[Kim-Ee Yeoh]

On Mon, Oct 28, 2013 at 2:12 AM, Brent Yorgey <byorgey at seas.upenn.edu>wrote:

> No, Nicholas was using NotVoid, which I defined as
>
>   data NotVoid = NotVoid NotVoid
>
> in this case fix NotVoid *is* distinguishable from bottom. But if
> NotVoid is defined using newtype, it is not distinguishable.
>

Good catch, Brent! I was still thinking of the true, newtype version of
Void when I wrote the comment.

For the gallery:

Let's define omega = fix NotVoid.

This distinguishability (or apartness, to use the more google-able term)
Brent speaks of is only semidecidable. And the case for omega is even worse!

E.g. How would you write an instance of Eq, i.e. (==) :: NotVoid -> NotVoid
-> Bool?

What you _can_ do is write a function isNotBottom :: NotVoid -> Bool that
returns True when the case applies. It'll never return False. That's what
semidecidability means.

It's better to call isNotBottom as isAtLeastBottomPlusOne.

(Popquiz: what's isAtLeastBottom and how would you write it in idiomatic
Haskell and why is it un-contributive to the discussion?)

Because then we'd see right away there are isAtLeastBottomPlusTwo,
...PlusThree, etc.

Main course:

I detect at least two senses in which the sentence "omega *is*
distinguishable from bottom" is misleading. First, normal English usage of
'distinguishable' is symmetric: if A is d-able from B, then so is B from A.

But here it's NOT! (Try writing isNotOmega.)

The other snare is that there's an expectation (because that's the whole
point of d-ability), that if A is d-able from B, then that act of
distinguishing has got us /closer/ to ascertaining A.

Again, not really. Within Haskell, knowing that a candidate
isAtLeastBottomPlusX only tells us that it could be still any of an
infinite number of possibilities!

Restated another way:

(1) Omega is distinguishable from /any/ one of its infinite approximants.
Because of asymmetry, the reverse isn't true.

(2) Omega is /not/ distinguishable from /every/ one of them.

So you can't even write crippled, one-legged versions of neither isOmega
nor isNotOmega !!!

Omega is truly more voodoo than the rest, which admittedly are already
pretty wild as far as Haskell data goes.

All this sounds like a cardinal case of academic wankery so notorious in
the community. Trust me, it's not. It's a price to pay for equational
reasoning (among other design points). Stuff like this rears its head once
you get deep into FRP, etc.

-- Kim-Ee
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20131028/fd7b2367/attachment.html>