Hello, It seems there are three different ways to declare an empty type in Haskell. http://www.haskell.org/haskellwiki/Empty_type 1) data E0 = E0 2) newtype Void = Void Void 3) data Void I'd like to know how the second trick works. Is it possible to create a new type from itself? How should I interpret this? Thanks, Kwang Yul Seo
KwangYul Seo
Hello,
It seems there are three different ways to declare an empty type in Haskell.
http://www.haskell.org/haskellwiki/Empty_type
1) data E0 = E0
Perhaps this is a bit nit-picky, but is this truly empty? I would actually argue that the type is inhabited by precisely one element, `E0` (note that we aren't counting _|_).
2) newtype Void = Void Void
3) data Void
I'd like to know how the second trick works. Is it possible to create a new type from itself? How should I interpret this?
I'll try to answer as far as I understand it but someone please correct any mistruths below. Consider your type, newtype Void = Void Void There are only two ways we could construct a value of type `Void`, a = Void _|_ and, b = Void b However, `b` is a non-terminating recursion, making it equivalent to `a`. By this reasoning, since both of these constructions evaluate to _|_, `Void` must be empty. Cheers, - Ben
On Fri, Oct 25, 2013 at 10:44 AM, KwangYul Seo
2) newtype Void = Void Void
It's a Catch-22: you: So tell me how to create smth of type Void newtype: Sure, I can do that! After all, I'm the declaration of the type, aren't I? But first, you gotta do something for me. you: Ok, what's that? newtype: gimme smth of type Void --- MWAHAHAHAHA you: (trolled hard) -- Kim-Ee -- Kim-Ee
KwangYul Seo
writes: It seems there are three different ways to declare an empty type in Haskell.
Hi KwangYul, it seems someone was playing games writing that page. I suggest you look at: http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/data-type- extensions.html#nullary-types So the answer is that there is one way to declare an empty type; and it's method 3) from your OP. I agree with Ben that method 1) is not truly empty. And I like both Ben's and Kim-Ee's explanations why 2) is kinda empty and kinda not. (Trying to use Void will almost certainly make your program loop. Using method 1) or 3) won't.) AntC
On Fri, Oct 25, 2013 at 12:44:06PM +0900, KwangYul Seo wrote:
Hello,
It seems there are three different ways to declare an empty type in Haskell.
http://www.haskell.org/haskellwiki/Empty_type
1) data E0 = E0
This one is not empty, as others have pointed out. It is inhabited by _|_ and E0.
2) newtype Void = Void Void
This one is in fact empty (that is, only inhabited by _|_), but it depends on the fact that newtype constructors do not add any laziness. The same thing done with 'data', data NotVoid = NotVoid NotVoid is not empty, because it is inhabited by _|_, NotVoid _|_, NotVoid (NotVoid _|_), ... With the data declaration, these are all different. With the newtype, they are all equal to _|_. This is a bit of a technical point, however; if I were you I wouldn't worry about it at this point. It sounds like the most important thing for you to understand is below:
I'd like to know how the second trick works. Is it possible to create a new type from itself? How should I interpret this?
Yes, it is possible to create a new type from itself! This is called a "recursive data type", and they are the bread and butter of Haskell programming. For some other less silly/trivial examples, consider data IntList = Nil | Cons Int IntList data BTree a = Empty | Node a (BTree a) (BTree a) both of which are recursive types. -Brent
Not sure if this is haskell-beginners material, but it's possible in a lazy
language like Haskell to define an inhabitant of NotVoid recursively:
let x = NotVoid x in x
Or, alternatively, using fix from Data.Function:
fix NotVoid
This gives NotVoid (NotVoid (NotVoid (...)))
Nick
On Fri, Oct 25, 2013 at 5:54 AM, Brent Yorgey
On Fri, Oct 25, 2013 at 12:44:06PM +0900, KwangYul Seo wrote:
Hello,
It seems there are three different ways to declare an empty type in Haskell.
http://www.haskell.org/haskellwiki/Empty_type
1) data E0 = E0
This one is not empty, as others have pointed out. It is inhabited by _|_ and E0.
2) newtype Void = Void Void
This one is in fact empty (that is, only inhabited by _|_), but it depends on the fact that newtype constructors do not add any laziness. The same thing done with 'data',
data NotVoid = NotVoid NotVoid
is not empty, because it is inhabited by
_|_, NotVoid _|_, NotVoid (NotVoid _|_), ...
With the data declaration, these are all different. With the newtype, they are all equal to _|_. This is a bit of a technical point, however; if I were you I wouldn't worry about it at this point. It sounds like the most important thing for you to understand is below:
I'd like to know how the second trick works. Is it possible to create a new type from itself? How should I interpret this?
Yes, it is possible to create a new type from itself! This is called a "recursive data type", and they are the bread and butter of Haskell programming. For some other less silly/trivial examples, consider
data IntList = Nil | Cons Int IntList
data BTree a = Empty | Node a (BTree a) (BTree a)
both of which are recursive types.
-Brent _______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
On Sat, Oct 26, 2013 at 12:26 AM, Nicholas Vanderweit < nick.vanderweit@gmail.com> 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. 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
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 < nick.vanderweit@gmail.com> 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 Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
On Mon, Oct 28, 2013 at 2:12 AM, Brent Yorgey
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
participants (6)
-
AntC -
Ben Gamari -
Brent Yorgey -
Kim-Ee Yeoh -
KwangYul Seo -
Nicholas Vanderweit