Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: Empty type (Brent Yorgey)
2. Re: Empty type (Kim-Ee Yeoh)
----------------------------------------------------------------------
Message: 1
Date: Sun, 27 Oct 2013 15:12:03 -0400
From: Brent Yorgey <[email protected]>
To: [email protected]
Subject: Re: [Haskell-beginners] Empty type
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
On Sat, Oct 26, 2013 at 03:12:36AM +0700, Kim-Ee Yeoh wrote:
> On Sat, Oct 26, 2013 at 12:26 AM, Nicholas Vanderweit <
> [email protected]> wrote:
>
> > Or, alternatively, using fix from Data.Function:
> >
> > fix NotVoid
> >
>
> Yes, and all of them are indistinguishable from bottom or 'undefined ::
> forall a. a', the ghost that inhabits all types, including the empty one:
> Void.
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.
>
> What trips up beginners is the interpretation of indistinguishable-ness. At
> the level of denotational design, 'undefined' and 'error "(sadface)"' are
> to be treated as equal, although beginners would point out: "hey look, I
> get different output!"
>
> Call it denotational design, or call it beautiful FP modelling, this stuff
> is really where it's at.
>
> -- Kim-Ee
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
------------------------------
Message: 2
Date: Mon, 28 Oct 2013 06:10:34 +0700
From: Kim-Ee Yeoh <[email protected]>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: Re: [Haskell-beginners] Empty type
Message-ID:
<CAPY+ZdRTHWkr=sbwzenkco-6c8ag4o_gr2zzevkeus-atry...@mail.gmail.com>
Content-Type: text/plain; charset="iso-8859-1"
On Mon, Oct 28, 2013 at 2:12 AM, Brent Yorgey <[email protected]>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-0001.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 64, Issue 39
*****************************************
