Should we rename Void and Bottom?

[FroMage]

We find that Void (the top of the hierarchy) is not adequatly named, since it conveys the idea that it can only point to nothing.

Similarly we find that Bottom (the subclass of every type) is confusing for those unfamiliar with the notion (everyone except ML guys).

We proposed the following alternatives:

• Top/Bottom
• Unknown/Impossible
• SuperType/SubType
• Anything/?
• Defined/Undefined
• Value/NonValue

Note that undefined is a valid value in many languages and would therefore be confusing.

[tombentley]

As for void functions, returning top is different from returning unit or not returning anything. In particular, not returning anything has different stack behavior than returning something. I don't know what the performance consequences of that are, though. As for returning unit versus returning top, unit has well defined operations on it such as equality, whereas top does not. If top did, it'd be something like .string, in which case the values for top are distinguishable, so reasoning about correctness would be very different for top and unit functions.

FTR, the semantics of void methods are described in ceylon/ceylon-compiler#538.

[quintesse]

assuming google shows you the same thing as me

I get videos and lyrics of a song with that name by Dramarama ;)

[ikasiuk]

I get videos and lyrics of a song with that name by Dramarama ;)

Do they make any statements with regard to the semantic interpretation of "anything"?

[RossTate]

Well, the discussion comes down to an English-usage question, so I googled that phrase and all the uses had the opposite meaning of what y'all are using. I asked a bunch of students in class today about List<Anything>, and most had your interpretation, but some had the other interpretation, and then when discussing which is right they just got really confused because they were talking about an ambiguous term. Also, the proportions swap when I ask about Anything.

I don't know how else to give you evidence of ambiguity. What I do know is that Thing is pretty unambiguous, and I haven't heard much about that.

[quintesse]

I don't think Thing is unambiguous at all, starting with myself, so there must be others :) Ask your class if they think this is allowed in the type system which has a Thing:

Thing x = ...
if (exists x) { ... }
if (is Nothing x) { ... }

To me a "thing" is something, it can't be nothing, it can't be just anything.

And people "getting it right" intuitively (as did most in your class) seems very valuable. If you start thinking about semantics too much there are many things in life which become confusing ;) After so many discussions here I doubt we'll ever come up with a term that will satisfy Everyone (Everybody).

Also, the proportions swap when I ask about Anything.

Wdym?

[RossTate]

That's why I proposed Nothing for bottom and Null for null. Is Thing still unclear after that change?

As for swapping proportions, I mean more peoples' intuition Anything corresponded to bottom than to top, whereas more peoples' intuition for List<Anything> corresponded to list of top than to list of bottom. That is intuitive meanings varied depending on context.

[ikasiuk]

I don't know how else to give you evidence of ambiguity. What I do know is that Thing is pretty unambiguous, and I haven't heard much about that.

To be honest, Thing to me sounds like "couldn't think of a name". Not really better than Foo or so.

My impression so far: there is no perfect name for the type at the top of the type hierarchy (and probably also for the type at the bottom of the type hierarchy) because it can play different roles and look different depending on the perspective. Anything (or maybe Any) is still by far the best suggestion so far - perhaps exactly because the word is somewhat ambiguous.

The nice thing about Anything and Nothing is that (in my opinion) they have a reasonable chance of conveying roughly the correct meaning at first glance to someone who doesn't have much knowledge about type systems. And that's exactly the audience we should aim for! Of course you can and will find ambiguities when you look a bit deeper. But I don't think that can be avoided with any name we can possibly pick. In the end you just have to learn and accept the meaning of these type names, whatever they are.

The only alternative is to take something much more abstract, like Alpha and Omega or so. But I really don't think that's better.

[quintesse]

Is Thing still unclear after that change?

I'm assuming Anything/Nothing and Null here. Of course I can learn that Thing is not an actual thing but more of an Idea, but I can already see myself explaining this to newbies: "this Thing here, it doesn't need to be an actual Object, it can actually be anything you want, any type is assignable to it". The word "any" keeps cropping up (is that why they call it Any in Scala?)

I mean more peoples' intuition Anything corresponded to bottom than to top

But how can Anything be considered to be bottom if we already have Nothing for that? Would they still confuse Anything with bottom when they know that? If they do we would have a problem with Nothing as bottom as well I should think.

Anyway, I guess this is about people who actually know what Top/Bottom etc means, which is a small minority of developers out there.

(edit: changed "anything at all" to "anything you want")

[quintesse]

The only alternative is to take something much more abstract, like Alpha and Omega or so. But I really don't think that's better.

Well IMO that's basically what Void and Bottom are right? They have meaning because type system experts gave them meaning, not because of much else (you can explain how they came to use those words, but you could probably come up with explanations for Alpha en Omega as well, begin - end).

[ikasiuk]

Well IMO that's basically what Void and Bottom are right? They have meaning because type system experts gave them meaning, not because of much else (you can explain how they came to use those words, but you could probably come up with explanations for Alpha en Omega as well, begin - end).

Yes, exactly.

[RossTate]

Good point that Anything would be less ambiguous in the context of Nothing as bottom. I tried to place my question with no context.

Also, I asked non-type-theorists. They're just students who had never heard of things like top and bottom.

Note, the phrase "can actually be anything" is ambiguous, which is why you added "at all". If you'd added "you want" then it would have the opposite meaning. If I were to ask you "Can you be anything?", what would you answer? If "no", then you're interpreting "anything" as bottom. Merriam-Webster give a bunch of example uses of "anything", and they take on both interpretations depending on context: http://www.merriam-webster.com/dictionary/anything.

Lastly, I still don't get why you say Thing is not an actual thing. If you have a Thing you have a value, such as null or some object. It would be completely possible to implement Integer asBits(Thing) in the compiler, though whether we'd want to provide that is another question entirely.

That makes me think of some alternatives if people really don't like Thing, such as Value or Datum.

[quintesse]

which is why you added "at all"

no actually, that was my mistake and something I must have been doing it wrong for a looong time. I always have this example in mind "you can ask for anything you want, anything at all", but obviously that's just wrong, it's used for "if there's anything you want anything at all come to me", where of course instead of something all-encompassing it means the least-encompassing, which isn't what we want. But the confusion is mine and only because of the addition of "at all" which I shouldn't have mentioned.

and they take on both interpretations depending on context

where? They only times I see that is when the rest of the sentence is a negation, all the other examples seem to say exactly what you'd expect "you can say anything", "the dog will eat anything", "he'd do anything".

If you have a Thing you have a value, such as null

Maybe that's the real issue here, for me null isn't really a value, it's an absence of value (which, to me, is why right now it's type is Nothing and a type like T? is called "optional"). If we do consider it a value then I don't see why we have two different branches: Object vs Null/Nothing.

[RossTate]

"I'd do anything [she (the environment/consumer) wants] to see her again." - bottom usage "If you're not sure what to say, just say anything [you (the actor/producer) want] that comes to mind." - top usage

As for null, I understand your intuition, but null is a value, at least from the mathematical perspective. It's bits are (typically) all 0s. If null weren't a value, you wouldn't have to reserve the 0 address.

[shelby3]

Regarding RossTate's point, I wrote before:

https://github.com/ceylon/ceylon-spec/issues/186#issuecomment-9058312

"All could be confused with Any because the user could assume all types can be assigned to it, instead of it can be assigned to all types. Ditto Any vice versa."

So the example of Anything being (thought to be) bottom is that the user tries to assign a member of List<Anything> to any variable of any type.

So I agree with RossTate that Anything is ambiguous.

As I pointed out in my prior above linked comment, Nothing can be easily confused with null and unit. Some users will think of that a void (unit) function returns nothing because the return value is discarded in the code (when in fact from a type theoretic perspective it returns the single instance of unit). Others will think of a null as being equivalent to nothing.

Additionally, Nothing does not convey the contravariant relationship for the empty list List<Nothing>. When I first saw that in Scala and wasn't yet familiar with the bottom type, I was very confused.

When used as return value for functions that never return, I think Never is much more clear because it is distinguishes "functions the never return" from "functions that return nothing".

When used to express contravariant subtyping relationships, e.g. the empty list, I think SubOfAll is much more clear (than Nothing or Never), and I can think of no other name that will make it easier to express those contravariant subtyping, without causing other confusion (and ambiguities). However, I suppose I could agree to List<Never> and the user would just have to go learn that Never is the subtype of all types.

In my prior comment, I had suggested giving bottom two names and let the user decide which name to use depending on the context. I said in the prior paragraph that I could agree to one name Never.

---

THIS SECTION OF THIS POST IS ERRONEOUS. SEE COMMENT I MADE BELOW.

Another reason to prefer two names for bottom is that when a function ONLY returns Never, then we don't want Never to be the bottom type, because we don't want it to be assignable to any type. However, when a function returns an intersection of Never and other possible return values, then we want Never to be the bottom type, because we want to be able to assign the function to those other possible return types. However, we really don't want it to be bottom either, because we don't want to allow assignment of the function to any type (which is what bottom can do).

So I guess I am also doubting the type theory, that says bottom is the correct type for a function that never returns.

It seems to me that Never should be a type that is only assignable to the other types it is intersected with. Thus it isn't bottom. Am I proposing to create new type theory?

---

As for the top and bottom type names, the only unambiguous names I can think of are SuperOfAll and SubOfAll.

The Any..., Every..., and All... names are ambiguously top and bottom simultaneously as explained above (depending whether the any and all is thought to be the source or the destination).

The Thing or Object may work for a top type, but it confuses the user between a type that can't be instantiated (i.e. top) and those that have historically been an instantiable class (e.g. Object).

I assume you all do not like SubOfAll because it is not simple and memorable?

I also like the suggestion for top made in the very first post, Unknown / Impossible. That is very clear at least for top. The top type holds an unknown type. It is less clear for bottom, because although it is true that bottom is impossible to instantiate, void also can't be instantiated, and that doesn't say anything about it being the subtype of all types.

[shelby3]

Three types.

1. Top: Unknown
2. Bottom: Every or EveryType or Universe
3. Non-termination: Never

1) Unknown is clear that it can contain any type (but not known until reflection or type introspection), but it can't be assigned to any type.

2) The definition of every says that every member is included without exception, thus EveryType or the Universe can not contain any finite set of type(s), yet it can be assigned to any type. Since it can't contain any finite set of type(s), it is thus implied it can't be instantiated (i.e. can't have values). Since it can be assigned to any type, then it is implied it is the subtype of all types. I suppose my favorite is Universe, as it is very memorable and no other language (I know) has used it and because Every... might suffer the ambiguity that I and Ross previously explained.

3) In my prior comment, I explained that non-termination is not the bottom type. Never is clear that the return type never occurs.

My choices are:

1. Top: Unknown
2. Bottom: Universe
3. Non-termination: Never

[RossTate]

Never could work for me as bottom. It has a bit of the same problem as Impossible, but not so bad.

I don't like your separation of bottom and non-termination. The whole point is we need a bottom, say for expressing universal lists (i.e. the empty list is a list of anything) or for inferring unconstrained type arguments.

The problem with SubOfAll and SupOfAll is they convey no intuition (outside of type theory).

As for things like Every, EveryType, All, and AllType, it is impossible to feed a consumer of bottoms, but it sure sounds possible to feed a Consumer<EveryType>. As for Universe, everything is in the universe, so that makes just as much sense to be top.

Unknown I don't think works for two reasons. First, List<Unknown> is usually how I'd describe List<?> in Java, which is different. Second, Consumer<Unknown> sounds like you can't feed it cuz you don't know what to feed it, but in fact you can feed a consumer of tops anything.

The Thing or Object may work for a top type, but it confuses the user between a type that can't be instantiated (i.e. top) and those that have historically been an instantiable class (e.g. Object).

That may work as an argument against Object (though I don't think I've ever said new Object(), and besides it's unnecessary since Object cannot be top in Ceylon), but there is no precedent for new Thing().

So, I still think these are the remaining viable options from all the ones I've heard: Bottom - Nothing, Never Top - Thing, Value, Datum

[shelby3]

Ross,

1. My suggestion was to use bottom for "expressing universal lists (i.e. the empty list is a list of anything)..." but not for expressing non-termination. I did not suggest eliminating a bottom type. I explained why I think bottom does not work for non-termination in type theory logic (I have not cited any research), i.e. essentially to not conflate subtyping and non-termination.
2. Agreed Sub... and Super... convey no intuition other than the subtyping relationships. They are the most direct to the point, if we want users to be aware of the subtyping relationships that give rise to the overall semantics, e.g. empty list List<Bottom>.
3. I will agree with your point that intuitively it is possible to assign any type to a member of List<Every...> or List<All...>. Any inclusive name would suffer this, including Universe. Thus, can not express the subtype relationship of bottom intuitively, and must use Sub.... Else we are left with some name that only applies to some uses of the bottom type, e.g. Empty, NoValue, Never, Nothing, etc.. I don't think there is any such non-subtyping name that will fit intuitively in all cases.

4. The argument for Universe is that unless you want the users to be ignorant of subtyping relationships, then they are going to need a name which means it has all the types simultaneously (thus can't be instantiated and is the subtype of all types). If you attempt to make them ignorant of subtyping relationships, then why even show them the library source code for a List? Just give List<Bottom> an alias such as Nil, which the user will recognize.

   I favor Universe over EveryType, because the former intuitively implies everything is contained in it, whereas the latter could be misinterpreted as "every type is allowed". If the user reasons that a type that contains everything can't be any one type, then they got it. If they reason that Universe can be any type, then they have not reasoned that the universe "contains everything all the time". Can someone reasonably intelligent reason that a universe is "just some things some of the time"?

   I also like Universe more than SubType or Every... because the extent of the Universe is infinite, as is the bottom type. I suppose SubOfAll also implies it is infinite for all possible types.

5. List<Any> can more clearly be fed any type than List<Unknown>, but Any has the ambiguity of being top or bottom as we discussed previously. List<Thing> looks like a list of the single type Thing (instead of a top type) and thus suffers the same problem as Unknown. At least Unknown does not suffer from ambiguity and it is correct that the type of the List is unknown (until reflection or type introspection). The user is going to ask themselves what is the point of putting only Unknown types in a collection. Then the only possible reasoning is to cast any type to Unknown.

   And this is not a valid criticism in Ceylon, because of the first-class intersection type, then almost never should the user cast away the types and employ List<Unknown>. The List<Unknown> is a type hole from which runtime exceptions can occur. It should not be used. I think Unknown helps to make this danger more explicit.

6. In my opinion, Thing, Datum, Value are too specific to be intuitively a top type. They don't imply generality. For example, a Thing is a Volkswagen too, and a Value in Scala is not a boxed object. And we documented that all the universal names are ambiguous. Thus afaics only Unknown remains. And the criticism against Unknown doesn't apply when there is a first-class intersection type.

7. For the bottom type, I think it is first important to decide if non-termination will be a separate type as I suggested. If yes, then I have argued that a name which conveys the subtyping relationship is best. If you want to hide subtyping from the user, then just give the List<Bottom> as alias, e.g. Nil.

   So if you prioritize subtyping understanding, then Sub... or Bottom or Universe is preferred. If you prioritize some intuitive use cases of bottom, then Empty, NoValue, Never, Nothing but then you lose understanding for the person who is trying to figure out what the subtyping code does (which is crucial to understanding the design of the code). I was confounded by use of List[Nothing] in Scala when I first encountered it, because I did not know that Nothing was the subtype of all types. I was thinking it meant null, and I was perplexed as to how the code could compile.

   If bottom will only be used as a type parameter (assuming we make non-termination a separate type), then it will always have an alias, e.g. List<Bottom>, thus library designers can give those use cases more intuitive aliases, e.g. typedef List<Bottom> Nil.

8. If we must choose between Nothing and Never, I prefer Never, because the bottom type is definitely not nothing. It is the subtype of all types, and that is an instance that can never occur, i.e. populated by all types but no values. Nothing is like null (a empty placeholder for something and the "$billion mistake"), and imo Ceylon is more correct than Scala on that.

   http://en.wikipedia.org/wiki/Tony_Hoare#Quotations

[RossTate]

I think I've figured out what bugs me about arguments like "They don't imply generality." Generality is a consequence of its position in subtyping and variance. In particular, it's an application of cool quirks of the type system. But a type should not be named by a application of it. After all, in the case of top and bottom, their applications swap places depending on whether they are used in covariant or contravariant locations. So while List<Unknown> may make sense because Unknown is in a covariant location and is named with that in mind, when you put Unknown in a contravariant location such as Consumer<Unknown> then the intuition backfires.

Rather than focusing on application, focus on inhabitants, as has been the norm in OO. For example, Object is top in many OO languages, yet they don't call it Top or Anything because those aren't the inhabitants. All objects belong to Object, and all inhabitants of Object are objects.

Now, in Ceylon, Object is not top because not everything is an object. Still, all things/values belong to top, and all inhabitants of top are things/values. Hence I think good names for top are Thing and Value.

As for bottom, no thing belongs to bottom, hence I think Nothing is a good name for bottom. As you point out, this term is conflated in OO world, but at least I'm being consistent with my naming scheme. Nothing is particularly great of Thing is chosen for top. Interestingly, a list of nothing is the empty list. Now, Never may work as well for the reasons you pointed out, but it's not even a noun, so it's kind of weird (though the situation is weird and so weirdness may be called for). As for Universe, one would expect its inhabitants to be universes. In fact, there are languages with universes, so to me Universe really doesn't fit.

I don't see any reason for a separate type for non-termination. At the least, can we move that to another discussion?

[shelby3]

THIS POST IS ERRONEOUS. SEE COMMENT I MADE BELOW.

From discussion of this on scala-language, let me clarify why I think the bottom type is not correct for non-termination:

The bottom type doesn't have any value. A function which returns the bottom type, therefore, cannot terminate (unless you consider throwing an exception to be termination).

Afaics, that is not a sufficient condition to make the non-terminating return type equal to the bottom type, because there are other problems with doing so.

The problem is that the bottom type is the subtype of all types in the universe (including those types outside your own program), thus a function returning bottom can be assigned to any type, which is incorrect, because it never returns.

And if the return type is an intersection of bottom and some type(s), then we don't want to be able to assign it to any type, but only to those other type(s).

Thus bottom is not the correct type for non-termination.

[shelby3]

Ross that was an excellent argument and almost swayed me to your preference. However, Unknown is still going to be an unknown type in the contravariant position, and Object will still be an object. I don't see an advantage.

Afaics, your argument reduces to Object is better than Unknown as a general container type for all types, but Object is an approximation for top in languages (e.g. Java) that have subtyping but don't an unknown type that can't be instantiated. The key is that unlike for Object in for example Java, in this proposal there is no object of type Unknown, i.e. new Unknown is illegal. Unknown hides the type of the object-- the type is still there via type introspection (reflection).

So although Object (or less generally so Thing and Value) works from the standpoint of being a general container for any type of object, they to seem to lean towards implication that they are instantiable (and can be optionally down-casted). And Unknown is more explicit that the type or the actual object has been thrown away and that down-casting is required to access the object.

I guess what I am suggesting is that we want to discourage users from unnecessary use of the top type-- to use it with caution. I like the scary name, because downcasting is a type hole. And from that type theoretic and user error standpoint, Unknown seems more correct to me.

I do understand that your opinions will decide, not mine. I am just trying to help give feedback. I am thinking about this, not just for Ceylon but for Scala and any other language I might be involved in. I found the use of Nothing very confusing when I first encountered in Scala as a novice. I am a reasonably smart person, so that was frustrating that I had to go searching the Scala site for the definition of Nothing (after being unable to reason how "nothing" could compile in the contravariant position of a List<T>) and then found out for the first time there is such a thing as a bottom type.

I was originally okay with the use of Any in Scala, until I started to think about a better name for Nothing, then I discovered that All (and Any) could be ambiguous with top and bottom, as you have noted too. Then since I discovered Scala's implicit subsumption, and the problems it creates, and then got into the need for an intersection type to avoid runtime type holes, I became more aware of the evils of Any being promoted as type to use.

http://stackoverflow.com/questions/8360413/selectively-disable-subsumption-in-scala-correctly-type-list-contains

Bottom

Since I don't find Thing to be better than Object or Unknown, then I don't find the disadvantages of Nothing are outweighed by that suggested symmetry (clever idea though). I would be more enthusiastic if that symmetry implied a subtyping polarity, but it seems it just implies a polarity w.r.t. to #2 quality below (which is not the most important quality).

The problem for a name of bottom is that bottom has two qualities:

1. Populated as the subtype of every type in the universe (including those not in your program).
2. Is never populated with values, never instantiated.

So the choice of Never addresses #2 without eliminating #1 (and a noun like Nothing doesn't work because it eliminates #1).

SubOfAll and Universe address #1 and also by reasoned implication address #2 also (impossible to instantiate the entire universe or a type which is the subtype of itself).

Note that List<Bottom> is not required to be empty by quality #2 (no where will you find the oxymoron of non-instance of the bottom type declared), rather it compiles because of #1 and the semantics of it representing the empty list are arbitrary.

I was preferring Never for a separate non-termination type, but I can live with making the bottom type so as to emphasize quality #2, even though that is not the quality required to understand the code for List<Bottom>. It just feels hacky, because is just coincidence of how List<Bottom> is used as a placeholder for the empty list. We could create a List<Bottom> that has a field that is an index into the list. The semantics are arbitrarily chosen to be the empty list. It has nothing to do with the type parameter being Bottom, except that we can't directly reference any member, because Bottom does not contain any values, yet we could reference an index into the list. So yes, I can live with Never for bottom, but I don't think it is most direct to the point intuitive for understanding the code.

And for hiding the true meaning of bottom in libraries, we can use an alias such as Nil. Thus I argue to emphasize the #1 quality of bottom, since only library designers are going to be looking.

[shelby3]

Direct to you my comment early in this thread for more problems I have with Nothing (and even Never) as a bottom type:

https://github.com/ceylon/ceylon-spec/issues/186#issuecomment-5468214

The point is that the List<Nothing> implies that the empty list can not be instantiated, or at least that it can not be assigned to List<T>, e.g. it implies that that List<Int> v = new List<Nothing> is illegal.

You see you really have to emphasize the subtyping quality in order for the code to make any sense. That is why Nothing totally blew my mind. Without the subtyping understanding, none of it makes any sense.

Never works as a separate non-termination type though.

[FroMage]

I could live with Top = Something and Bottom = Nothing, and honestly I can also live with Top and Bottom :)

I find Thing disturbingly short and it seems like a half-assed name chosen in haste at random (even though I agree it's not and you have very good reasoning behind it, but people don't necessarily know).

[shelby3]

Disregard my erroneous assertion that a return type of type bottom can be assigned to any type. Obviously the compiler should warn that bottom can't be populated with any values, thus the return value can not be assigned to any type.

I got myself confused with the assignment of List<Bottom> to List<T> for any T.

So now we are back to choosing a name for bottom that can apply to both return values of non-terminating functions and other usages, unless we wanted to allow two names for bottom (admittedly a weird idea).

I don't think this invalidates the points I made about Universal for bottom. And obviously doesn't impact the points I have made about a name for top.

[RossTate]

@FroMage: What about Value?

[shelby3]

@FroMage: what does List<Int> v = new List<Nothing> mean intuitively (without exploring the subtype relationships which Nothing does not intuitively convey any way)?

How can one intuitively assign a list of members of Nothing to a list of integers, without understanding the subtyping of contravariant type parameters?

This is why I argue that it is not going to make any sense unless the user either understands that bottom is the subtype of all types, in which case better to not name it Nothing because how can nothing be populated by all types?

And/or you give the user an alias, e.g. Nil or EmptyList, then it is intuitive List<Int> v = Nil.

And how is returning Nothing intuitively distinct from return null?

I am just wondering what you thought of my points and still arrived at choosing Nothing.

Universe is very wrong as it supposes that it contains everything. Whereas bottom contains nothing.

Bottom does contain everything, when it is used only as a type. Bottom only contains nothing when it is used to instantiate a value, because it can't be instantiated.

The more I think about it (from a theoretical physics standpoint), bottom is the whole unbounded (infinite) universe, but not any part of it. This is why it (the universe as a whole) can't be instantiated, but it can serve as a unbounded quantification in type parameter relationships.

We know very well that unbounded quantification exists in every Turing machine (a Turing machine is unbounded recursion).

I understand from the cited paper, that the point of top and bottom is to give us types that let us express unbounded quantification. Obviously unbounded types can't be instantiated, they can only be used to express relationships where the lack of a bound is congruent in the logic.

[quintesse]

@shelby3 Actually you can! Just that at the moment it gets executed you'll get a runtime error. It allows for things like:

String foo() {
    return bottom; // Not implemented yet
}

@RossTate I still feel Value is pretty much similar to Thing, especially because I don't consider null to be a "real value", like I said before, if it is then I don't see why we would have a separation between Object and Nothing (or Null if we'd use the new name).

Datum would seem sufficiently strange so as not to have too many wrongful connotations, but it has the disadvantage that it does not seem to have anything to do with the other side of the coin: Nothing. Besides I'm pretty sure that for many people not familiar with Latin you could just as well write Alpha or Omega (like @ikasiuk said before).

I have a similar problem with shelby3's Unknown, although at first it sounds pretty reasonable, to me it at falls flat when putting it next to Nothing. I'm pretty sure that when confronted with a combination of Unknown and Nothing people will have to think hard as to what is what and possibly get really confused.

This way I'd rather keep Bottom and introduce Top because that would at least have the advantage that, although not intuitive at first glance, they'll be very easy to explain to people that know about class hierarchies.

[shelby3]

I explained briefly at the following link that exceptions leave the program in an indeterminant state:

http://groups.google.com/group/scala-language/browse_thread/thread/22bfb3666b1ac43d/76dfac9ba1f93ebd?#76dfac9ba1f93ebd

Thus if it were my language, I would discourage the use of exceptions and I would not prioritize the name of bottom based on its rare use for non-terminating functions.

[ikasiuk]

@FroMage: what does List<Int> v = new List<Nothing> mean intuitively (without exploring the subtype relationships which Nothing does not intuitively convey any way)?

Firstly, it means a syntax error because of the new ;-) Apart from that I find this very intuitive: v is an empty list, obviously! What else should a "list of nothing" be?

This way I'd rather keep Bottom and introduce Top because that would at least have the advantage that, although not intuitive at first glance, they'll be very easy to explain to people that know about class hierarchies.

While Top and Bottom are surely better than some other suggestions in this thread, I would prefer something that works well for people how don't have much knowledge about type systems.

I'm getting more and more convinced that Anything and Nothing are the most reasonable choices.

[quintesse]

@shelby3

then it is intuitive List v = Nil.

This is exactly what is being done, only it's called Empty. But of you go and look at it's implementation you'll find that it refers Bottom.

I would discourage the use of exceptions

But then we would have a completely different language. And personally I'm glad we have them, because I can still remember programming in assembler and C without it and boy I don't want to get back to that ;)

The more I think about it, bottom is the whole unbounded (infinite) universe

That's just how you look at it, if it's bottom then the whole unbounded universe can be found inside a single (impossible) type while for top the whole unbounded universe consists of the set of all possible types. So this definitely depends on your POV (which is why Universe is so ambiguous, you see it as bottom while I think more people think of it as top).

[shelby3]

@ikasiuk: thanks for sharing your POV.

Firstly, it means a syntax error because of the new ;-)

I did that on purpose to make the point that how would you know not to use new? You know that because you've already familiarized yourself with the library design of List. And this follows to my next point...

Apart from that I find this very intuitive: v is an empty list, obviously! What else should a "list of nothing" be?

A list of members of type Nothing. How would I think otherwise, if I did not know the design of the library for List?

Think about it coming from C++ or Java, why would I think that Nothing was special and that List<Nothing> was not a case of List<T>?

And how could I assign a list of members of type Nothing to a list of members of type Int? Didn't make any sense to me. Then I started to study the contravariant type parameter and the special singleton for List[Nothing] in Scala, and I was confused as to how Nothing could be a subtype of any type T.

Nothing was very non-intuitive for me in the normal progression of the learning curve. It didn't imply an empty list based on what I expected about type parameters in collections and it didn't also tell me how it could be a subtype of all types, when I studied the library design and learned about contravariance declared at the definition site.

The only time it clicked is when I discovered that Nothing is bottom in Scala. So the name never helped me. After I knew it was bottom, then it sort of made sense that List[Nothing] is an empty list, but by this time it really didn't matter what the name is (and I still have to memorize that Nothing does not mean it contains no types when used as a type, and remember that the bottom type does).

I would prefer something that works well for people how don't have much knowledge about type systems.

Agreed, and that was my case (experienced in C, C++, PHP, Haxe) when I started learning Scala. And I found Nothing did not make any sense, per the logic I presented above. I don't know if my mind works different than most people, but I was proceeding based on what (I know) a parametrized type does in other languages I know.

[shelby3]

@quintesse:

I would discourage the use of exceptions

But then we would have a completely different language. And personally I'm glad we have them, because I can still remember programming in assembler and C without it and boy I don't want to get back to that ;)

At the link provided, I briefly explained (what I believe to be) a more determinant solution that does not go back to the hassle of assembler and C:

http://groups.google.com/group/scala-language/browse_thread/thread/22bfb3666b1ac43d/76dfac9ba1f93ebd?#76dfac9ba1f93ebd

I have suggested (not tried extensively in real world yet) elsewhere that it is better to declare the input type of p: UInt and push the exception out to the caller before being called, or return an error value and let the caller clean up to a determinant state. The further up the nested function hierarchy that the exception is caught, the more likely the program is an indeterminant state.

I have a link to a long debate about that, but I would rather try this idea in the real world and prove it is viable.

I am not saying all exceptions can be eliminated, but the goal is to use types to anticipate and replace exceptions.

I think the above can be done in Ceylon, as it is just libraries and user choice.

[ikasiuk]

I did that on purpose to make the point that how would you know not to use new? You know that because you've already familiarized yourself with the library design of List.

How does the syntax of the language depend on the design of the List interface?

I don't know if my mind works different than most people

Well, it obviously works very different than mine, but that's not necessarily a bad thing :-) BTW, I also come from C++ and Java.

Think about it coming from C++ or Java, why would I think that Nothing was special and that List<Nothing> was not an case of List<T>?

That argument is valid independently of the name we choose for the bottom type! The concept of a special bottom type is something that inevitably takes a moment to understand, no matter what name we choose. To me at least, Nothing is a name that somewhat helps this understanding - it is not too hard to accept that a "list of nothing" must be empty. And IMO that's simply as good as we can get: there is no name that immediately conveys this whole abstract concept.

I think the above can be done in Ceylon, as it is just libraries and user choice.

If you want to continue that discussion then please move it to a separate thread. This one's complicated enough as it is :-)

[shelby3]

@quintesse:

The more I think about it, bottom is the whole unbounded (infinite) universe

That's just how you look at it, if it's bottom then the whole unbounded universe can be found inside a single (impossible) type while for top the whole unbounded universe consists of the set of all possible types.

Indeed, you have reaffirmed my point.

Top and bottom are all about unbounded quantification.[1]

[1] Google the cited research paper: http://en.wikipedia.org/wiki/Bottom_type#cite_note-bounded-0

But the key is that all infinite possible instances of top is the universe set (an instance of top is never the entire universe), yet bottom can't be instantiated. Thus any single instance of top can't be the entire universe, so we can't name top Universe (it never refers to the entire universe). But bottom can be named Universe because it is never instantiated and thus it is the entire universe.

From a physics POV, top is analogous to the relative observer (and note the reality of all other observers is unknown until observed), and bottom is the entire universe.

So this definitely depends on your POV (which is why Universe is so ambiguous, you see it as bottom while I think more people think of it as top).

Top can't be the entire universe, because it references specific instances (parts of the universe).

I can't see an ambiguity.

[shelby3]

@ikasiuk:

How does the syntax of the language depend on the design of the List interface?

I am not 100% familiar with all nuances of Ceylon syntax (new is I guess never needed). I was thinking of how in Scala or Java (or other languages), that new would be needed, unless we had defined a singleton for the empty list, e.g. Nil or Empty.

That argument is valid independently of the name we choose for the bottom type!

Agreed.

it is not too hard to accept that a "list of nothing" must be empty

Yes I figured that was the way you were thinking about it. That may help memorize an empty list syntax, but in my prior reply to you, I explained that during the learning process, I needed to know that Nothing was the subtype of all types, in order to know that List<Nothing> was not a "list of members of type Nothing" and was instead of "list of no members or empty list".

I am making the point that during learning, the fact that the bottom type is the subtype of all types, is more important than memorizing what an empty list is. And we will never see List<Nothing> when we use it, because we have Empty or Nil. The only time we need to see List<Nothing> is when we are learning how the library for List is programmed. And at that stage of learning, afaics the most important thing is to know that we have a bottom type and that the bottom type is the subtype of all types and thus works in that contravariant position.

But of course that was only one person's experience.

I understand Nothing is more intuitive (than other choices, except for perhaps Never) for the return type of non-terminating functions. So this is probably an overriding reason to say it all fits with the choice of Nothing.

Then I say I would discourage exceptions, but afaik that is not (yet) the consensus in the real world.

So I understand your POV.

However, I still find that Nothing is incorrect. The bottom type is populated with all types in the universe, not nothing.

[quintesse]

However, I still find that Nothing is incorrect. The bottom type is populated with all types in the universe, not nothing.

@shelby3 I don't agree. Top is "populated with" (contains) all the types in the universe, Bottom is all the types in the universe.

But we're more and more going from "type theory" to "type philosophy" and further and further away from the needs of the "common developer" that just wants to get his work done.

This means the names we choose should be:

1. Intuitive - as much as possible, but not to us but to the majority of people that have no or little knowledge about type systems (which will be 99% of our audience)
2. Easy to learn/teach/explain - when point 1 is not enough
3. Theoretically sound - a far third, the names we choose should not be completely wrong, but it doesn't matter if there's some ambiguity as long as points 1 and 2 can take care of that

[ikasiuk]

I am making the point that during learning, the fact that the bottom type is the subtype of all types, is more important than memorizing what an empty list is.

Exactly, it's the subtype of all types and therefore represents the intersection of all types, which is empty (wrt the contained values). That makes Nothing a fitting name. Yes, that's only one possible point of view. But I think it's the most reasonable point of view if we keep in mind that we are not designing this language for people with a type theory background.

[quintesse]

@ikasiuk Which actually fits quite nicely with Ceylon's view on "unions" and "intersections" that is also based on sets and not structure

[RossTate]

I still feel Value is pretty much similar to Thing, especially because I don't consider null to be a "real value", like I said before, if it is then I don't see why we would have a separation between Object and Nothing (or Null if we'd use the new name).

null is a real value, especially in Ceylon. After all, what is the value of x after value x = null;? What's confusing you is that not everything in Ceylon is an object, which is why Object and Null are separated. Indeed, there are languages where null is an object. Orthogonally, it can actually be quite useful to have many null values because then you can track where an unexpected null value came from in the code.

So, given value x, any type that can be inferred for x makes sense to be a subtype of Value, making Value top.

(Note that in the case of value x = bottom/error/non-termination the variable x is never assigned a value since the actual assignment is never actually reached, so it makes sense for the inferred type of x to be Nothing.)

[shelby3]

I agree with quintesse's 3 priorities.

Let me number them as you did.

1. I just don't agree that novices will think of Nothing in terms of the logical conjunction of all sets, where types are sets. Most of them never even heard of the Liskov Substitution Principle, much less it being explained clearly with subtypes as narrower sets.

   For me before, Nothing meant null. Period. As it is currently in Ceylon, which is thus gives weight to it being the obvious meaning for newcomers.

   Thus Nothing as null hinted nothing to me about a subtype relationship.

   From a novice's mind, if the Universe "contains all types", what type would the universe be? Hmmm. It obviously can't be any one type, because some of the types contained in it are mutually exclusive.

2. That hints a lot more to me about the qualities of bottom. It gets me thinking that the Universe can't be a single type, thus can't be instantiated.

3. This is because it IS the logical conjunction of all types. Yet it does also CONTAIN all types even though itself it can't be (instantiated as) any one of them, thus it CONTAINS the logical disjunction of all types, thus being the subtype of all types. Even if the novice doesn't get this far, even the first step (in 2 above) is a lot further than Nothing is null. And at the end of correctness, Universe is (I argue) the most correct also from a type theoretic POV:

   http://groups.google.com/group/scala-language/browse_thread/thread/22bfb3666b1ac43d/416ff028e1d3dc58?#416ff028e1d3dc58

   Top is "populated with" (contains) all the types in the universe, Bottom is all the types in the universe.

   Vice versa. Top IS all the (set of all) types in the universe, but it CONTAINS only one (unknown statically) type at a time. Whereas, Bottom IS the empty set of types (as sets) and it CONTAINS all the types in the universe.

I am okay if you chose Something and Nothing. I do like Something more than Thing, as it implies it is unknown and an uninstantiable type. Perhaps you are correct in terms of what users want.

The symmetry is cute, but that symmetry still doesn't help me think Nothing is not null, and rather something much more complex. The symmetry does not intuitively tell the newcomer that they are opposite ends of the type hierarchy. All the symmetry says intuitively is that Something is not null, and Nothing is null.

Want to place bets that you will have a FAQ, "Nothing is not null", hehe.

I would still vote for corrrectness, since afaics other choices don't aid learning any way:

Top: Unknown Bottom: Universe Bottom alias for non-termination: Never (and discourage usage of exceptions).

[quintesse]

@shelby3 really, you say you agree with the 3 points but then you come up with the same old stuff that you already know nobody is going to agree with. So why bother?

And when you rewrite what I wrote about contains and is you just came up with something that will make most people's heads spin. Like I said before let's stop the philosophical discussions and focus on practicalities.

[shelby3]

@quintesse: I was addressing your 3 priorities in order.

1. I first explained that I think Nothing is not more intuitive, because there is some evidence that it is intuitively equated with null.
2. I then explained why I think newcomers will find Universe more intuitive initially and will cause them to think about the first vague qualities of bottom.
3. I then got into the gory correctness details.

I will go back and number my prior post, to demarcate those sections so they match your stated priorities.

[quintesse]

In points 1 and 2 you keep claiming that novices will clearly think Universe is the bottom type, and I'm telling you you're mistaken. No ordinary user is going to intuitively "get" that and even after being told they'll be "sure whatever". You just have to see how people reacted to that suggestion here, let alone people who really don't want to spend time theorizing about type systems.

And in point 3 you go directly against what I said: it's the least important of the 3 points and comes "after" the other two have been satisfied, not "instead of" and admitting defeat that we can't figure out how to do them.

So unless you come up with something new I'll stop replying now, I've lost more than enough time on this discussion.

[shelby3]

Let me try to simplify my explanation (or opinion) of gory correctness details.

The type of Top is set of all possible types, thus is unknown what single type it contains at any place in code (i.e. statically/compile-time).

At every place in code, Bottom always contains every possible type simultaneously, thus its type is the empty set of types and can't be instantiated.

Because how can a container of every type, have any single type.

Bottom can be used to express a covariant relationship, because it contains all types.

Top never contains more than one type simultaneously. But it is unknown what type it contains, because the type of top is the set of all possible types.

[RossTate]

Again, types are normally named after their elements, not their subsets. In particular, a type's name should make sense even if there were no subtyping. Top does not contain tops. Unknown does not contain unknowns. Bottom does not contain bottoms. Also, using quantifiers is problematic because in English their formal meaning depends on context, which is why names like Any and Every are ambiguous. So far the big problem is that OO has some misleading terminology. I'm pretty sure if you told a non-OO person that a list of nothings can be nonempty they'd be a little perplexed.

[quintesse]

Ok very last time because in my opinion your mixing all kinds of different ideas together.

If we think of sets, top is the set of all possible types (agreed). That set contains all possible types. It is structureless, a void. A reference of the top type at runtime can only contain a single type (but that holds true for all references, so I don't see why it should be mentioned specifically here) chosen from the set.

And again thinking of sets, bottom is the empty set. That set contains no types. It is (the combination of) all possible types (not contains, it doesn't hold anything, we're not talking about sets anymore because we already agreed that was empty) and therefore impossible. A reference of the bottom type at runtime can only contain a single type chosen from the set, but because the set is empty it cannot contain anything at all.

I keep hammering on this definition of contains and is because that's how people are used to talk about hierarchical relations in OO: a car is a vehicle. So bottom is whatever type you want (it is all types at once), while every type is top.

[shelby3]

@quintesse:

In points 1 and 2 you keep claiming that novices will clearly think Universe is the bottom type.

Not what I wrote.

I wrote that Nothing will be thought to be null by users. And that Universe will at least cause them to ponder what it is.

That is a difference between explaining that "Nothing is not null" and explaining "Hey what is this odd Universe type I never seen before".

No ordinary user is going to intuitively "get" that and even after being told they'll be "sure whatever".

I think this is equivalent to saying that no ordinary user is ever going to understand Liskov Substitution Principle, covariance, contravariance, types as sets, etc.. I agree. And thus the name is not for them any way. At least we avoid the "Nothing is not null" explanation. We can at least get to say understand intuitively at a minimum that Universe is something they don't understand and don't need to understand. And they will end up using Nil or Empty aliases.

Now for those who are going to learn about LSP, etc, I am thinking there are also a lot of smart coders out there. And I think directing them initially away from null and towards "this is a different kind of type than you've seen before" is a useful first step.

What name would most help them learn faster and aid their understanding and them help them remember the concepts later? Perhaps no name can do all that, so I would then argue for prioritizing not confusing initially with null and being the most correct name.

Honestly I often forget the logic that Nothing could be a subtype of all types, because such subsets are mutually exclusive and thus render an empty set.

For me when I was a novice, the Universe has all types. But then if I instantiate it, what type does it have? Darn I realize I can't instantiate it. Okay but I can't instantiate Top either, so I can understand the Universe could be confused as Top. But at least it gets me thinking about it being a container for all types that can't be instantiated.

So I guess I am saying I hate Nothing more than I love Universe in terms of novice initial understanding. As for deeper learning, I can't think of any cute names that are unambiguous for those learning. The most unambiguous are Top and Bottom or SuperOfAll and SubOfAll.

As for correctness, I like Unknown more than Top or SuperOfAll because it implies some useful qualities that I want users to remember, i.e. mainly that it is a run-time type hole. Again for the correctness perspective only, I like Universe more than Bottom and SubOfAll, because it implies some deep qualities.

You just have to see how people reacted to that suggestion here, let alone people who really don't want to spend time theorizing about type systems.

I am wondering if you all are representative of newcomers. You want to undo what you did as newcomers, i.e. making Nothing equal to null, so perhaps you've forgotten now that stage.

And in point 3 you go directly against what I said: it's the least important of the 3 points and comes "after" the other two have been satisfied

I hope you can appreciate that when brainstorming, one needs to write down their thoughts before they lose them. I can't queue up things perfectly as if I have a secretary working for me to file future posts that enter my mind now. I did put them at the end, since they are the 3rd priority.

Also I think I have come to the conclusion that there is no way to satisfy the first 2 conditions very well, thus we are left to some extent largely with correctness as a potential benefit. In other words, I think we may be deluding ourselves on the intuitive power of our choices.

I've lost more than enough time on this discussion.

When the goals are unrealistic, it is best to turn to what can be accomplished. I would like to see something reasonably correct in type theory and which steers the user towards understanding they are top and bottoms of the type hierarchy.

So I would almost prefer to go back to my original suggestion of SuperOfAll or SubOfAll, or simply Top and Bottom.

As I said in the prior post, I find Something to be roughly correct as Unknown, as well as being intuitive.

The problem is Nothing and the logic that has been explained here for why it is intuitive, doesn't strike me as being intuitive. The only way that has been explained to get a bottom type understanding from Nothing is to reason deeply about LSP and sets. The other argument for Nothing has been that List<Nothing> is obviously an empty list, but I argued that is not the way a newcomer would view it. Perhaps I am wrong.

And perhaps the only thing that matters is to say List<Nothing> is an empty list and say don't try to figure out why, just memorize it. And users will say "yeah List of nothing is empty, got it". But any way, we have Empty for them, so I don't understand this big win. So then I turn to correctness as the benefit we could gain.

[shelby3]

@RossTate:

Again, types are normally named after their elements, not their subsets. In particular, a type's name should make sense even if there were no subtyping.

Why?

So if true, this logic argues for Nothing for bottom. Is there any name that will not cause the new user to think of null, given that is the only concept of an empty element they know of?

I guess that would be Impossible?

[shelby3]

@quintesse: Perhaps we both got it wrong still.

Top is the disjunction of all types. And bottom is the conjunction of all types.

I need to convince myself it is logically true, but I think that definition allows top to be the supertype for all types and bottom to be a subtype for all types.

[quintesse]

@shelby3 : exactly, top is a logical disjuntion or union in set theory (http://en.wikipedia.org/wiki/File:Venn_0111_1111.svg , which encompasses everything) and bottom is the logical conjunction or intersection in set theory (http://en.wikipedia.org/wiki/File:Venn_0000_0001.svg , which contains nothing because the intersection of everything is necessarily empty): , that's why we talk about unions and intersections in Ceylon. (BTW this is the opposite if you would be looking at the type's structure, where Top is empty and Bottom is this enormous superposition of every possible type)

[shelby3]

So if my succinct definition is true, then I have a problem with Nothing (other than it being confused with null) that is throws away (obscures) most of the definition of bottom's type.

Afaics, Unknown and Something don't throw away the disjunction, since any type can be intuitively be assigned to these types.

@RossTate: are you saying that we should only name according to which elements can populate the type's instances, and not which types formulate the compound type? Why?