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.

[durban]

What about Anything/Nothing? (Scala has Any/Nothing.) I also like Top/Bottom.

[simonthum]

This is subjective by nature, so:

To me (i.e. with some C(++) background) void mainly means "comes with no assumptions about the actual type". Of course, the concept's beatuy dies with the pointers you don't have in Java/Ceylon. So I concur that Void is a bit misplaced, even though it is to me because void* is pretty much what Void means in references but not return types.

Top/Bottom is nice for thinking in trees. Less so if you include interfaces in your topology ;(

Anything/Everything comes to mind, but is probably a bit off for c eyes.

Why Bottom could be SubType or NonValue or Undefined is beyone me. I guess I hate it.

I could think of Void/Unspecified, though that only works if you have in idea of void, i.e. it's not too clear which is what.

[Maia-Everett]

Unknown/Impossible sounds good to me. Unknown invokes memories of COM's IUnknown, the superinterface of IDispatch (which was mapped to Object in Visual Basic).

[gavinking]

@durban Nothing works as the name of the bottom type in Scala because null is an instance of the bottom type. But Ceylon's null is typesafe, so Nothing is a completely different type, not the bottom type.

But I suppose we could potentially use Anything/Nothing as the names of the top / bottom types if we renamed our current Nothing class to Null. That might work out pretty nicely.

[FroMage]

I vote for!

[durban]

@gavinking Well, if I understand correctly this: http://www.scala-lang.org/api/current/index.html, then Scala actually has a type called "Null" (null is an instance of this), and has a type called "Nothing", which is indeed Bottom (the empty type, i.e., it has no instances, and it is a subtype of every type). So yes, I think it would be good to rename the current "Nothing" to "Null", and use Anything / Nothing as top/bottom as you said.

I mostly like this version, because then if I have something which has the type "Nothing", then I know, that "it can be nothing" (because Nothing has no instances). Similarly with Anything: "it can be anything" (because everything is an instance of Anything). (I'm not a native speaker though, so I may be mistaken.)

[quintesse]

Definitely seems the best option so far. Nicely symmetric names and null being an instance of Null also seems more intuitive than Nothing. +1

[gavinking]

Scala actually has a type called "Null" (null is an instance of this), and has a type called "Nothing", which is indeed Bottom (the empty type, i.e., it has no instances, and it is a subtype of every type).

Ah, OK, well, yeah, Scala's Null is the bottom of the reference types, whereas Nothing is the bottom of all types. There's two differences here:

1. Ceylon doesn't really split the type hierarchy into "reference types" and "value types", except to the extent that some classes aren't subclasses of IdentifiableObject.
2. Ceylon's null isn't an instance of any kind of bottom type - it's not even an instance of Object.

So just be a little bit careful about mapping concepts back and forth between Ceylon and Scala, because they are not precisely the same.

[Maia-Everett]

I like Anything/Nothing and using Null as the type of null. It makes the type system look more regular.

[gavinking]

This change would be acceptable to me.

[quintesse]

+1

[shelby3]

-1 on the Anything/Nothing.

I prefer Anything/Everything, or Anything/All, or Any/All.

An instance of SomeType<All> is assignable to SomeType<out T> for any T.

SomeType<Nothing> does not make the correct implication in the above case. Without deeper reasoning by the user, it seems to imply that it can't instantiated.

An example use case is if an empty collection is modeled with a Nil satisfies Collection<All>. This specific use example may not apply to the eventual standard collection library, since Ceylon has first class treatment of null with an intersection type. Nevertheless, there may be other use cases.

Also in my mind, Nothing is not the symmetric meaning to Anything. For me, it is intuitive that All or Everything can't be instantiated, because the set of types of a program is open due to subtyping.

[quintesse]

"Without deeper reasoning by the user, it seems to imply that it can't instantiated" well as far as I understand things that's exactly what it means. That's why one of the alternative suggestions was Impossible.

[shelby3]

But my point is that SomeType<Impossible> can be instantiated.

The user has to reason out that while Impossible can't be instantiated, given the covariant parameter of SomeType, the former can be instantiated (the type parameter will never be allowed in the method input position).

Whereas, in my mind, it is obvious that type All or Everything, can't be instantiated, because there is no value that is all types of the program. And then there is not the implication that SomeType<All> can't be instantiated.

But the more I think about it, I don't like All and Everything, because the bottom type is not the supertype of all types. And it is not just Nothing or Impossible either. It is the subtype of all types. It is something and it is possible to use it for the type of a value, as per the example above.

The most accurate I can think of which is perhaps more intuitive than Top/Bottom is AnySub/AllSuper or AnySubtype/AllSupertypes. Since Ceylon favors verbosity for clarity, perhaps my suggestion is AnySubtype/AllSupertypes.

[quintesse]

It cannot be instantiated, no value will ever exist of the type SomeType<Nothing> that's exactly why Impossible was one of the suggestions. No value will ever exist with a type that is a subtype of all possible types. It's a completely "virtual" type but still useful in some cases.

[shelby3]

Please correct me, but I think it can be instantiated.

http://en.wikipedia.org/wiki/Bottom_type#Computer_science_applications

"3. List[Bot] is a natural type for the "null pointer" value (a pointer which does not point to any object) of languages like Java: in Java, the null type is the universal subtype of reference types. null is the only value of the null type; and it can be cast to any reference type.[3] However, the null type does not satisfy all the properties of a bottom type as described above, because bottom types cannot have any possible values, and the null type has the value null."

You can work it out by studying the Scala use cases.

Scala instantiates "object Nil extends List[Nothing]" and "object None extends Option[Nothing]":

http://www.codecommit.com/blog/ruby/monads-are-not-metaphors

---

Tangentially, that Wikipedia link says that Void is not the top type, and instead the unit type. I am not sure what corner cases that might introduce since Ceylon is conflating the top and void types. I saw that Ceylon wants to be able to assign any function that returns any type, to a type that is a function that returns Void.

[quintesse]

I'd say this says it all: "However, the null type does not satisfy all the properties of a bottom type as described above, because bottom types cannot have any possible values, and the null type has the value null". Our bottom type is a "real" bottom type and has no possible values.

[shelby3]

Apparently you are equating the instantiation of the bottom type with the instantiation of a type where the bottom type is a covariant parameter (which is exactly the misunderstanding I am trying to avoid, by suggesting using AllSupertypes instead of Nothing or Impossible). The latter is instantiable, the former is not.

The Scala type Nothing is not instantiable, and is the "real" bottom type too. The Scala type Option[Nothing] is instantiable (and is not a bottom type, so agrees with your Wikipedia quote). The Null type is distinct from Nothing in Scala too.

The requirements of a covariant type parameter enable that. What you are forgetting is that the bottom type is populated with every supertype in the program (which is why Nothing and Impossible are not truthful names). This means it can be instantiated where it is used as covariant type parameter.

P.S. In Ceylon, currently Nothing corresponds to Scala's Null type and Bottom to Scala's Nothing type. What I said for Scala, applies the same to Ceylon.

[quintesse]

I don't see how List<AllSuperTypes> would be more understandable than List<Nothing>?
And you're right that List<Nothing> is instantiable but it conveys the correct meaning that you won't be able to do anything with it. In case of the List it will always be empty, which is just what you want. For soomebody not well-versed in type theory it seems like a very intuitive thing.

[shelby3]

It can do something, e.g. the instance of Nil is an empty list, and it assignable to any type List<T>, which is exactly what List<AllSuperTypes> conveys in my mind since T represents all types and assignment is covariant subsumption. For example, a list data structure has two fields, T head and List<T> tail, so the tail is set to Nil to mark the end of the list.

Note that in Ceylon, one could mark the end of the list with null and use type List<T>? tail instead. But perhaps this is only an example of a more generally applicable type construction (I need to think about other use cases).

Whereas, assigning a List<Nothing> to a List<T> connotes that we are setting an unpopulated item to a populated one.

If I am not mistaken, there is a key type theory insight. In the domain of values, the bottom type is an empty set, but in the domain of types, it is definitely not an empty set, because it is populated by every supertype (every type other than bottom) in the program. That is fundamental reason that Nothing or Impossible is semantically untruthful. And the Ceylon spec makes the error of stating that the bottom type is the empty set, without stating which domain.

Any way, in the end perhaps it is just a matter of user taste on the name choice (although in any case, I am thinking the spec needs to corrected on the empty set domain point). I dunno.

[quintesse]

Well the matter of taste is an important one in this case, because the current name is maybe to most semantically correct but we're looking at alternative names exactly because of the reason that we think it will be hard to explain to "The Average Java Enterprise Developer" what things like Void and Bottommean. Se we're basically looking for intuitive, almost "catchy" names that are not too incorrect.

[shelby3]

Yeah I leave the interpretation of user pyschology to the major stake holders in Ceylon. ;)

Thanks for taking the time to help me explain my point on the issue deeply.

Also hope someone looks at the point I made about Void should be distinct from the top type.

[shelby3]

If I am correct that the bottom type is populated as the subtype of all types other than itself (i.e. not the empty set in the type domain), then another suggestion is:

AnyValue / AllTypes

Maybe that makes it more clear that the bottom type is not populated with values, but is populated with all types. So if user thinks about instantiating an AllTypes, they will realize there is no single type that will suffice.

When I first saw Nothing in Scala, I thought it was the type of the null value, since I didn't yet know there was a distinct Null type, which confused me because List<Nothing> (List[Nothing] notation in Scala) was implying to me an empty list could contain null values. But a list of null values is not the same as an empty list.

The List<AllTypes> implies to me a list of values each of which has the type of all types, which is thus a list which is impossible to populate, so I know it is empty.

But I see that if not confused to be List<Null>, then List<Nothing> could be interpreted as a list of values that are nothing, thus impossible to populate.

More descriptive:

AnyTypeOfValue / AllTypesNoValues

[simonthum]

Probably it is completely nuts, but have you considered promoting void to a keyword which stands for Void or Bottom in each case where it cannot sensibly be the other one?

E.g. Sequence<void> would become Sequence<Void>, not Sequence<Bottom>. At the least, it would matter less which actual type names there are. I presume there are enough cases in favour of Bottom.

[gavinking]

Hey, let's call the bottom type either Error or Problem. Meaning that if the called function terminates it results in a thrown exception. I like Problem, personally. To me this is more meaningful than Nothing for the bottom type.

[gavinking]

So, if the bottom type is Problem (or Error) here's a few idea for the renaming of Void. Note that upon reflecting I think the name Object is also in play, since the truth is that Ceylon's null is an object according to ... so it's kind of lying to pretend it is not. Hell, it's even declared object null, even though it is not an instance of the class Object according to the naming scheme in use today. So here's some less-lying options:

class Object() of Nothing | Something {} 
class Value() of Nothing | Something {} 
class Anything() of Nothing | Something {}

[shelby3]

Aren't you conflating unit (i.e. Void) and bottom (i.e. Nothing) types?

http://en.wikipedia.org/wiki/Unit_type

I also made an argument for equating unit and bottom, and was not well received:

http://stackoverflow.com/questions/19132/expression-versus-statement/8450398#8450398

You've given me an idea. Perhaps I like the name Exception or Exceptional for bottom, since bottom is not always a problem or error. It is an exceptional case. For example, to represent the empty list, e.g. List<Exception>. Then it also works as a name for the unit type too, if conflating the names does not cause a problem?

[shelby3]

The bottom type has no values, but is populated as the subtype of all types. The unit type has only one value, thus contains no compile-time information. Runtime exceptions can't be checked at compile-time, as that defeats the point of having them (as Java painfully discovered).

Even functions that return a value and have exceptions, really return the union containing the unit type. I read that unit is necessary to express some generic relationships, where bottom won't work.

Bottom type can only be used where it doesn't instantiate a value, so afaik this is some exceptional case, because it can be populated by all types in the contravariant direction.

So if you really don't want the user to think hard about what bottom really means, perhaps Exception works. But if you do want deeper understanding, that is far from meaning "subtype of all types" and the "type of no value". But that concept is so deep, that I don't think most people get it even after it is explained.

[gavinking]

Aren't you conflating unit (i.e. Void) and bottom (i.e. Nothing) types?

I don't think so, no. Ceylon doesn't use a unit type to represent the type of a void function. We specifically wanted to make the return type of a void function analyze to the top type. Even if that's slightly "wrong", it's much more convenient for working with higher-order functions.

[shelby3]

I remember that void is the top type in Celyon to be able to assign a function with any return type, to a function that returns void. I assume this so we can throw away the return type.

Afaics, this is a type hole because one can assume they are calling a function that has side-effects (void functions always do), but which does not, thus wasting the CPU. Perhaps there are other more complex negative ramifications?

Afaics, the underlying dilemma is due to mixing pure functions with impure functions. Pure functions can never be void. But this gets into a totally different way of looking at how for example a GUI should be programmed, and it reaches into the design of all the libraries. And pure functional reactive it is an area of research that has not provided conclusive results. If it were possible, I would prefer to not mix side-effect spaghetti with pure functions, and to make as much of the program as possible pure. But this is a really deep research issue and I know you don't want recreate Haskell, and thus I understand what Ceylon is working with and trying to improve. Just not sure if I agree with the compromise (I am researching solutions).

The bottom type is the type of any function that does not return, e.g. exit or die. This is different from the void (unit) type, which does return but without any variable value. My point was that every function that can throw an exception returns a union including the bottom type. I wasn't thinking clearly when I asked if you were conflating void with bottom. You never even implied that.

Exception, NoValue, or Nothing seems to work for the return type of a function that never returns (and/or throws exceptions), as well as for the contravariant type parameter of a class. The user wouldn't be burdened with knowing it is also the subtype of all types, but they will need to know this if to understand why the bottom type works in the contravariant position. Are there any other practical uses of the bottom type?

I can't think of a name other than Bottom that could imply "subtype of all types" intuitively. Even AllSuperTypes or All is confused with the top type. I argued that All can't mean one type, so it must be a subtype, but I admit it is not intuitive.

So I guess I would choose Any/NoValue, because I assume you are not going to support unions of bottom for functions that optionally return exceptions. But I wish I could find a better solution.

[quintesse]

Well, but on the other hand we have exists, as in "does this value exist"? And null means "no".

[ikasiuk]

So, my personal opinion is that bottom should be called Nothing

I agree.

and top should be called Value or Thing.

I can't bring myself to take Thing serious. Value is better but I agree with @quintesse that it feels wrong with null. I still prefer Anything or maybe Something.

[shelby3]

We can perhaps express categorical duals in english using the word "not".

Top and bottom are categorical duals, given their simple definitions:

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

So I have a fresh idea, to get us away from the many problems of Nothing (e.g. Bottom's values are not empty, it has one instance that is a set), without losing the intuitive spirit of it:

OneThing / NotOneThing
Something / NotOneThing
Thing / NotOneThing
Thing / NotAThing

This is not the same as saying Nothing, because it can be more than just one or a thing (and Bottom is the conjunction of all things).

I don't agree with @RossTate that Something is ambiguously top or bottom. It can't be bottom, and "some" does not preclude any type, so it can be top. In my mind, the synonym of "some" is "one" and thus eliminates the ambiguity, which for Any..., All... and Every... is whether they have any specific type or simultaneously have any (thus every) type:

#186 (comment)

For me, NotOneThing is sufficiently equivalent to Universe, while is also expresses more intuition on the duality to OneThing or Thing.

For me, NotAThing is not sufficiently equivalent to Universe, but it is better than Nothing (as stated above).

I preferred Something or OneThing over Thing, because they connote a general uninstantiable supertype, whereas Thing leans to being a real world instance. However, I like the conciseness of Thing.

I agree that Thing is comical (hard to take serious).

This leads to another idea:

Instantiable / NotInstantiable

Hmmm.

Brainstorming continues...

[RossTate]

Well, but on the other hand we have exists, as in "does this value exist"? And null means "no".

Given a T? x, exists doesn't actually tell you if x is a T. It actually tells you if x is not the null value. Thus, exists is really a shorthand for !is Null and would be more accurately called nonnull. Also, is Nothing or nonnothing both don't correspond to null in my head, which further makes me feel that Null is a better type for null.

I still prefer Value (I agree Thing is lackluster). If we had to go with a quantifier, I'd prefer Something since I'd prefer too weak a name (e.g. Consumer<Something> consumes more than just something; it consumes anything) over too strong a name (e.g. Producer<Anything> is not a producer of anything).

Brainstorming continues...

As I said, we are not brainstorming anymore. We could keep coming up with new possibilities forever, but we've done that for long enough. We are now trying to eliminate/narrow options so that we can come to a decision.

[shelby3]

Also why was Unknown discarded from the objective list of candidates for Top?

• serious
• accurate
• no ambiguity with Bottom
• obviously not instantiable (discourage casting away types, encourage use as a bound only)
• "is-a" thus does not apply, Should we rename Void and Bottom? #186 (comment)

Negatives:

• doesn't intuitively convey duality with the Bottom (perhaps it does for Unknown / Never)
• doesn't intuitively convey that it is an object (but we want to discourage this use any way)

[shelby3]

We are now trying to eliminate/narrow options so that we can come to a decision.

Thing / Nothing

Or:

Any / Nothing

None of your available choices are perfect, so might as well choose the most concise, symmetrical, and stay consistent with Scala (at least on bottom).

One argument that can be made against the ambiguity of Any is that Bottom is rarely used.

I want to see how it works out for a mainstream targeted language :)

If I were creating a language for the mainstream, I would instead choose concise type theoretically correct names (e.g. Top / Bottom, SuperOfAll / SubOfAll, Unknown / Never, or Unknown / Universe), and then hide the use of top and bottom as much as possible (using the ideas I explained already to eliminate their use in most cases, arguably improving type correctness of programs and success of novice programmers).

[shelby3]

In the Curry-Howard correspondence, logical falsity (falsum or contradiction) is equivalent to the Bottom type.

http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#General_formulation

A function that returns the bottom type Never returns, and the program is subject to an arbitrary contradiction (indeterminance) w.r.t. to its logical structure. So Never is type theoretically correct in that sense, as well as providing intuition.

Never returning is equivalent to attempting to return the entire Universe, in that neither can occur in finite time. (Btw, thus an exception does not return the entire determinant universe to the program)

Bottom is Never used where it is a type of a value (as it only has one possible value, empty set).

[shelby3]

I want to end by moving my feedback objectively towards your consensus as much as I can, without being dishonest with myself.

When we can't describe exactly what something is with a noun, but we can describe what a coinductive type[1] can't do exactly with a verb, then perhaps we should choose the verb.

Afaics, there exists only one noun for Bottom that fully completes the is-a relationship, but people don't understand well the meaning of the entire Universe.

The noun Nothing does not describe the "logical conjunction of all types" and the values (the set which is always empty), any more than "black" distinguishes "a room in the absence of light" from "a cow in the absence of light" from "_______ in the absence of light". If every set that is empty is Nothing, then the empty collection is Nothing. But that is not correct, rather it is List<Nothing>. Empty or not, a set is always something, not nothing. Inconsistency can have a butterfly effect and explode into chaos.

Thus if Universe, Bottom, and SubOfAll are not under consideration, then I think Never throws away the least information of the terms under consideration which are not ambiguously top or bottom.

Thus I change my vote from Nothing to Never for bottom.

As for Top, Any, Thing, and Unknown each have tradeoffs. I would pick Unknown because I would be discouraging its use for instances (okay to use it as a bound).

I don't understand why you want to copy Scala's emphasis on using the top type to hold instances, as it throws away type information at compile-time and opens the run-time to use of default cases (downcasting) and thus run-time exceptions. It is essentially dynamic typing (a/k/a unityping). Scala has to do this because it doesn't have a first-class intersection type, but Ceylon has one. And Scala does implicit subsumption (automatically casting to top), but afaik Ceylon does not.

But any way, I can tolerate well any of those 3 choices for top, as well Top (not that my opinion should carry much weight, but hopefully I can join the consensus).

[1] A inductive type such as the integers is expressed by a known initial point, e.g. 0 and a succeeding function to get the next values. A coinductive type such as a stream or bottom, is where the succeeding function that expresses the type is expressed towards the final point, but we never get there. The succeeding function for bottom is the disjunction, as we add another type to the universe. It is difficult to describe the succeeding function of a coinductive type as noun. Stream works because we've been taught it. Universe would work for bottom if we were taught it in computer science, but we are not.

[shelby3]

Correction: bottom does not have one instance which is the empty set, but bottom's type is also more than the empty set (so my argument against Nothing = bottom remains):

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/KE5_ZpH5EX0J
https://groups.google.com/d/msg/scala-debate/vysv97J0xok/0o92CFajrLkJ

[gavinking]

So here's my take on all this:

1. We should always pick names for types that describe the values of the type, not relationships between types. Therefore shit like Top, Bottom, Sub, Super, All, etc, are out.
2. The only name I have seen for the bottom type that results in an intuitive interpretation when it appears as a type argument is Nothing. i.e. I don't know of any other name that would work as well as List<Nothing>. (This means we need to rename the type of null to Null.)
3. I think we should strive to make the names of the top and bottom types somewhat symmetric. Therefore, if the bottom type is Nothing, then the top type should be either Anything or Something.
4. Null is a subtype of the top type. To me it would be a little less satisfying if Null were a subtype of Something than if it were a subtype of Anything—just because in everyday English, "anything" is a little less definite-sounding than "something".

Therefore, I'm inclined to stick with the much earlier proposal:

• top type: Anything
• null type: Null
• non-null type: Object
• bottom type: Nothing

To be truthful, I can think of some much better names for Object, including Value, or even Something, but I think we should stick with tradition here.

[shelby3]

Gavin wrote:

We should always pick names for types that describe the values of the type, not relationships between types

Gavin I am sorry to inform you that the bottom type is never used to represent its non-existent value.

So naming it based on its value is going to lead to incorrect semantics.

Here is the hard proof:

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/bIy1VbYIagoJ

After 129 messages in that thread, I think that is pretty well vetted now with some very strong programmers there. Notice they all went silent after the revelation in the link above.

Bottom is always used as either the input or output type of a function (that can't be called or returns the universe of exceptions), or as a type parameter that has semantics that doesn't have anything to do with the type of a non-existent value (see the proof at the link above).

If you are determined to find an "intuitive" name for bottom, which is not too much incorrect from its use cases (which are always contravariant semantics!), and if you are going to choose Anything for top, then perhaps Everything is the best for symmetry using the suffix "thing". Because when used as a type parameter (as proved at the link above), Bottom will always be a supertype in the semantics of the type parameter, in the contravariant direction (regardless whether it is declared out, see the proof at the link above). And when used as the input or output type of a function Everything is of course impossible to instantiate, so it has a non-existent value.

List<Nothing> is not intuitive. How can I assign a List<Nothing> to a List<Anthing>.

Accepted english definitions do allow that a "nothing" is an "anything". Nonsense! List of elements of type "Nothing", again nonsensical. I know you want to say "List of Nothing" in your mind, but that is not how type parameters work. Do we want to create this false semantics that type parameters can not do.

List<Everything> is intuitive. It can be assigned to every supertype and obviously elements of Everything can not be instantiated.

Anyway, my 2 cents...good luck with your choice.

[gavinking]

@shelby3 You're overthinking this. We have a type with no values. If asked to describe a value of this type, "nothing" is as good a description as you're going to find.

Consider the following common English usage:

Q: what is both an animal and a mineral?
A: nothing

The question asks for a description of an element of the empty set. I don't think anyone would find the response "nothing" unnatural. Now, the empty set is a subset of the universal set, and I don't see how anyone could disagree with using "anything" as a good description of an element of the universal set. So it seems that, from the set view of the world:

Accepted english definitions do allow that a "nothing" is an "anything".

At least in the sense that the set of nothing is a subset of the set of "all anythings".

Now consider how this stuff actually occurs in code:

class Empty() satisfies List<Nothing> {
    Nothing item(Integer index) { throw; }
}

To me it is totally intuitive that an empty list is a "list of nothing", and that asking for the element at an index would return "nothing". To me it would be completely unnatural that an empty list would be a "list of everything", and I'm pretty certain that 99.9% of English speakers would agree with me on that.

[shelby3]

Q: what is both an animal and a mineral?
A: nothing

That answer is incorrect (should be Everything) if the semantics of the usage of the type is contravariant. In the example for Tri (a better Try) at the link I provided, the +P (out P in Ceylon) type parameter is narrowest (conjunction) when the possible types it can represent is the widest, as given by the Q >: P (Q is supertype of P) requirement on all the methods.

And we can reason out that bottom will never be used in covariant semantics.

Thus your answer is always wrong (should be Everything). You are trying to apply covariant semantics to a type that is never (can't be!) used in covariant semantics.

class Empty() satisfies List { Nothing item(Integer index) { throw; } }

First, it is the wrong design. List<T> should not contain an item method, Head<T> should. The user then can never access item in an unsafe (untyped) way. If one has a reference to a List<T>, the compiler will force the test for Head before item can be called. This is what I meant about pushing runtime exceptions out to the caller, so they are tested at compile-time. It is analogous to the user is going to need to test head != null in your incorrect design, except that compiler will force them to.

Even if you allow yourself the wrong unsafe (no typing!) design, it is still not "intuitive" that item returns Nothing. It most definitely returns an exception.

an empty list is a "list of nothing", and that asking for the element at an index would return "nothing". To me it would be completely unnatural that an empty list would be a "list of everything",

But you are giving magic powers to type parameters that they don't have.

The type parameter does not become the kind, the kind is List<MemberType>, not ListOfNothing<MemberType>.

The correct descriptions are:

"list of members, where the members have a type nothing"
"list of members, where the members have a type everything"

The first choice is nonsense (assuming out MemberType), because it means we could never assign a "nothing" to an "anything". The latter choice can be an empty list with no member instances.

Do you really expect to dumb-down programming to the level where people don't even speak in their mind correctly what a type parameter is and thus conflate it with the kind of the type? You will create inconsistencies with conflated thought process in the mind of the user.

To make it more clear, List<T> is a shorthand for List with a membertype of <T>. Removing that verbose part from the syntax of the language, does not mean it was removed from the semantics of the language. So now insert Nothing in the verbose type. And you see it no longer works.

[gavinking]

Q: what is both an animal and a mineral?
A: nothing

That answer is incorrect (should be Everything) if the semantics of the usage of the type is contravariant.

WTF? That was a question about ordinary types, not about parametrized types. I'm certain that no native English speaker would answer the above question with the response "everything".

And FTR, the name Nothing works even better for contravariant types than it does for covariant types. Observe:

• a Consumer<Nothing> is not a Consumer<String>
• a Consumer<String> is a Consumer<Nothing>

Which is fair enough. If the bottom type were named Everything, we would wind up with the following backwardness:

• a Consumer<Everything> is not a Consumer<String>
• a Consumer<String> is a Consumer<Everything>

I think your preference for "everything" over "nothing" here is that you're still thinking of relationships between types here i.e. bottom is the intersection of "every type". But that's not our naming convention. We name things by the values of the type, in this case "no values".

You are trying to apply covariant semantics to a type that is never (can't be!) used in covariant semantics.

I don't understand the basis for this assertion, but I'm quite certain that everything I'm doing with the bottom type is perfectly sound from a type theory point of view.

First, it is the wrong design. List<T> should not contain an item method, Head<T> should.

That's a strange assertion and irrelevant to the discussion. Let's think of a Producer<T> type with a produce() method. It's perfectly reasonable to instantiate a Producer<Nothing> whose produce() method has return type Nothing i.e. it never produces anything.

Even if you allow yourself the wrong unsafe (no typing!) design, it is still not "intuitive" that item returns Nothing. It most definitely returns an exception.

That's simply wrong. A method of return type Nothing doesn't return an exception, it throws an exception (or just never returns). I think you understand this. So when I have a Producer<String>, what I know is not that produce() always returns a String—there is no way for any compiler to verify this. Instead, what I know is that if it returns a value, then that value is of type String. Likewise, I know that if Producer<Nothing> returns a value, it returns "nothing"—which is a fancy way to say it never returns a value.

But you are giving magic powers to type parameters that they don't have.

We're arguing about naming conventions and what names encourage the right intuition in most developers. We're not discussing the semantics of type parameters, which we all understand perfectly well. So I'm definitely not giving "magic powers" to anything.

Do you really expect to dumb-down programming to the level where people don't even speak in their mind correctly what a type parameter is and thus conflate it with the kind of the type? You will create inconsistencies with conflated thought process in the mind of the user.

I don't think anyone is conflating anything. I think you're projecting thought processes onto us that are not actually anything like how we understand this stuff.

To make it more clear, List<T> is a shorthand for List with a membertype of <T>

FTR, no, it's not. Ceylon doesn't define this stuff in terms of virtual types, but in terms of type constructors. List<T> is a shorthand for the function List which produces a type List<T> when given an argument type T.

[shelby3]

Q: what is both an animal and a mineral?
A: nothing

That answer is incorrect (should be Everything) if the semantics of the usage of the type is contravariant.

WTF? That was a question about ordinary types, not about parametrized types. I'm certain that no native English speaker would answer the above question with the response "everything".

The only other use case is as the input type of a function that can never be called, and the return type of a function that can never return. Both can never happen because the bottom type is subtype of all types. In neither case, will a non-existent value be input or returned. Thus we see the meaning of bottom is always about typing, never about values.

And FTR, the name Nothing works even better for contravariant types than it does for covariant types.

I am wondering if you entirely missed the point I was claiming, which is to differentiate between the semantics given by the declaration of in or out, as these apply to the external semantics of the kind type, e.g. assigning a List<Nothing> to a List<Any> is covariant. Whereas the semantics of the type parameter itself within the class, will be always be contravariant where the bottom type can be used.

• a Consumer<Nothing> is not a Consumer<String>
  
• a Consumer<String> is a Consumer<Nothing>
  
• a Consumer<Everything> is not a Consumer<String>
  
• a Consumer<String> is a Consumer<Everything>
  

(there appears to be a bug in the parsing of your markdown, if I put the above inside blockquote tags)

Afaics, the contravariant (w.r.t. to the kind Consumer, i.e. in declaration in Ceylon) examples you showed will never be instantiated, i.e. they are illegal, because it would mean that the bottom type could be the input of a function and could not be a return value. And it would mean such a semantics would be the top of all types of the kind Consumer.

I think your preference for "everything" over "nothing" here is that you're still thinking of relationships between types here.

Yes, I even said so many times. And I said the reason is because never will the bottom type be used in any semantics where it is about its non-existent value.

Bottom is at the other end of the infinite inductive type hierarchy, thus it only has coinductive semantics. This is why it will never have a use case where its semantics are about its non-existent value.

And conversely for a coinductive language like Haskell, where the roles of the top and bottom types are reversed. In Haskell, the bottom type (conjunction of all types) is the root of all types! And the top type (disjunction of all types) never has a value!

So you can't think about the infinite co-end of your infinite type hierarchy as consistent in semantics with the rest of your hierarchy in terms of values. Bottom in an inductive language represents the entire universe of values that is available in the coinductive (lazy) languages (which is accessible only as a type in contravariant semantics in an inductive language). And vice versa, in Haskell, top represents the entire universe of values that is available in our inductive (eager) languages, e.g. Ceylon, Java, Scala, (which is accessible only as a type in covariant semantics in a coinductive language).

You are trying to apply covariant semantics to a type that is never (can't be!) used in covariant semantics.

I don't understand the basis for this assertion, but I'm quite certain that everything I'm doing with the bottom type is perfectly sound from a type theory point of view.

When bottom is used as a type parameter, it will never have covariant semantics.

The only other uses cases are for the input and return type of a function.

First, it is the wrong design. List should not contain an item method, Head should.

That's a strange assertion and irrelevant to the discussion. Let's think of a Producer type with a produce() method. It's perfectly reasonable to instantiate a Producer whose produce() method has return type Nothing i.e. it never produces anything.

If you want in private email, I can share with you the correct way to design a list api, so that it never throws an exception. Then we can talk about how your Producer argument is irrelevant. It would be too lengthy to go back and forth on here. Or we can just leave the issue as is.

Even if you allow yourself the wrong unsafe (no typing!) design, it is still not "intuitive" that item returns Nothing. It most definitely returns an exception.

That's simply wrong. A method of return type Nothing doesn't return an exception, it throws an exception (or just never returns). I think you understand this.

There are two ways of thinking of the same thing. Either we say the function never returns, which supports my argument (as I explained near top of this post). Or we can conceptually realize that the function returns to any function in the program (via an exception) and returns any possible type. In support of the latter interpretation, note that exceptions can be modeled as return values in an ExceptionMonad.

Thus we never have semantics for bottom, which are about its non-existent value, rather always about its type.

We're arguing about naming conventions and what names encourage the right intuition in most developers. We're not discussing the semantics of type parameters, which we all understand perfectly well. So I'm definitely not giving "magic powers" to anything.

Every use case of bottom never relatives to it as a non-existent value. So WTF would you name its non-existent value? Use cases are vital in engineering.

You want to be consistent and name types according to their values, but this rule must be broken for the bottom type, because it has no semantics that use its non-existent value property.

Thus by emphasizing the semantics of bottom that are never used, you impart some inconsistent thinking about what type parameters do (as I explained in the prior post).

I don't think anyone is conflating anything. I think you're projecting thought processes onto us that are not actually anything like how we understand this stuff.

You guys are the one who wrote "list of nothing" is intuitive. That means you are encouraging the interpretation of type parameters that is inconsistent with what type parameters are. You are actually moving the type parameter into the kind (as I explained in my prior post).

To make it more clear, List is a shorthand for List with a membertype of

FTR, no, it's not. Ceylon doesn't define this stuff in terms of virtual types, but in terms of type constructors. List is a shorthand for the function List which produces a type List when given an argument type T

Agree that List is a kind which is a type constructor (like a Functor in Standard ML), and the type parameter is T. And you are correct that generally speaking T does not mean "member type". But in the case of the List, it does mean member (or element) type. So both of our statements were correct, yours was just less specific (i.e. more generalized to all possible semantics for kinds).

P.S. I am not arguing this to force any name for Ceylon. I am arguing so that FTR, I will know if I was able to present an objective logic. Because ultimately I have to pick a name for the language I am creating. If my effort to explain my logic can benefit Ceylon, then great.

[shelby3]

I consider my input here to be completed.

Thank you for letting me contribute my feedback. I accept any name choice. I need to move on. I have spent too much time on it, and it is objectively clear (in my own mind at least) for my own language that in type theory the co-end of our language's evaluation strategy (eager or lazy, i.e. inductive/covariant or coinductive/contravariant) is never about its non-existent value.

Afaik, that is a new finding in type theory (also that the dual evaluation strategy is the other side of the universe), so although it is obvious in hindsight, I should probably write a research paper on the finding.

---

P.S. For my language, I have chosen Unknown and Everything. Everything is more descriptive than Universe and All. I also considered AllThings, but that almost sounds like top, as it could be each of all things (or at least it is not more clear than Everything and it is not one word).

I am conflicted about the choice betweenAnything and Unknown, so I might change my mind. Anything is symmetric to Everything, thus gives contrast that so hopefully Everything won't be confused with top. However, Unknown is more clear that we've thrown away typing (unityping) and so its name discourages its use and encourages use of the first-class disjunction type.

Regarding the prior complaint about Everything (or All) being confused with Any:

#186 (comment)

I have since shown that the bottom type will never be used in such a contravariant (i.e. in in Ceylon) type parameter type, so it can never be the destination of an assignment.

Here is a link to my prior post with the tradeoffs for Unknown:

#186 (comment)

The more I think about it, I could choose Anything, because Unknown would have no meaning when used as a type bound. Since we want to discourage its use as a reference for an instance (i.e. the main motivation for choosing name Unknown), then the use as type bound will probably be the main use case. OTOH, we normally never write the top type for an upper bound or inheritance, because the upper bound of top is always implicit. So thus I may stick with Unknown. The choice is all about real world use cases.

So by choosing Unknown, I am saying we will never write the type, unless the user chooses to throw away static typing. Thus the "is-a" relationship is not as important as strongly implying "do not use this type" name (at least not use it explicitly).

And I am not sure it is an inferior implicit "is-a" relationship to Anything (top is the implicit top of all types). Is an Int an Anything, more so than it is an Unknown? (i.e. how can something be both any thing and also something specific simultaneously)

The names that have a correct "is-a" relationship are Value, Thing, Something, and Instance. Of those I prefer Value, but given a name for bottom that contains "thing", then I would choose either Thing or Something.

The advantage of Something is that it is almost as good as Unknown in implying that we've thrown away static typing. And imo it is not as comical as The Thing.

Finally, I could also accept Value and NoValue, because then we would not be encouraged to think erroneously about type parameters "list of nothing" and instead correctly "list of element type of no value". We would have to memorize that NoValue has a "subtype of all types" semantic, as it is not intuitive from the name. We would at least not be implying erroneously that bottom type is nothng (no types) in contravariant typing semantics where it is used. I just happen to prioritize a semantic which makes bottom's type clear, e.g. Everything and then de-prioritize the "is-a" value relationship for top type, because imo we never want to write the top type in our (eager language) programs.

[jdpatterson]

Extremely happy to see Anything/Nothing replace Void/Bottom. I found this discussion after googling for "name bottom ceylon". Excellent!

[OneCheese]

WTF? I just noticed the top type in Ceylon is Void, that's like so confusing, I give up and switch to Scala, this is so lame. I wish someone would fix this already.

[OneCheese]

I'm sooo going to tweet about this.

[gavinking]

The nirvana of the active nonresponse strategy is simply not having a twitter account to not respond with.

Sent from my iPhone

On 06/12/2012, at 3:59 PM, OneCheese notifications@github.com wrote:

I'm sooo going to tweet about this.

—
Reply to this email directly or view it on GitHub.

[gavinking]

I have renamed Void to Anything, Bottom to Nothing, and Nothing to Null.