On Mon, Oct 28, 2013 at 2:12 AM, Brent Yorgey <byorgey@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