Re: [scala-language] Re: Top, bottom, non-termination, and their names

[Alec Zorab]

(Forking to scala-debate, please remove scala-language from any subsequent replies)

Since I think most of us are pretty comfortable with the variance of Function1 being [-A, +B], I would propose the following litmus test:

If I write a function with a signature,  Universe => ???, would one expect that to take any available input or would one expect it to be uncallable?

Personally, I interpret A => B to mean "takes a member of Set A and return a member of Set B"

Based on that I'd expect Universe => B to take any member of the Set of things in the Universe and return me a B (whatever that might be). From that I'd conclude that Universe is Top.

On 4 October 2012 10:28, nicola...@gmail.com <nicola...@gmail.com> wrote:

What is usually called Universe in Type Theory is the type of types.
(or the type of the codes for types).

[Shelby]

I have proved mathematically that the only two possible theories of the universe are equivalent (as modeled by programming in "System F with subtyping"):

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

I explained in the above link, that I was aided by Adriaan Moor's idea for improving the model of subtyping in Scala.

On Thursday, October 4, 2012 5:28:14 PM UTC+8, Nicolas Oury wrote:

What is usually called Universe in Type Theory is the type of types. 
(or the type of the codes for types). 

 I assume this is the universal quantification of the "universal type" created by the type constructor, i.e. a kind:

http://en.wikipedia.org/wiki/Type_system#Types_of_types

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

Top is apparently also referred to as a "universal type":

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

The universality applies "for all" types in the system, i.e. Top is a supertype for all types and a kind is a type constructor that may input all types.

Whereas, I am proving that the programming model (in "System F with subtyping") of the infinite physical `Universe`, is the Bottom type.

On Thursday, October 4, 2012 5:47:16 PM UTC+8, Alec Zorab wrote:

(Forking to scala-debate, please remove scala-language from any subsequent replies)

Since I think most of us are pretty comfortable with the variance of Function1 being [-A, +B], I would propose the following litmus test:

If I write a function with a signature,  Universe => ???, would one expect that to take any available input or would one expect it to be uncallable?

Personally, I interpret A => B to mean "takes a member of Set A and return a member of Set B"

Based on that I'd expect Universe => B to take any member of the Set of things in the Universe and return me a B (whatever that might be). From that I'd conclude that Universe is Top.

The input to your function is not the entire universe (not the infinite collection of all its members), but rather any member of the universe (that has any of type from the disjunction of the all the types in the universe). The input to your function is the universal type, Top, not the entire `Universe`.

It is impossible to input the entire universe, because it is infinite in extent. And I have proved that this infinite set is an equivalent model (from an observer outside the universe) to the model that is the conjunction of all the types in the universe (i.e. Bottom) for us inside the universe. Bottom can not be input, because it can't be instantiated (actually it can but its only value is always the empty set).

Note one could point out that a lazy list can represent an infinite structure, but this still does not input the entire universe, because only a finite number of members will be accessed.

[John Nilsson]

If we were talking about Universe.type I could see how the type implies a special type of object. But Universe just implies any object in the universe, not all of them at once.

BR
John

[John Nilsson]

Might also add that Universe => T is a tautology:
Given that anything exists at all then there exists a T
And given that this implication exists in our universe it must then be that a T exists.
Thus Universe => T is the same type as just T, no?

BR
John

[Shelby]

On Friday, October 5, 2012 2:16:55 AM UTC+8, John Nilsson wrote:

...But Universe just implies any object in the universe, not all of them at once.

Does Circus imply any actor in the circus? 

[John Nilsson]

Would you say x:Boolean ⇔ x={true, false} or x:Boolean ⇔ x=true ⊕ x=false?
When you said that an argument of type Universe implies an object that is the set of everything it seems you you were saying that x:Universe should be interpreted like the first statement.

[Shelby]

On Friday, October 5, 2012 4:50:50 AM UTC+8, John Nilsson wrote:

Would you say x:Boolean ⇔ x={true, false} or x:Boolean ⇔ x=true ⊕ x=false?
When you said that an argument of type Universe implies an object that is the set of everything it seems you you were saying that x:Universe should be interpreted like the first statement.

Boolean can never have both values of true and false simultaneously-- it is the union (disjunction) of true and false. Ditto an Integer is the disjunction of the integers.

However, for example a House is not the disjunction of the furniture inside of it, a Car is not the disjunction of the seats, engine, windows, etc..

The Universe has all the things in it simultaneously.

I understand that many people have this same ambiguity in their mind as you did, so I am wondering what causes it? (I am not being critical, heck I make mistakes all the time, just wanting to understand how our minds work)

Apparently they get the logic confused between a Universal type, e.g. Top, which can have any value and the "is-a" relationship of the Universe itself. The difference of "al" and "e" on the end, is perhaps too similar? Rather I think they just don't think of the House and Car examples, because I suppose they are used to thinking about a Universal type, and have never seen before a Universe type, because it is impossible to instantiate the entire Universe. But this is Bottom, but they've either never been taught Bottom, or never been exposed to the idea that Universe and Bottom are the same thing.

[Alec Zorab]

Trivially no, because it expresses any one of an arbitrary number of mappings between those two sets.

[Alex Repain]

The only way my mind can make sense of what you say is if you take for granted that
"A subtype of B" => A as a Set of values is a subset of B as a set of values (which is quite trivial)
AND the reciprocal implication. Which is not trivial at all, at least for me.

You said in your replies on the ceylon-spec list that

"Since the conjunction (intersection) is always narrower or equal to the sets for those types contained in the conjunction, then the conjunction is also a subtype of each of those types contained in the conjunction."

That seems to imply that :

"A subtype of B" <=> "A as a Set of values is a subset of B as a set of values"

But is it really that simple ? Int is a type, but the set of all positive Int values is not a subtype of Int, unless of course I can define it and state it is.
The same goes for collections, an array of Int is an array of Anyval, so all values of Array[Int] are also in Array[Anyval] TAKEN AS  A SET. but is Array[Int] a subtype of Array[Anyval], regardless of if I enforce covariance ? Following this thought, if what you understate is true, the concept of user-defined variance would be rendered meaningless, since variance would implicitly flow from the types taken as a sets. I'm not saying you are "wrong", but I'm intrigued.

2012/10/5 Shelby <she...@coolpage.com>

[John Nilsson]

On Fri, Oct 5, 2012 at 6:32 AM, Shelby <she...@coolpage.com> wrote:
> On Friday, October 5, 2012 4:50:50 AM UTC+8, John Nilsson wrote:
>>
>> Would you say x:Boolean ⇔ x={true, false} or x:Boolean ⇔ x=true ⊕ x=false?
>> When you said that an argument of type Universe implies an object that is
>> the set of everything it seems you you were saying that x:Universe should be
>> interpreted like the first statement.
>
> Boolean can never have both values of true and false simultaneously-- it is
> the union (disjunction) of true and false. Ditto an Integer is the
> disjunction of the integers.
>
> However, for example a House is not the disjunction of the furniture inside
> of it, a Car is not the disjunction of the seats, engine, windows, etc..

Ok, I think I see what you mean. On my end I was somewhat begging the
question. If x:Universe reads x is a member of Universe (in the venn
diagram sense) it must be Top, but you are focusing on the x IS A
Universe sense.

But to be A Universe, you must be THE Universe. Thus my earlier
reference to Universe.type as a more sensible type for that use case.

> The Universe has all the things in it simultaneously.

But now you are again flipping to a HAS A relationship between our
universe and it's content. Again something I think makes sense when
discussing Universe.type


How do you arrive at the conclusion that Universe IS A <anything> ?


It would imply that for all types there is an instance that is not
only that type but also the Universe?

> they are used to thinking about a Universal type, and have never seen before
> a Universe type, because it is impossible to instantiate the entire
> Universe. But this is Bottom, but they've either never been taught Bottom,
> or never been exposed to the idea that Universe and Bottom are the same
> thing.

But this is a paradox. You first claim that there is an object
containing everything, and that the type of this object is Universe,
and then based on the premise that this object contains everything
then it must be infinite and therefore cannot exist? But if it does
not exists, how can it then be infinite or contain everything?

BR,
John

[Shelby]

On Saturday, October 6, 2012 6:30:41 AM UTC+8, Repain Alex wrote:

But is it really that simple ? Int is a type, but the set of all positive Int values is not a subtype of Int, unless of course I can define it and state it is.
The same goes for collections, an array of Int is an array of Anyval, so all values of Array[Int] are also in Array[Anyval] TAKEN AS  A SET. but is Array[Int] a subtype of Array[Anyval], regardless of if I enforce covariance ? Following this thought, if what you understate is true, the concept of user-defined variance would be rendered meaningless, since variance would implicitly flow from the types taken as a sets. I'm not saying you are "wrong", but I'm intrigued.

If you defined the collection with a contravariant type parameter, you would never be able to get any value out of it, because the return values will have to be a supertype of Anyval. So Int can be a supertype of Anyval for a collection that is the empty set as viewed by all reading consumers.

As you know, covariance is based on the Liskov Substitution Principle, which is best understood in terms of sets. Afaics, it doesn't become inconsistent, i.e. our choice for variance annotation will still obey the narrower sets are subsets rule, and will never be an arbitrary result.

Does that entirely address your point?

What is very intriguing to me is that afaics we can mathematically prove the Liskov Substitution Principle is a consistent model for the universe, and then arrive at Bottom is the Universe. 

(Tangentially, Erik Verlinde has also proven how entropy is mathematically equivalent to the gravitational force, and I related LSP to entropy, so I posit it will probably be possible to show consistency to the other proven theories of the universe such as relativity)

I reviewed my logic proving that the two possible (categories of) theories of the universe (i.e. inside relative observers or an outside observer) are equivalent. I had to edit what I had written before, because too much of it had remained in my head and was not there. Now I think it is more clear and is relevant to your point about the choice of variance of the collection:

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

 

 

So the model of the Universe as the conjunction of all its types, i.e. Bottom, is consistent with the collection of its members[1] for an outside observer that can see all infinite possible types in the universe. The type of each such member is a supertype of Bottom and the collection's type parameter has the Top type, i.e. the disjunction of the types of all infinite members in the universe. Since the type parameter of the collection is covariant (not contravariant), the type of the type parameter of the collection when assigning to supertypes is the contravariant dual, i.e. the conjunction of the types of all infinite members in the universe, i.e. which has only one value which is the empty set. So in terms of how both theories can view (i.e. share, assign, or read) the type of the entire universe, they both are the empty set of the conjunction of all infinite types. (Note, the outside observer can also enumerate all the members individually from its infinite collection, but as explained in prior post, this is not a falsifiable theory because we can't test or measure an outside observer since we are inside the universe.)

 

Thus this proves mathematically that the two possible theories for the universe, are equivalent. The only difference is the perspective of the observer. Since we are inside the universe, then we model the universe as a conjunction of its types (thus get an empty set as the observation shared with all infinite instances in the universe), instead of as a collection of the infinite members of those infinite types. But when the outside observer tries to assign the entire universe (instead of enumerating the individual members of its infinite collection), the type also degenerates mathematically to conjunction of its types, as explained in the prior paragraph.

[Shelby]

On Saturday, October 6, 2012 7:05:32 AM UTC+8, John Nilsson wrote:

> However, for example a House is not the disjunction of the furniture inside
> of it, a Car is not the disjunction of the seats, engine, windows, etc..

Ok, I think I see what you mean. On my end I was somewhat begging the
question. If x:Universe reads x is a member of Universe (in the venn
diagram sense) it must be Top, but you are focusing on the x IS A
Universe sense.

":" means subtype of (equivalent to "is or is subtype of").

Subtype means a narrower set (given by the Liskov Substitution Principle).

There is nothing less narrow than top, because it is the disjunction of all types (the instances in the set can be all types).

There is nothing more narrow than bottom (Universe), because it is the conjunction of all types (the only instance is the empty of of types).

We get confused because we want to erroneously think that an *instance* of x:Universe is narrower than all the instances "in the universe". But anything "in the universe" has the top type (disjunction of all types), not the bottom type. In short, anything "in the universe" does not have the type of the entire universe.

But to be A Universe, you must be THE Universe.

Exactly. Note, the empty set of types is the universe from the perspective of an observer inside the universe (because we can only see the mutual perception of all types). An outside observer of the universe can see the collection of all types of the universe, but this conjecture of the existence of an outside observer (while mathematically possible and consistent as I showed), is not falsifiable (we can't take a measurement from the perspective of an outside observer).

 

Thus my earlier
reference to Universe.type as a more sensible type for that use case.

I don't understand this notation.

> The Universe has all the things in it simultaneously.
But now you are again flipping to a HAS A relationship between our
universe and it's content. Again something I think makes sense when
discussing Universe.type

I agree I could spend some time (in the future, and see below) improving my explanation/proof to distinguish between where I am talking about types and where I am talking about instances.

 

How do you arrive at the conclusion that Universe IS A <anything> ?

I have shown mathematically that the universe as a conjunction of all types (perspective of inside observer), is equivalent to the collection of its members which have all types (perspective of an outside observer).

I assert it is obvious there could be no other type of observer which could record the types of the universe. If that is accepted as unarguable and if I have correctly proved that both models are mathematically equivalent, then the model of bottom as the Universe is unarguable.

It would imply that for all types there is an instance that is not
only that type but also the Universe?

I have shown that the (type of the) Universe is the set that is conjunction of all types. An instance of that set, is not the type of that set.

That is the same confusion I explained further up in this reply.

 

> they are used to thinking about a Universal type, and have never seen before
> a Universe type, because it is impossible to instantiate the entire
> Universe. But this is Bottom, but they've either never been taught Bottom,
> or never been exposed to the idea that Universe and Bottom are the same
> thing.

But this is a paradox. You first claim that there is an object
containing everything, and that the type of this object is Universe,
and then based on the premise that this object contains everything
then it must be infinite and therefore cannot exist? But if it does
not exists, how can it then be infinite or contain everything?

You are confusing "a tree fell in the forest" with "I saw the tree fall in your forest".

For the perspective of an observer inside the universe, things only exist for us if we are made aware of them (in sampling theory parlance, we sample them).

Thus the reality for an set of relative observers, is the mutually shared types they are aware of. So their perspective of the universe is the conjunction of the types.

Whereas for an outside observer that is aware of everything in the universe in real-time, that entity can see a collection of instances of all the types.

I have shown that these two models are mathematically consistent.

Thus the entire *infinite* universe is simultaneously everything (to an outside observer) and also the empty set (to all *infinite* inside observers). Take a subset of observers, and then the conjunction of their shared types may not be empty (if they have a shared set of perceptions).

Instances of top are shared perception, when they are not cast to top, because top only knows that it can be anything (that is why I call it Unknown).

But note how some types don't know how to talk to each other in any way. The only thing they have in common is their share top. Thus conjunction of these types is the empty set.

It all makes perfect and consistent sense to me. But I have been thinking about their "theory of everything" aspect for a few years now.

[Rex Kerr]

On Sat, Oct 6, 2012 at 2:50 AM, Shelby <she...@coolpage.com> wrote:

What is very intriguing to me is that afaics we can mathematically prove the Liskov Substitution Principle is a consistent model for the universe, and then arrive at Bottom is the Universe. 

I think you're confusing the abstract notion of "the universal set" with the notion of a physical universe.  The universal set is not really tenable as a mathematical object; it's really a "proper class", or it has weird properties such as not supporting filtering (i.e. if you have an indicator function phi: U => Boolean, you cannot in general find {x in U  | phi(x)} in the universe).  And the physical universe isn't a set at all, it's an instance.

The bottom type is uninhabited, so calling it Nothing makes sense to me, as does identifying it with non-termination (since you don't actually get anything in that case).

(Tangentially, Erik Verlinde has also proven how entropy is mathematically equivalent to the gravitational force, and I related LSP to entropy, so I posit it will probably be possible to show consistency to the other proven theories of the universe such as relativity)

This is astoundingly unlikely.  A field falling off as 1/f^2 (or potential as 1/f) is the same as a statistical phenomenon that goes as the power of the number of particles?  I don't think so, not under any remotely useful definition of "mathematically equivalent".

  --Rex

[Shelby]

On Saturday, October 6, 2012 4:35:58 PM UTC+8, Rex Kerr wrote:

On Sat, Oct 6, 2012 at 2:50 AM, Shelby <she...@coolpage.com> wrote:

What is very intriguing to me is that afaics we can mathematically prove the Liskov Substitution Principle is a consistent model for the universe, and then arrive at Bottom is the Universe. 

I think you're confusing the abstract notion of "the universal set" with the notion of a physical universe.

Are you refuting my proof that the collection of all instances has as its supertypes the collections of any (permutations of) types, thus it has the same supertypes as the bottom type, when restricted to collections of instances?

Thus the bottom type is consistent when we are talking about a universe which is a collection of all instances.

How do you refute that math?

 

  The universal set is not really tenable as a mathematical object; it's really a "proper class", or it has weird properties such as not supporting filtering (i.e. if you have an indicator function phi: U => Boolean, you cannot in general find {x in U  | phi(x)} in the universe).  And the physical universe isn't a set at all, it's an instance.

You are considering the universal set from the perspective of an absolute outside observer. It is not surprising that it is untenable given there is no known outside observer of our universe.

What I have done is shown that such an outside observer's perspective is equivalent to the bottom type. When we as insider observers view the universal set, we only see part of it. And we can only share what we see in common, i.e. a conjunction.

The bottom type is uninhabited, so calling it Nothing makes sense to me, as does identifying it with non-termination (since you don't actually get anything in that case).

The bottom type is inhabited by the empty set. Its instance has a count member and it returns 0.

The universe when viewed collectively by all *infinite* types (observers) in the program is viewed as an empty set. Bottom is not nothing, it is in fact a universal (shared collective) perspective of the universe.

A function which returns bottom is actually returning the entire universe, which is why the program is in an indeterminant state after an exception (the shared types of the program have not been respected and the runtime semantics has been exposed to all the types in the universe).

So nothing is semantically wrong. I argued it more here:

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

 

(Tangentially, Erik Verlinde has also proven how entropy is mathematically equivalent to the gravitational force, and I related LSP to entropy, so I posit it will probably be possible to show consistency to the other proven theories of the universe such as relativity)

This is astoundingly unlikely.  A field falling off as 1/f^2 (or potential as 1/f) is the same as a statistical phenomenon that goes as the power of the number of particles?  I don't think so, not under any remotely useful definition of "mathematically equivalent".

Did you read his proof? It shocked the scientific world two years ago and has been heavily peer reviewed.

[Jan Vanek]

On 06.10.2012 10:26, Shelby wrote:

On Saturday, October 6, 2012 7:05:32 AM UTC+8, John Nilsson wrote:

Ok, I think I see what you mean. On my end I was somewhat begging the
question. If x:Universe reads x is a member of Universe (in the venn
diagram sense) it must be Top, but you are focusing on the x IS A
Universe sense.

":" means subtype of (equivalent to "is or is subtype of").

Nope, it means "is instance of". A value which belongs to the set. "x∈A"

Subtype means a narrower set (given by the Liskov Substitution Principle).

There is nothing less narrow than top, because it is the disjunction of all types (the instances in the set can be all types).

The instances in the set cannot be all types. The instances are not types. The instances *can be/are of-any-type*.

There is nothing more narrow than bottom (Universe), because it is the conjunction of all types (the only instance is the empty of of types).

The bottom *IS* the empty set, there is nothing in the empty set. Not even "empty of types", whatever it might be, is the instance of bottom type. There is no instance, there can't be.

With regards,
Jan

P.S. To put gently, I think this "bottom = Universe" is a total non-sense. I'm surprised you can hold it for so long. But I am not arguing against it anymore, it feels hopeless.

[Shelby]

On Saturday, October 6, 2012 4:35:58 PM UTC+8, Rex Kerr wrote:

On Sat, Oct 6, 2012 at 2:50 AM, Shelby <she...@coolpage.com> wrote:

What is very intriguing to me is that afaics we can mathematically prove the Liskov Substitution Principle is a consistent model for the universe, and then arrive at Bottom is the Universe. 

...  And the physical universe isn't a set at all, it's an instance.

The physical universe has a type, and it is an instance of its type.

The type of the physical universe is either a conjunction of the shared observations of it, or the collection of all its instances. I have shown mathematical equivalence between these two models. The differences between the two models is the perspective of the observer (shared relative observers or an outside absolute observer).

What other possible kind of observer could there be for the Universe's type?

Someone has to observe the instance of the Universe (and all the instances inside of it), in order to verify it is exists. Thus the possible models of the universe's type will all have to fall into the categories of possible observers.

[Shelby]

On Saturday, October 6, 2012 5:07:21 PM UTC+8, j3vanek wrote:

On 06.10.2012 10:26, Shelby wrote:

":" means subtype of (equivalent to "is or is subtype of").

Nope, it means "is instance of". A value which belongs to the set. "x∈A"

It can contain any instance which "is or is subtype of".

The "is" does not mean it can't contain a subtype (rather it just means that we don't know more subtype of the contained instance at compile-time).

Subtype means a narrower set (given by the Liskov Substitution Principle).

There is nothing less narrow than top, because it is the disjunction of all types (the instances in the set can be all types).

The instances in the set cannot be all types. The instances are not types. The instances *can be/are of-any-type*.

Each instance can have any type. (that was the intent of the poorly worded "the instances in the set can be all types") 

 

There is nothing more narrow than bottom (Universe), because it is the conjunction of all types (the only instance is the empty of of types).

The bottom *IS* the empty set, there is nothing in the empty set. Not even "empty of types", whatever it might be, is the instance of bottom type. There is no instance, there can't be.

Not it is not. There are many things that are the empty set:

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

That is a grave error in logic.

Bottom has a single value that is the empty set, but its type is not the empty set. Its type is the conjunction of all types. Period. If you want to try to refute that, have fun hitting yourself over the head with a hammer.

 

P.S. To put gently, I think this "bottom = Universe" is a total non-sense. I'm surprised you can hold it for so long. But I am not arguing against it anymore, it feels hopeless.

To put it gently, you have not impressed me yet as having very sound logic.

Perhaps try to be a little less judgmental to start, and then maybe we can help each other find the truth.

[Shelby]

On Saturday, October 6, 2012 5:26:09 PM UTC+8, Shelby wrote:

On Saturday, October 6, 2012 5:07:21 PM UTC+8, j3vanek wrote:

The bottom *IS* the empty set, there is nothing in the empty set. Not even "empty of types", whatever it might be, is the instance of bottom type. There is no instance, there can't be.

Not it is not. There are many things that are the empty set:

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

That is a grave error in logic.

Bottom has a single value that is the empty set, but its type is not the empty set. Its type is the conjunction of all types. Period. If you want to try to refute that, have fun hitting yourself over the head with a hammer.

It is true that the conjunction of all types is a subtype of the type of the empty set.

 

Saying bottom is the empty set, is like saying that List<T> is the top type.

So you want to give the name Any to List<T>? That means we name all types Any. Then we have unityping at compile-time, i.e. a dynamically typed language.

I would rather give a name to bottom, which indicates more about what it is that is more narrow than the empty set. Specifically it is the universe, as perceived by all types in the program.

[Shelby]

I think I did make a mistake where I claimed Bottom has a single instance which is the empty set.

Bottom's type is the conjunction of all types, which reduces mathematically to the empty set of types, thus bottom has one instance that is the conjunction of all types.

We know (originally pointed out by Andriaan Moors) that the conjunction of types, has the disjunction of the members (methods) of those types. So all the methods of the universe are in the Bottom's type, so clearly it is not just the empty set of types.

Thus my argument holds that saying Bottom is the empty set of types, i.e. nothing, is semantically incorrect.

We can't perceive all of the universe, but the universe continues running anyway (the methods of all the types continue to run).

We can't instantiate the bottom type, because the disjunction of the methods has the conjunction of the types of the arguments of all the methods, again arriving at any empty set for argument input types. The methods are not empty, but the ability to call them is obscured from our perspective of infinite shared observers inside the universe.

I understand that is very non-intuitive to conceive that something that contains everything could also be an empty set. The key is to understand that the empty set is our mutual (shared) coherence when viewing that infinite set.

But it is not empty, because the structure remains, even though we can't perceive the infiniteness of it, i.e. all the methods remain, but we can't all them.

[Alex Repain]

2012/10/6 Shelby <she...@coolpage.com>

On Saturday, October 6, 2012 6:30:41 AM UTC+8, Repain Alex wrote:

But is it really that simple ? Int is a type, but the set of all positive Int values is not a subtype of Int, unless of course I can define it and state it is.
The same goes for collections, an array of Int is an array of Anyval, so all values of Array[Int] are also in Array[Anyval] TAKEN AS  A SET. but is Array[Int] a subtype of Array[Anyval], regardless of if I enforce covariance ? Following this thought, if what you understate is true, the concept of user-defined variance would be rendered meaningless, since variance would implicitly flow from the types taken as a sets. I'm not saying you are "wrong", but I'm intrigued.

If you defined the collection with a contravariant type parameter, you would never be able to get any value out of it, because the return values will have to be a supertype of Anyval. So Int can be a supertype of Anyval for a collection that is the empty set as viewed by all reading consumers.

As you know, covariance is based on the Liskov Substitution Principle, which is best understood in terms of sets. Afaics, it doesn't become inconsistent, i.e. our choice for variance annotation will still obey the narrower sets are subsets rule, and will never be an arbitrary result.

Does that entirely address your point?

Not exactly, or maybe I missed something in your sentences. What I was trying to point out is that, if the subtyping relation is governed by the set inclusion on types taken as sets, then there would be no theoretical value in variance annotations, since we could infer variance from the types used in the type instanciation... That links to your idea of observer relativity, I suppose : the Universe I observe only has that amount of types, those I'm using or able to access, and if I know their relationships as sets, then every type I will construct using these have their relationships already determined. What I don't know, I can't use, but assuming an external observer that is omniscient and knows fully about the relationships between the types in the Universe (taken as sets of values), that observer do not need the concept of variance, which is what I stumbles on.

[Alex Repain]

2012/10/6 Shelby <she...@coolpage.com>

I think I did make a mistake where I claimed Bottom has a single instance which is the empty set.

Bottom's type is the conjunction of all types, which reduces mathematically to the empty set of types, thus bottom has one instance that is the conjunction of all types.

We know (originally pointed out by Andriaan Moors) that the conjunction of types, has the disjunction of the members (methods) of those types. So all the methods of the universe are in the Bottom's type, so clearly it is not just the empty set of types.

Thus my argument holds that saying Bottom is the empty set of types, i.e. nothing, is semantically incorrect.

We can't perceive all of the universe, but the universe continues running anyway (the methods of all the types continue to run).

We can't instantiate the bottom type, because the disjunction of the methods has the conjunction of the types of the arguments of all the methods, again arriving at any empty set for argument input types. The methods are not empty, but the ability to call them is obscured from our perspective of infinite shared observers inside the universe.

I understand that is very non-intuitive to conceive that something that contains everything could also be an empty set. The key is to understand that the empty set is our mutual (shared) coherence when viewing that infinite set.

But it is not empty, because the structure remains, even though we can't perceive the infiniteness of it, i.e. all the methods remain, but we can't all them.

It would make more sense if you associated the methods (more generally, the fields) to the value instances of a type than to the type itself. That is, all values in a type share the same set of methods. It can be considered the structure of the type itself, but let's rather see it as the common structure of all instances of a type. Thus Bottom can have only one type instance (disjunction of all types), this instance has zero value (it reduces to the empty set, the only set that is subset of all sets), and all values of this instance possess all fields from all values of all types, by the disjunctive nature of Bottoms. Since there is no value in the Bottom type only instance, that holds true without being counter-intuitive, it is roughly the same as the well-known "false => true" trick : "S contains no value => whatever you want about the values in S".

[Shelby]

On Saturday, October 6, 2012 6:23:29 PM UTC+8, Repain Alex wrote:

2012/10/6 Shelby <she...@coolpage.com>

On Saturday, October 6, 2012 6:30:41 AM UTC+8, Repain Alex wrote:

But is it really that simple ? Int is a type, but the set of all positive Int values is not a subtype of Int, unless of course I can define it and state it is.
The same goes for collections, an array of Int is an array of Anyval, so all values of Array[Int] are also in Array[Anyval] TAKEN AS  A SET. but is Array[Int] a subtype of Array[Anyval], regardless of if I enforce covariance ? Following this thought, if what you understate is true, the concept of user-defined variance would be rendered meaningless, since variance would implicitly flow from the types taken as a sets. I'm not saying you are "wrong", but I'm intrigued.

If you defined the collection with a contravariant type parameter, you would never be able to get any value out of it, because the return values will have to be a supertype of Anyval. So Int can be a supertype of Anyval for a collection that is the empty set as viewed by all reading consumers.

As you know, covariance is based on the Liskov Substitution Principle, which is best understood in terms of sets. Afaics, it doesn't become inconsistent, i.e. our choice for variance annotation will still obey the narrower sets are subsets rule, and will never be an arbitrary result.

Does that entirely address your point?

Not exactly, or maybe I missed something in your sentences. What I was trying to point out is that, if the subtyping relation is governed by the set inclusion on types taken as sets, then there would be no theoretical value in variance annotations, since we could infer variance from the types used in the type instanciation... That links to your idea of observer relativity, I suppose : the Universe I observe only has that amount of types, those I'm using or able to access, and if I know their relationships as sets, then every type I will construct using these have their relationships already determined. What I don't know, I can't use, but assuming an external observer that is omniscient and knows fully about the relationships between the types in the Universe (taken as sets of values), that observer do not need the concept of variance, which is what I stumbles on.

I get your concept, but I don't have anything to add in terms of understanding or proof. 

Perhaps there are some cases where we don't need to know all the types in the universe in order to deduce the only variance that will work for the code the compiler sees for the class. Perhaps there are other cases where the code for the class allows more than one variance choice, and the unknown types in the universe impact the choice of variance we choose.

Thus your idea is that a total observer would see the total restrictions on variance and could automate the choices.

[Shelby]

On Saturday, October 6, 2012 6:32:05 PM UTC+8, Repain Alex wrote:

It would make more sense if you associated the methods (more generally, the fields) to the value instances of a type than to the type itself. That is, all values in a type share the same set of methods. It can be considered the structure of the type itself, but let's rather see it as the common structure of all instances of a type. Thus Bottom can have only one type instance (disjunction of all types), this instance has zero value (it reduces to the empty set, the only set that is subset of all sets), and all values of this instance possess all fields from all values of all types, by the disjunctive nature of Bottoms.

Disagree. I now have more mathematical clarity than the post you replied to...

The type of bottom has an empty set of *names* of types, but it still has a type with structure.

The type of bottom can't be just the empty set of types, because the conjunction of types is not the empty set of types. Rather it is a type which includes the disjunction of all fields.

Bottom's type thus has no name (there is an empty set for the *names* of types), but the structure is a disjunction of all fields.

A disjunction can't be instantiated, because there are multiple choices. The subtype of a disjunction can be instantiated, and since these are fields (i.e. their type comes from an implicit type parameter, even if hard-coded), then the fields of the supertypes of bottom are subtypes of the fields of bottom.

(note for novice readers, I am often using the property of covariance that it flip flops between contravariance, when go from type to type parameter to arguments of fields, etc)

So the conclusion is that bottom has a type which is not nothing, its type as a structure of fields which is a disjunction, so it can't instantiated. Similarly top has a type which can't instantiated (disjunction of all types in the universe) and thus is not nothing. Note that type also has a conjunction of all the fields, thus an empty set of fields.

So what is bottom? Well I shown w.r.t. Liskov Substitution Principle, it is consistent from the perspective inside the universe, with a collection of all the instances in the universe from the perspective outside the universe. So therefor I assert bottom it is the universe. There is no instance of the entire physical universe either, because the  Second Law of Thermo says the entropy is always trending to maximum, meaning you can't ever reach the edge of the universe. And there is no instance of bottom. Also I have asserting that returning bottom from a function is returning the entire universe of types (indeterminance), because the (other) type constraints of your functions have been (otherwise) violated. I probably have more reasoning to support why bottom is universe, will need to collect my thoughts more.

P.S. correcting your typos, disjunction should be conjunction w.r.t. to bottom. The disjunction is for the fields of the types in the conjunction of bottom.

[Shelby]

On Saturday, October 6, 2012 7:28:56 PM UTC+8, Shelby wrote:

So the conclusion is that bottom has a type which is not nothing, its type as a structure of fields which is a disjunction, so it can't instantiated...

[...] 

 

...meaning you Never reach the edge of the universe. And there is no instance of bottom.

This is why I think Never is also a good name for bottom.

The entire universe may be there for a untestable absolute observer outside the universe, but we (inside the universe) can only represent this as bottom (an unknown type name, with structure of infinite possibilities for fields). We Never will get to the representation of the entire universe in terms of a known instantiation, because it is untenable, due to not having that total observer. (your god may promise you that, but that is off topic here)

Also I have asserting that returning bottom from a function is returning the entire universe of types (indeterminance), because the (other) type constraints of your functions have been (otherwise) violated. I probably have more reasoning to support why bottom is universe, will need to collect my thoughts more.

Never also works for non-terminating functions. I like Universe better, because it is more explicit about what is being returned, but Never is at least not wrong as nothing is. It is true that the function will Never return to the compile-time typed semantics, once an exception is issued (chaos of the entire universe has been introduced, but this is often unavoidable and part of the quest for constantly increasing knowledge, i.e. improving the coherence of your known types to the infinite possibilities). 

[Shelby]

Summary of prior message from me.

Never for bottom is addressing the perception we have the entire universe (including the portions we can't instantiate). Universe for bottom is saying that perception is the entire universe, at least as it matters to us and our perception of what we can instantiate.

The types in our programs is our perception of the universe we can instantiate.

[John Nilsson]

Den 6 okt 2012 10:26 skrev "Shelby" <she...@coolpage.com>:

>>
>> Thus my earlier
>> reference to Universe.type as a more sensible type for that use case.
>
>
> I don't understand this notation.

It is a singleton type

Boolean = true.type + false.type

BR
John

[Alex Repain]

Referencing an earlier post of you : you're right, my bad for the typos !

I think that the intrusions of physics principles is not serving your point very well here. I can understand the quest for an analogy, but it's hard to follow your thoughts when you do so many travels between type theory and (meta)physics.

What is commonly accepted up to now is that "Univers", as in "Universal Type", is referring to Top, and that Bottom is a type that has no value (interestingly enough, in the Curry-Howard correspondance, Bottom is mapped to falsity). Using Universe for Bottom sounds very unappealing to me, rather I'd find something like "All" easier to comprehend : a value of type All is a value that is of all types in the universe. Because of the Curry-Howard correspondance again, we can affirm it's impossible : if we take a non-trivial type Int, and NotInt, the type of all that is not an Int, we can not find any value that is both an Int and a NotInt. Thus Int inter NotInt can not be populated, and by extension All can not be either. We are indeed using the type that is the conjunction of  all types, and it is easy to prove that it is unpopulated. The word Universe is not as easy to comprehend, at least IMHO. That said, I'm satisfied enough with Nothing as the bottom type in Scala. It is really used to mean "nothing" most of the times...

2012/10/6 Shelby <she...@coolpage.com>

[Shelby]

On Saturday, October 6, 2012 8:25:54 PM UTC+8, Repain Alex wrote:

I think that the intrusions of physics principles is not serving your point very well here. I can understand the quest for an analogy, but it's hard to follow your thoughts when you do so many travels between type theory and (meta)physics.

Agreed. The argument is more concise when it is expressed purely from Liskov Substitution Principle and the logic of sets.

So when I refer to universe below, I will be referring to the universe of types and instances in computer programs, except where noted by "physical".

What is commonly accepted up to now is that "Univers", as in "Universal Type", is referring to Top

"Universal Type" is not commonly accepted have an instance which is the entire infinite "Universe", because it can't.

Can you instantiate the entire infinite universe and assign to top?

The entire universe would be all things in the universe, the only possibilities are:

1. collection of infinite instances

2. conjunction of infinite types

Since #1 is impossible, then only #2 remains as a typed model of the entire infinite universe.

What other possible typed model of a the entire infinite universe can anyone think of?

The only other possible answer is that we can't have a typed model of the entire infinite universe.

I already showed using only LSP and logic of sets, that #2 is consistent with #1. That is already a strong argument for #2 being a model of the entire infinite universe.

The other reasons that #2 is a strong model of the entire infinite universe, is that it has the properties that we expect for the entire infinite universe:

a. it is the subtype of every type in the universe (infinite lower bound is always expressed in computer science as a coinductive type, e.g. streams)

b. it is the ONLY TYPE that has no instances, because nothing infinite can be instantiated (whereas Top has instances)

c. a conjunction is common for all types (the entire universe should be what is common from the perspective of the observer type instantiating it)

 

, and that Bottom is a type that has no value (interestingly enough, in the Curry-Howard correspondance, Bottom is mapped to falsity).

I pointed that out too. Falsity is a logical contradiction of the axioms and propositions. The entire universe ("physical" or types/instances) is very much a contradiction, as it is both infinite yet no known instance can be fully enumerated and thus instantiated (duplicated).

Using Universe for Bottom sounds very unappealing to me, rather I'd find something like "All" easier to comprehend : a value of type All is a value that is of all types in the universe.

`All` was originally my choice, until I realized it was ambiguous whether it is top or bottom:

 

Because of the Curry-Howard correspondance again, we can affirm it's impossible : if we take a non-trivial type Int, and NotInt, the type of all that is not an Int, we can not find any value that is both an Int and a NotInt. Thus Int inter NotInt can not be populated, and by extension All can not be either. We are indeed using the type that is the conjunction of  all types, and it is easy to prove that it is unpopulated.

`All` is like saying "entire universe", but it doesn't as strong express "infinitely all" (might just mean "all enumerated"), and it has the above noted ambiguity.

 

The word Universe is not as easy to comprehend, at least IMHO.

Agreed. Just as "Stream" would not be meaningful coinductive type, if it had not been taught.

We don't teach what the typed model of the entire infinite universe is in computer science courses (nor books).

There are much more difficult concepts that people would not have understood before they were taught.

 

That said, I'm satisfied enough with Nothing as the bottom type in Scala. It is really used to mean "nothing" most of the times...

It never means nothing in Scala.

List<Nothing> is not a list of null elements. It is a list of no elements. Big difference.

Non-terminating functions don't return nothing, they return the state of the entire universe, because the localized typing of the function has failed.

[Shelby]

On Saturday, October 6, 2012 7:28:56 PM UTC+8, Shelby wrote:

The type of bottom has an empty set of *names* of types, but it still has a type with structure.

The type of bottom can't be just the empty set of types, because the conjunction of types is not the empty set of types. Rather it is a type which includes the disjunction of all fields.

Bottom's type thus has no name (there is an empty set for the *names* of types), but the structure is a disjunction of all fields.

 

Bottom is a structural type. I wanted to make that analogy, since everyone knows well what a structural type is.

It has no name, because the conjunction of all type names is empty, but it retains the disjunction of the fields of those types from the conjunction.

[Shelby]

On Saturday, October 6, 2012 10:08:16 PM UTC+8, Shelby wrote:

> Since #1 is impossible, then only #2 remains as a typed model of the

> entire

> infinite universe.

I meant #1 is impossible to instantiate.

> c. a conjunction is common for all types (the entire universe should be

> what is common from the perspective of the observer type instantiating it)

Poorly worded.

I meant a conjunction is what is mutual between all types. And to represent the entire universe we need a type that can express what is mutually observable to all types in the universe.

Our programs are composed of types. These types observe and interact with the other types in the universe.

From the perspective of our types in our programs, they see the universe as anything they can interact with, i.e. the mutual coherence between there invariants.

So we would expect the mutually agreed perspective of the universe, to be what is mutually common between all types.

> `All` is like saying "entire universe", but it doesn't as strong express

Typo, s/strong/strongly/

[Shelby]

On Saturday, October 6, 2012 10:08:16 PM UTC+8, Shelby wrote:

a. it is the subtype of every type in the universe (infinite lower bound is always expressed in computer science as a coinductive type, e.g. streams)

This was also poorly worded.

We use a coinductive type to express something that we don't know the total structure of until we get to its final object, yet we know how to extract objects from it:

http://tunes.org/wiki/algebra_20and_20coalgebra.html

So coinductive types are what we expect for infinite final bounds.

Thus bottom very much fits what we would expect for a model of an infinite thing for which we can't expess the total structure a priori, but from which we can express the finite current (not final infinite) structure as we build it.

 

[John Nilsson]

Two things about structural types

A) Do you base your argument on all types being structural? Because that would imply that true.type = false.type which either means not singleton types or that true = false. Neither seems that applicable to Scala.

B) If your point is that Universe can't be instantiated because it must have all possible members I think you are wrong. Wouldn't such an instance simply be the equivalent of a dynamicly typed object responding to every possible message?

BR
John

[Shelby]

On Sunday, October 7, 2012 12:23:32 AM UTC+8, John Nilsson wrote:

Two things about structural types

A) Do you base your argument on all types being structural?

Bottom is a structural type because it is the conjunction of all types. So the conjunction of all types is the disjunction of (I believe all permutations of groups of) the fields of those types. Thus the result is a type which has no name, but has the disjunction of all fields of all types.

A structural type is type without a name, that is matched to other types based on the fields of the type. Afaics, this is how bottom is a subtype of all types (it is matched structurally).

Afaics, this puts to rest the notion that the type of bottom is Nothing. The type of bottom is inhabited with a disjunction of all fields in the universe. The values of bottom are not inhabited, so we can say that instances of bottom Never occur.

With a normal inductive type, the fields of the type are matched to the values, i.e. a Car class that has a 'color' field. So we are used to focusing only on the "is-a" relationship to the values that are inhabited. But with a coinductive type, the structure of the final object is obscured (disjunction of all fields means the field structure can be anything is thus unknown) and if we name only the final object, then we ignore the coalgebra that gives the coinductive type its semantics. The whole reason that bottom exists is because it is the subtype of all types. To say its final object value is Nothing (does not exist), ignores what bottom really is. See my prior message discussing coinductive types and the link on coalgebras.

 

Because that would imply that true.type = false.type which either means not singleton types or that true = false. Neither seems that applicable to Scala.

I don't understand. 

B) If your point is that Universe can't be instantiated because it must have all possible members I think you are wrong. Wouldn't such an instance simply be the equivalent of a dynamicly typed object responding to every possible message?

Oh sure if you want to throw away static typing, then you can model the universe with runtime semantics, but still your code is a coinductive algebra, because you can't respond to every possible message, without knowing the structure of every possible message. You end up with default cases that don't respond or throw exceptions.

[Shelby]

On Sunday, October 7, 2012 1:12:08 AM UTC+8, Shelby wrote:

On Sunday, October 7, 2012 12:23:32 AM UTC+8, John Nilsson wrote:

Two things about structural types

A) Do you base your argument on all types being structural?

No. As explained below, the names of types are lost in the conjunction for bottom's type.

 

Bottom is a structural type because it is the conjunction of all types. So the conjunction of all types is the disjunction of (I believe all permutations of groups of) the fields of those types. Thus the result is a type which has no name, but has the disjunction of all fields of all types.

A structural type is type without a name, that is matched to other types based on the fields of the type. Afaics, this is how bottom is a subtype of all types (it is matched structurally).

Afaics, this puts to rest the notion that the type of bottom is Nothing. The type of bottom is inhabited with a disjunction of all fields in the universe. The values of bottom are not inhabited, so we can say that instances of bottom Never occur.

With a normal inductive type, the fields of the type are matched to the values, i.e. a Car class that has a 'color' field. So we are used to focusing only on the "is-a" relationship to the values that are inhabited. But with a coinductive type, the structure of the final object is obscured (disjunction of all fields means the field structure can be anything is thus unknown) and if we name only the final object, then we ignore the coalgebra that gives the coinductive type its semantics. The whole reason that bottom exists is because it is the subtype of all types. To say its final object value is Nothing (does not exist), ignores what bottom really is. See my prior message discussing coinductive types and the link on coalgebras.

 

Because that would imply that true.type = false.type which either means not singleton types or that true = false. Neither seems that applicable to Scala.

Thus the above doesn't apply.

 

I don't understand. 

B) If your point is that Universe can't be instantiated because it must have all possible members I think you are wrong. Wouldn't such an instance simply be the equivalent of a dynamicly typed object responding to every possible message?

No. Dynamic typing is just static typing with one type. As explained below, it doesn't help you correctly model a infinite coalgebra. You still can't create an infinite instance of anything, e.g. not infinite cases of message structure responses.

[John Nilsson]

Ok, lets simply this a bit.

Assume a very simple universe of only two object: true and false both
containing the members ∨, ∧ and ¬.

I would say that we have the following types
true.type = { true }
false.type = { false }
Top = true.type ∪ false.type
Bottom = true.type ∩ false.type

If I follow your reasoning this is also how you would define Top and Bottom.

However you also claim that Bottom, due to this definition, is a
structural type.

That would mean that x:Bottom iff x has members =, ∨, ∧ and ¬. By
definition this is true for both true and false, so in this universe
Bottom would be inhabited by both, or in other words Bottom = Top
which clearly is not a good thing if want Bottom to be a subtype of
both true.type and true.false.

I see two ways to resolve the situation:
1) Make all types structural which means true.type = false.type = Top
= Bottom = { true, false }
2) Allow Bottom to imply more than structure so that x:Bottom iff x:
true.type and x: false.type, a paradox so Bottom must = {}

BR,
John

[Rex Kerr]

On Sat, Oct 6, 2012 at 4:58 AM, Shelby <she...@coolpage.com> wrote:

On Saturday, October 6, 2012 4:35:58 PM UTC+8, Rex Kerr wrote:

On Sat, Oct 6, 2012 at 2:50 AM, Shelby <she...@coolpage.com> wrote:

What is very intriguing to me is that afaics we can mathematically prove the Liskov Substitution Principle is a consistent model for the universe, and then arrive at Bottom is the Universe. 

I think you're confusing the abstract notion of "the universal set" with the notion of a physical universe.

Are you refuting my proof that the collection of all instances has as its supertypes the collections of any (permutations of) types, thus it has the same supertypes as the bottom type, when restricted to collections of instances?

I'm not sure the collection of all instances is well-defined theoretically (e.g. what axioms of set theory are you taking?).  Also, at the very least you're not being clear about what you mean by "instance" and "collection".

Presumably by "collection" you mean "intersection" as in A0 with A1 with A2 with ....  Then, yes, that collection is the bottom type, but no, it's not a universe in any traditional sense.  If you are talking about the inhabitants of types, then, no, having a bunch of ints and floats around doesn't make you represent the subtype of both ints and floats because you also need something from which you can build an indicator function (at the very least) so you can tell which of the entities you've got is actually an Int with Float.  (I suppose there is some argument that zero is shared, but that's beside the point.)

Anyway, I am probably misunderstanding, but there seems to me to be something profoundly lacking in your view of types that is required to support the universe idea.  For example, the type Char with Double is uninhabited/uninhabitable, just like Nothing is.  But they're not the same; Char with Double promises far less than Nothing does.  You can enforce duality between the intersection of types and the union of inhabitants of those types (if you disallow uninhabited types as irrelevant), but why do you want to name the type after its dual?  We need a type; just name the type.  Nothing is fine, as a mnemonic to remind us that it's uninhabited.  Yes, we have to remember that it's not the only uninhabited type, but the Nothing type.  We could more accurately call it Politician as it will promise to be whatever anyone asks it to be (but not actually do it), or UniverseDual, but I don't think this actually clarifies anything.  Even calling it Bottom is probably not an improvement; people who already know what Bottom is can trivially learn that the bottom type is called Nothing in Scala, and people who don't know what Bottom is aren't helped at all by the name, while with "Nothing" they get the idea that you don't actually have an instance, so maybe it's useful for exception handling or something.  (WithAll is also more correct, but awkward.)

(I'm skipping the set theory stuff since you haven't addressed it.)
 

The bottom type is uninhabited, so calling it Nothing makes sense to me, as does identifying it with non-termination (since you don't actually get anything in that case).

The bottom type is inhabited by the empty set. Its instance has a count member and it returns 0.

You can define it that way, but Char with Double is _also_ inhabited by that empty set with a count member which returns zero.  That particular inhabitation is pretty useless.  Why bother formulating things so that it exists?
 

A function which returns bottom is actually returning the entire universe

This is again completely confusing instances with sets that are duals of type intersections.
 

 

(Tangentially, Erik Verlinde has also proven how entropy is mathematically equivalent to the gravitational force, and I related LSP to entropy, so I posit it will probably be possible to show consistency to the other proven theories of the universe such as relativity)

This is astoundingly unlikely.  A field falling off as 1/f^2 (or potential as 1/f) is the same as a statistical phenomenon that goes as the power of the number of particles?  I don't think so, not under any remotely useful definition of "mathematically equivalent".

Did you read his proof? It shocked the scientific world two years ago and has been heavily peer reviewed.

All right, since your answer was less glib than I'd thought--the relativity thing kind of threw me since there is no intrinsic time among types--what I actually mean is that first, no, I haven't read the proof, but from what I gather of the prerequisites he's come up with a substantially _more_ complicated system to explain a less complicated one.  In particular, since entropy is a component of Gibbs free energy, you can run devices, including presumably instantiations of Turing machines, purely off of entropy.  Thus _that_ you have found some computation you can do using entropy is much less interesting than _how_.  I'm unconvinced that Verlinde has done anything but a nonintuitive curve-fitting exercise.  I should probably withhold judgment rather than concluding that he's probably on the wrong track, but I don't think it looks very hopeful.

Inferring anything about relativity from this is almost certainly unwise; the mathematics is very different to that for statistical mechanics, and requires a particular kind of space (-t,x,...) to work.

  --Rex

[Shelby]

On Sunday, October 7, 2012 3:49:35 AM UTC+8, John Nilsson wrote:

Bottom would be inhabited by both, or in other words Bottom = Top

Please check the logic again. Clearly the above conclusion does not follow from the logic presented before it.

Due to the logic for conjunction, type of bottom is neither the type of true nor false, yet it will contain the disjunction of any fields in the types of true and false. Since the types of true and false do not contain any fields, then bottom's type is not inhabited in your *finite* universe example.

Note to readers, afaik bottom never applies to *finite* universe, thus the type of bottom is always inhabited by the disjunction of *infinite* fields.

[Shelby]

Rex, thanks for help with vetting...below...

On Sunday, October 7, 2012 3:51:30 AM UTC+8, Rex Kerr wrote:

On Sat, Oct 6, 2012 at 4:58 AM, Shelby <she...@coolpage.com> wrote:

On Saturday, October 6, 2012 4:35:58 PM UTC+8, Rex Kerr wrote:

On Sat, Oct 6, 2012 at 2:50 AM, Shelby <she...@coolpage.com> wrote:

What is very intriguing to me is that afaics we can mathematically prove the Liskov Substitution Principle is a consistent model for the universe, and then arrive at Bottom is the Universe. 

I think you're confusing the abstract notion of "the universal set" with the notion of a physical universe.

Are you refuting my proof that the collection of all instances has as its supertypes the collections of any (permutations of) types, thus it has the same supertypes as the bottom type, when restricted to collections of instances?

I'm not sure the collection of all instances is well-defined theoretically (e.g. what axioms of set theory are you taking?).  Also, at the very least you're not being clear about what you mean by "instance" and "collection".

Set of infinite instances is given by the *inductive* Axiom of Infinity.

So my quoted statement above it is wrong because I equated supertypes, but any subset of the infinite set I, will be a subset and thus a subtype.

Instead of proving that the *inductive* Axiom of infinity is equivalent to bottom, I need to prove that they are categorical duals.

http://ncatlab.org/nlab/show/coinductive+type

http://tunes.org/wiki/algebra_20and_20coalgebra.html

The algebra of the *inductive* Axiom of Infinity is a successor function, x union {x} elemof I, that proceeds from an instantiable initial object x towards infinity. Whereas, its categorical dual, would be a coalgebra that has only one morphism from each instantiable object to the uninstantiable final object infinity.

Intuitively it is clear that bottom is that categorical dual. How to prove it?

The natural numbers and the intervals of the reals are examples of an algebra and a coalgebra respectively:

http://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#NaturalNumbers

http://ncatlab.org/nlab/show/terminal+coalgebra+of+an+endofunctor#UnitInterval

Intuitively any countable number is contained within the intervals of reals. (not any formal proof of anything, just to aid thought process about duality)

By definition, each instantiable type in (i.e. subtype of) the *inductive* Axiom of infinite set of types is a supertype of the conjunction of the infinite set of types.

The category is the same, which is the infinite set of types.

An algebra or coalgebra must have exactly one morphism to any object in the category. The *inductive* Axiom of infinity can only build new types from existing types via a successor function, and there is only one morphism from a supertype to its subtype. There is only one morphism such that any type is the supertype of the *coinductive* conjunction of all types. It is only one morphism because the conjunction of two or more copies of the same type is equivalent to that type by itself.

Thus they are categorical duals.

Q.E.D.

My formalism above is weak. Did I fail?

Note the disjunction of all types (i.e. Top), is not an *inductive* model of the infinite set of types, because there is no an inductive morphism to create a new type from top. Induction always requires an instantiable type to build a new type from. Whereas, coinduction is the dual, so it requires that we show that any type we have, has only one morphism to the final object (the conjunction of all types).

 

Presumably by "collection" you mean "intersection" as in A0 with A1 with A2 with .... 

No I meant the infinite set as explained above.

 

Anyway, I am probably misunderstanding, but there seems to me to be something profoundly lacking in your view of types that is required to support the universe idea.  For example, the type Char with Double is uninhabited/uninhabitable, just like Nothing is.  But they're not the same; Char with Double promises far less than Nothing does.

 Do you refute Andriaan Moors' insight that the conjunction of two types contains the disjunction of the fields of those two types?

You are only referring to the ability to reference an instance with a type. But we never use bottom to not refer to any instance. We are always using bottom to represent the category of infinite types.

 

  You can enforce duality between the intersection of types and the union of inhabitants of those types (if you disallow uninhabited types as irrelevant), but why do you want to name the type after its dual?

I want to name the category of objects that the coalgebra of the type contains. The bottom type does not contain nothing. Nor is the use cases of the bottom giving it a semantic of nothing (as I enumerated in a prior message).

 

  We need a type; just name the type.  Nothing is fine, as a mnemonic to remind us that it's uninhabited.

What are the use cases where it can't contain an instance (i.e. is uninhabited)? I don't know of any.

 

  Yes, we have to remember that it's not the only uninhabited type, but the Nothing type.

Can you name any other type that can't contain an instance (i.e. is uninhabited)? I can't think of one that is named.

 

  We could more accurately call it Politician as it will promise to be whatever anyone asks it to be (but not actually do it), or UniverseDual, but I don't think this actually clarifies anything.  Even calling it Bottom is probably not an improvement; people who already know what Bottom is can trivially learn that the bottom type is called Nothing in Scala, and people who don't know what Bottom is aren't helped at all by the name, while with "Nothing" they get the idea that you don't actually have an instance

But we never use bottom to represent no instance. I already enumerated the use case examples in a prior message.

 

, so maybe it's useful for exception handling or something.

An exception does not return a "can't make an instance" to the caller. It never returns to the call. And it returns an indeterminant state to some catch block. It has exposed the catch block to all possibilities, i.e. all types in the universe, thus is has returned the universe.

The reason is because the catch block has no control over the hierarchy of functions (and thus types) below it. Any thing is possible.

 

  (WithAll is also more correct, but awkward.)

(I'm skipping the set theory stuff since you haven't addressed it.)
 

The bottom type is uninhabited, so calling it Nothing makes sense to me, as does identifying it with non-termination (since you don't actually get anything in that case).

The bottom type is inhabited by the empty set. Its instance has a count member and it returns 0.

You can define it that way, but Char with Double is _also_ inhabited by that empty set with a count member which returns zero.  That particular inhabitation is pretty useless.  Why bother formulating things so that it exists?

I already refuted that mistake of mine. The bottom type is not a single instance of the empty set, because the empty set does not include the disjunction of all the fields of the types in the conjunction of all types.

 

 

A function which returns bottom is actually returning the entire universe

This is again completely confusing instances with sets that are duals of type intersections.

Did I not prove above the categorical duality?

 

(Tangentially, Erik Verlinde has also proven how entropy is mathematically equivalent to the gravitational force, and I related LSP to entropy, so I posit it will probably be possible to show consistency to the other proven theories of the universe such as relativity)

This is astoundingly unlikely.  A field falling off as 1/f^2 (or potential as 1/f) is the same as a statistical phenomenon that goes as the power of the number of particles?  I don't think so, not under any remotely useful definition of "mathematically equivalent".

Did you read his proof? It shocked the scientific world two years ago and has been heavily peer reviewed.

All right, since your answer was less glib than I'd thought--the relativity thing kind of threw me since there is no intrinsic time among types--what I actually mean is that first, no, I haven't read the proof, but from what I gather of the prerequisites he's come up with a substantially _more_ complicated system to explain a less complicated one.  In particular, since entropy is a component of Gibbs free energy, you can run devices, including presumably instantiations of Turing machines, purely off of entropy.  Thus _that_ you have found some computation you can do using entropy is much less interesting than _how_.  I'm unconvinced that Verlinde has done anything but a nonintuitive curve-fitting exercise.  I should probably withhold judgment rather than concluding that he's probably on the wrong track, but I don't think it looks very hopeful.

I think that has been the essentially one of the main criticisms coming from peer review, i.e. that showing correlation does not prove cause and effect.

I need to study more, although I already tried to blow some holes in some of the prominent criticism:

http://goldwetrust.up-with.com/t124p15-theory-of-everthing#4626

 

Inferring anything about relativity from this is almost certainly unwise; the mathematics is very different to that for statistical mechanics, and requires a particular kind of space (-t,x,...) to work.

As you and I both know, making general intuitions can somtimes prove to be quite silly when dig into the formal details.

[Shelby]

On Sunday, October 7, 2012 1:52:39 PM UTC+8, Shelby wrote:

I already refuted that mistake of mine. The bottom type is not a single instance of the empty set, because the empty set does not include the disjunction of all the fields of the types in the conjunction of all types.

 

Thus bottom can not be instantiated. And it can not be used to reference an instance. It is not an empty set either.

Coinductive types are weird and they are non-intuitive to us, because we are accustomed to thinking in terms of forming things by constructing them from building blocks. Whereas, co-inductive types are formed by deconstructing from something to the parts it was built from.

Thus of course an infinite thing can't be instantiated and can't be the subtype of anything, thus it can't ever return to an instance of anything. But that infinite thing is not nothing. It it the final object that everything is deconstructed from.

[Shelby]

On Sunday, October 7, 2012 2:04:58 PM UTC+8, Shelby wrote:

Thus of course an infinite thing can't be instantiated and can't be the subtype of anything, thus it can't ever return to an instance of anything. But that infinite thing is not nothing. It it the final object that everything is deconstructed from.

 

Typos:

s/subtype/supertype/

s/ever return to/ever reference/

s/it it/it is/

Embarrassing.

[Shelby]

On Sunday, October 7, 2012 3:51:30 AM UTC+8, Rex Kerr wrote:

(Tangentially, Erik Verlinde has also proven how entropy is mathematically equivalent to the gravitational force, and I related LSP to entropy, so I posit it will probably be possible to show consistency to the other proven theories of the universe such as relativity)

This is astoundingly unlikely.  A field falling off as 1/f^2 (or potential as 1/f) is the same as a statistical phenomenon that goes as the power of the number of particles?  I don't think so, not under any remotely useful definition of "mathematically equivalent".

It is the integration of the projection of the *volume* of micro-states at the event horizon of the black hole that gives rise to the higher-exponential relationship of entropy to gravity:

http://www.youtube.com/watch?v=yk_Yy6TqgJs (start around the 12 min point)

http://en.wikipedia.org/wiki/Entropic_gravity#Erik_Verlinde.27s_theory

I was also developing in my mind some similar concepts of emergence as early as 1991, and wrote down some concepts of mass, energy, force, etc being emergent, publicly circa 2008.

 

Did you read his proof? It shocked the scientific world two years ago and has been heavily peer reviewed.

[...]

 

Inferring anything about relativity from this is almost certainly unwise; the mathematics is very different to that for statistical mechanics, and requires a particular kind of space (-t,x,...) to work.

I suspect the above video will throw a lot of doubt into your mind about the above intuition. 

[Shelby]

On Sunday, October 7, 2012 2:04:58 PM UTC+8, Shelby wrote:

Coinductive types are weird and they are non-intuitive to us, because we are accustomed to thinking in terms of forming things by constructing them from building blocks. Whereas, co-inductive types are formed by deconstructing from something to the parts it was built from.

Note that bottom is a value in Haskell. See the link to Bob Harper's explanation.

 

I posted the following comment to following blog:

http://augustss.blogspot.com/2011/05/more-points-for-lazy-evaluation-in.html

I have come to the conclusion that neither an eager (a/k/a strict, e.g. most languages) nor lazy (a/k/a total, e.g. Haskell) language is vastly superior to the other. They each have tradeoffs, because they are categorical duals.

Eager is an *inductive* evaluation model, meaning we run the leaves as we as build the nested function tree of runtime possibilities.

Lazy is a *coinductive* evaluation model, meaning we run the leaves as needed from the nested function tree of runtime possibilities.

Eager can't instantiate coinductive types, such as bottom (i.e. the entire Universe) or any infinite type, but it can instantiate inductive types such as the natural numbers.

Lazy can instantiate coinductive types, such as bottom and infinite types, but it can't instantiate inductive types such as the natural numbers.

See Harper's explanation:

http://existentialtype.wordpress.com/2011/04/24/the-real-point-of-laziness/#comment-798

Eager does not have conjunctive products, so we can't do general function composition (e.g. or . map p) without potentially doing evaluation that is not shared (i.e. required) by the conjunctive result.

Lazy does not have disjunctive sums, so we can't do logic such as:

((if ... then 1 else 2),3) == if ... then (1,3) else (2,3) 

For example, if we only evaluate the second element in a lazy language and if ... has an exception, then the left version will not generate the exception, but the right version will.

I suppose most people think rather inductively.

And models can be used in eager to provide conjunctive products for some cases.

[Shelby]

On Sunday, October 7, 2012 3:51:30 AM UTC+8, Rex Kerr wrote:

 

A function which returns bottom is actually returning the entire universe

This is again completely confusing instances with sets that are duals of type intersections.

The correct semantics is it is Never returning an instance, not that is returning Nothing.

Here is an idea for the name of bottom which captures the categorical duality to the inductive universe, and also means the function can never return. This name is also correct for use as unbounded quantification on a type parameter (e.g. List[CoUniverse]).

CoUniverse

[Shelby]

We can not instantiate the entire infinite set in an eager language, so we can only refer to the infinite set by its coinductive dual type.

I am referring to an earlier message wherein I explained that eager (strict) evaluation strategy programming languages, can not instantiate the entire infinite set for inductive types, i.e. an individual element of Int can be instantiated, but the infinite set of possible Int values can not be instantiated.

In a lazy (total) evaluation strategy programming language, e.g. Haskell, an infinite set can be expressed by an infinitely recursive function, and this does not present a problem because evaluation only proceeds as needed (for as many elements of the infinite set needed), not forever. The evaluation strategy is such that infinite things are not fully evaluated. Thus bottom is instantiated (has the value _|_ falsum) in Haskell and is the supertype of every type in the program.

So in Haskell, bottom is the instance of the infinite set.

So in an eager language, bottom is CoUniverse, is the subtype of all types, and can not be instantiated.

Whereas in a lazy language, bottom is Universe, is the supertype of all types, and can be instantiated.

In the Curry-Howard correspondence, bottom is a logical contradiction to the axioms of the system. So in an eager (inductive evaluation strategy) language with inductive types, bottom can not be instantiated inductively and can only be referred to by its coinductive dual.

In a lazy (coinductive evaluation strategy) language with coinductive types, bottom populates all types as a supertype value, i.e. it is the initial object thus any defined inductive type is not an inductive type because it is populated by the entire universe, i.e. there are no true Ints in Haskell.

So bottom is always a logical contradiction.

[Rex Kerr]

Since this is only marginally on topic for Scala, maybe you can try to compress your thoughts into a smaller number of posts?  I only have a few brief remarks.

On Sun, Oct 7, 2012 at 1:52 AM, Shelby <she...@coolpage.com> wrote:

My formalism above is weak. Did I fail?

I don't know.  I haven't studied category theory.  It looks plausible given what I know, but I don't know whether that formalism maps adequately onto actual type systems.  Anyway, I actually was never arguing that there was no dual, just that naming something by its dual is liable to be confusing, especially when the duals are in some sense inverses of each other dimensionally (which is true here).  For example, I do not call a shot glass the "nearly-universe glass" because almost all the universe is outside of it.

 

 

Anyway, I am probably misunderstanding, but there seems to me to be something profoundly lacking in your view of types that is required to support the universe idea.  For example, the type Char with Double is uninhabited/uninhabitable, just like Nothing is.  But they're not the same; Char with Double promises far less than Nothing does.

 Do you refute Andriaan Moors' insight that the conjunction of two types contains the disjunction of the fields of those two types?

Of course not.  That's what I'm _declaring_.

 

I want to name the category of objects that the coalgebra of the type contains. The bottom type does not contain nothing. Nor is the use cases of the bottom giving it a semantic of nothing (as I enumerated in a prior message).

Well, I don't think that's a good idea.
 

 

  We need a type; just name the type.  Nothing is fine, as a mnemonic to remind us that it's uninhabited.

What are the use cases where it can't contain an instance (i.e. is uninhabited)? I don't know of any.

 

  Yes, we have to remember that it's not the only uninhabited type, but the Nothing type.

Can you name any other type that can't contain an instance (i.e. is uninhabited)? I can't think of one that is named.

Named?  No.  But I already gave the Char with Double example.
 

 

But we never use bottom to represent no instance. I already enumerated the use case examples in a prior message.

You have it backwards: if we never intend to return an instance (because we're not going to return normally at all, for example), we can promise whatever we want, including everything.  Hence, in cases where no instance will materialize, we naturally use Nothing.
 

 

, so maybe it's useful for exception handling or something.

An exception does not return a "can't make an instance" to the caller. It never returns to the call. And it returns an indeterminant state to some catch block. It has exposed the catch block to all possibilities, i.e. all types in the universe, thus is has returned the universe.

Did you not notice that in the JVM, the catchable value has type Throwable?  Saying it has "returned the universe" is just not correct.  First, it doesn't return normally, so saying that it has returned is wrong.  Second, that value which is given is a Throwable and isn't the universe.

  --Rex

P.S. The entropic gravity and related physics discussions are too far afield from Scala for me to continue here, except to mention that I question the parsimony of such a model; it would need to accurately predict a *lot* of data to be worth the weight of the theory.  But that's an aside better discussed in another forum.

[John Nilsson]

Den 7 okt 2012 05:22 skrev "Shelby" <she...@coolpage.com>:
> Please check the logic again. Clearly the above conclusion does not follow from the logic presented before it.
>

Clearly it is not clear to me :)

> Due to the logic for conjunction, type of bottom is neither the type of true nor false, yet it will contain the disjunction of any fields in the types of true and false. Since the types of true and false do not contain any fields, then bottom's type is not inhabited in your *finite* universe example.

I assume that by fields you mean the same thing as I meat with member.

I did define the fields of true and false like so
fields(true.type) = fields(false.type) = { ∨, ∧, ¬ }
not sure why you would say that those types do not contain any fields.

fields(Top) = fields(true.type) ∩ fields(false.type) = { ∨, ∧, ¬ }

fields(Bottom) = fields(true.type) ∪ fields(false.type) = { ∨, ∧, ¬ }

if T is a structural type then x: T iff fileds(x.type) = fields(T)

And, since Bottom is structural and fields(Bottom) = fields(true.type)
= fields(false.type) it follows that true: Bottom and false: Bottom

Then I concluded that Bottom = Top based on the premise that T = U iff
x:T ⇔ x:U and fields(T) = fields(U)

Where did I fail?

> Note to readers, afaik bottom never applies to *finite* universe, thus the type of bottom is always inhabited by the disjunction of *infinite* fields.

Ok, then my point is moot. But it does seem that both Top and Bottom
seem ok in this limited universe if we don't take Bottom to be a
structural type.

BR,
John

[Shelby]

On Monday, October 8, 2012 2:59:58 AM UTC+8, Rex Kerr wrote:

Since this is only marginally on topic for Scala,

Understanding type systems is seems to be what Scala is all about with its type parameter variance annotations, type bounds, abstract types, structural types, implicit typing, higher-kinds, implicit subsumption, dependent typing, etc..

 

maybe you can try to compress your thoughts into a smaller number of posts?  I only have a few brief remarks.

Of course in an ideal world (e.g. one where I wasn't rushing and applying exhausting effort), I would like to.

It is easier to be brief when you are not the one trying to develop a theory of the bottom type, and reading and replying with a summary to all the investigative interaction of the other person doing it.

I appreciate your brevity and your interaction.

After all, this is scala-debate.

If I had everything figured out about bottom in one nice terse summary before I posting here, I probably wouldn't be posting here to get interaction in order to feed my thought process. I am confident that Scala is not going to change the name of bottom. I am here to learn, since Scala is all about language research.

I would bet that most everyone who reads this thread is going to know more about bottom, than they did before.

 

On Sun, Oct 7, 2012 at 1:52 AM, Shelby <she...@coolpage.com> wrote:

My formalism above is weak. Did I fail?

I don't know.  I haven't studied category theory.  It looks plausible given what I know, but I don't know whether that formalism maps adequately onto actual type systems.

I don't know well either. I studied category theory briefly only.

 

  Anyway, I actually was never arguing that there was no dual, just that naming something by its dual is liable to be confusing, especially when the duals are in some sense inverses of each other dimensionally (which is true here).  For example, I do not call a shot glass the "nearly-universe glass" because almost all the universe is outside of it.

Afaics this analogy does not correlate.

The development of the last few posts of mine is that in an eager language, the only way to represent the Universe, is by its coinductive dual form. Thiis coinductive form is no less the universe for an eager language, than the inductive form is in a lazy language. And so in an eager language, the CoUniverse is the Universe. Our Universe is a contradiction, it has both inductive and coinductive forms simultaneously. Anything that is infinite will have this contradiction. This is why bottom is a contradiction in the Curry-Howard correspondence.

If you name bottom something less than the universe (or at least less than the subtype of all types in eager or supertype of all types in lazy), then the name is not correct.

 

 

 

Anyway, I am probably misunderstanding, but there seems to me to be something profoundly lacking in your view of types that is required to support the universe idea.  For example, the type Char with Double is uninhabited/uninhabitable, just like Nothing is.  But they're not the same; Char with Double promises far less than Nothing does.

 Do you refute Andriaan Moors' insight that the conjunction of two types contains the disjunction of the fields of those two types?

Of course not.  That's what I'm _declaring_.

I later realized that you were only claiming there is nothing of instances in bottom. But when I had asked you that, I had thought you were saying there was nothing in bottom's type, because I thought you were saying (or thinking) that a conjunction of infinite types is empty (but it is not empty because it is also the structural type that has the disjunction of all the fields).

 

 

I want to name the category of objects that the coalgebra of the type contains. The bottom type does not contain nothing. Nor is the use cases of the bottom giving it a semantic of nothing (as I enumerated in a prior message).

Well, I don't think that's a good idea.

But I haven't seen a good reason for naming something nothing, when it is the universe.

I haven't even seen a use case where bottom is semantically nothing.

 

 

 

  We need a type; just name the type.  Nothing is fine, as a mnemonic to remind us that it's uninhabited.

What are the use cases where it can't contain an instance (i.e. is uninhabited)? I don't know of any.

 

  Yes, we have to remember that it's not the only uninhabited type, but the Nothing type.

Can you name any other type that can't contain an instance (i.e. is uninhabited)? I can't think of one that is named.

Named?  No.  But I already gave the Char with Double example.

Right. So if bottom is the only named type we have that has no instances, that gives you a pretty strong indication that it is the universe, since we know the only thing we can't instantiate in an eager language is an infinite thing.

All those verbose posts were contributing to the logical conclusion here.

 

 

 

But we never use bottom to represent no instance. I already enumerated the use case examples in a prior message.

You have it backwards: if we never intend to return an instance (because we're not going to return normally at all, for example), we can promise whatever we want, including everything.  Hence, in cases where no instance will materialize, we naturally use Nothing.

From my perspective, that is illogical.

If the name has no semantics in that context (your logical proposition, which I disagree, below...), then logically the name doesn't matter in that context and should be based on context(s) where it does have semantics, such as in the List[Nothing], where it does not mean a list of members of type nothing. So the name is incorrect. Whereas, CoUniverse would fit correctly (so would Bottom and SubOfAll, or even All perhaps but disfavor All's ambiguity with top).

If you are going to prioritize a name that is most intuitive for non-terminating functions (notwithstanding if name has semantics in that context), then Never is better. And a list of members of type Never is more correct. An empty list won't have members of type nothing, it won't have members. The verb works much better, even though it still isn't 100% correct.

If a non-terminating function returns CoUniverse, then it is clear that it returns no instance, but it can be assigned to any structural type that has any of the fields of any type in the universe. So that is telling you is your function that catches the exception (the return value) could be any method in the program. So it is mathematically congruent to what an exception can do.

 

 

 

, so maybe it's useful for exception handling or something.

An exception does not return a "can't make an instance" to the caller. It never returns to the call. And it returns an indeterminant state to some catch block. It has exposed the catch block to all possibilities, i.e. all types in the universe, thus is has returned the universe.

Did you not notice that in the JVM, the catchable value has type Throwable?  Saying it has "returned the universe" is just not correct.  First, it doesn't return normally, so saying that it has returned is wrong.  Second, that value which is given is a Throwable and isn't the universe.

The return value of an exception is the coinductive form, not what is being return, but where it is being returned to.

Another math proof? I am bit tired, so I will establish that more later, and perhaps in a different forum.

 

  --Rex

P.S. The entropic gravity and related physics discussions are too far afield from Scala for me to continue here, except to mention that I question the parsimony of such a model; it would need to accurately predict a *lot* of data to be worth the weight of the theory.  But that's an aside better discussed in another forum.

Unifying many well established major theories of the universe as congruent with an entropic interpretation, seems to worthwhile even if there never arise predictions that are not also predicted by the major theories. I find it fascinating, because I think the universe is not as fragmented as all these proliferation of theories since relativity suggest.

[Shelby]

On Monday, October 8, 2012 4:54:56 AM UTC+8, John Nilsson wrote:

I did define the fields of true and false like so
fields(true.type) = fields(false.type) = { ∨, ∧, ¬ }

[...]

Where did I fail?

Top's type (being a disjunction of all types) would have the conjunction of all fields, and Bottom's type (being a conjunction of all types) would have the disjunction of all fields, so Top would not equal Bottom.

[Shelby]

 

 Do you refute Andriaan Moors' insight that the conjunction of two types contains the disjunction of the fields of those two types?

 

Yikes, if the disjunction of some types is the structural type with the conjunction of the fields of those types, then if Scala ever adds first-class disjunctions and also keeps the ability to instantiate structural typs, then it means functions returning a disjunction can't be assigned to the named types in the disjunction (note they are subtypes of the disjunction). They can only be assigned to a structural type with NO fields, because we can not assume the function is not returning a structural type no fields. Without structural types, then the disjunction must contain a named subtype from the disjunction (and that named subtype will have its fields).

Afaics, the ability to instantiate structural types is incompatible with a first-class disjunction type.

I will also post this to scala-language in the thread where Andriaan mentioned the quoted idea above.

[Rex Kerr]

On Sun, Oct 7, 2012 at 5:02 PM, Shelby <she...@coolpage.com> wrote:

The development of the last few posts of mine is that in an eager language, the only way to represent the Universe, is by its coinductive dual form. Thiis coinductive form is no less the universe for an eager language, than the inductive form is in a lazy language. And so in an eager language, the CoUniverse is the Universe. Our Universe is a contradiction, it has both inductive and coinductive forms simultaneously. Anything that is infinite will have this contradiction. This is why bottom is a contradiction in the Curry-Howard correspondence.

Why is it not the case that the CoUniverse is the CoUniverse and the Universe is the Universe?  In particular, you have built a type that claims instances of it can do anything and everything that any other type can do.  This is _not a property of the universe_ since, for example, it doesn't make any sense to negate the universe as negation isn't defined on most things in it.  You _can_ identify this peculiar type with the universe via an isomorphism--that's fine--but where we part company is that you want to call this the universe.  It's not.  It is it's very own thing, a conjunction of all types, and instead of searching for a name that describes it, you want to use the name for its dual.
 

If you name bottom something less than the universe (or at least less than the subtype of all types in eager or supertype of all types in lazy), then the name is not correct.

I think you're missing something, but I don't have time to check.  Laziness ought not change the typing relationship, only whether something can be "instantiated" when it can't actually be computed.
 

 

 

I want to name the category of objects that the coalgebra of the type contains. The bottom type does not contain nothing. Nor is the use cases of the bottom giving it a semantic of nothing (as I enumerated in a prior message).

Well, I don't think that's a good idea.

But I haven't seen a good reason for naming something nothing, when it is the universe.

I haven't even seen a use case where bottom is semantically nothing.

I think that's because you're trying to name things on the basis of what the fields/methods are, and I'm trying to name the on the basis of what the set of instances is.  That is, when you name something Int, do you say, "Well, this type has methods +,-,* and is inhabited by an additive and multiplicative zero, etc. so I will call it Int", or do you say, "Well, this has elements 0,1,-1,2,-2,... which are the integers, and therefore I will call it Int"?

The naming conventions we use, I argue, are most of the what-instances-can-be-here.  For example, Int and a hypothetical UnsignedInt would have exactly the same methods, but in one case you interpret the 0xFFFFFFFF as -1 and in the other as 4294967295 (when converting to other types).  In your interpretation, since the fields/methods are the same for the two types they ought to get the same name.

So, anyway, I reject all this "let's call the universal conjunction type Universe" business.  That's not how we normally name types, and naming it using the opposite convention from normal isn't likely to yield much insight as to how to use it.  I don't think "Nothing" is necessarily the best, since as we've both pointed out it's not the only possible uninhabited type, but it's way, way better than Universe.  There are no instances in Nothing.  You don't find a Universe in there; if you could instantiate it, it would be the dual of the universe and have really interesting properties but it wouldn't be the universe.  And in Scala you can't even instantiate it.  So calling it Universe is a really bad idea.  Universal would hit nearer the mark as it wouldn't confuse name-via-dual vs. name-via-instances so badly, but I don't like that this implies that it might be possible to have one of these magic Universal things (which would work by, I suppose, keeping a Universe in its pocket and picking out just the right element from the universe to fit any given context it found itself in).

If a non-terminating function returns CoUniverse, then it is clear that it returns no instance, but it can be assigned to any structural type that has any of the fields of any type in the universe. So that is telling you is your function that catches the exception (the return value) could be any method in the program. So it is mathematically congruent to what an exception can do.

Well, yes, in that sense it is, if you adjust your blinders exactly the right way.  But this isn't a particularly useful property to notice.  (In any particular program, an exception can only be caught by things in the stack trace, which produce way less diversity than anything in the universe, typically.  And you completely ignore the fact that exceptions carry a payload; they're not just control flow.)
 

 

 

, so maybe it's useful for exception handling or something.

An exception does not return a "can't make an instance" to the caller. It never returns to the call. And it returns an indeterminant state to some catch block. It has exposed the catch block to all possibilities, i.e. all types in the universe, thus is has returned the universe.

Did you not notice that in the JVM, the catchable value has type Throwable?  Saying it has "returned the universe" is just not correct.  First, it doesn't return normally, so saying that it has returned is wrong.  Second, that value which is given is a Throwable and isn't the universe.

The return value of an exception is the coinductive form, not what is being return, but where it is being returned to.

Have you read about the equivalence of programs using exception handling and transformation of that program using Either?  This is the useful duality to think about.  "Where it is being returned to" is not the useful type information; rather it is "what is being returned".  I can't find the reference at the moment; maybe you've seen the paper (or something that refers to it)?

  --Rex

[Rex Kerr]

Indeed.  There are two things you might mean by A | B.  If {a|a is A} is the set of all possible instances of an A--let's abbreviate it {A}--and likewise for B, then you might mean {A} union {B}.  But if you work at the field/method level--let's say iA is the interface of A (methods, fields, whatever, in a set) and iB is for B--then you might mean iA intersect iB.  Either captures the first case; structural types capture the second.  A first class union type has to decide which it is.  It is certainly _not_ the case that you can _equate_ a sum type with a structural type with the intersection of members of the types in the sum.  You can use the structural type to safely operate on the sum type, however (it is a supertype of the sum type).

I'm not sure this qualifies as a momentous insight, though, since there can be multiple types with the exact same methods.  All marker traits are of this sort, for example--as far as fields and methods go, they're indistinguishable from Object or whatever it is they inherit from.  You can "fix" this problem by assuming that each named type T has a unique method iAmTheTypeT just to mark it, but this fix doesn't work for fixing the first-class intersection type ambiguity.

  --Rex

[John Nilsson]

On Sun, Oct 7, 2012 at 11:17 PM, Shelby <she...@coolpage.com> wrote:
> Top's type (being a disjunction of all types) would have the conjunction of
> all fields, and Bottom's type (being a conjunction of all types) would have
> the disjunction of all fields, so Top would not equal Bottom.

Now its your conclusion that doesn't follow the logic. :P

My point was precisely that in this limited universe the conjunction
and disjunction of fields are the same, and this is why Top would
equal Bottom if there is nothing else defining Bottom.

BR,
John

[Rex Kerr]

In Shelby's framework (as I understand it), you only have one type.  Top, True.type, False.type, and Bottom are all the same type, since they all have the same interface.  (I don't think this is either a useful way to think about types or consistent with Scala's type system.)

  --Rex

[Shelby]

On Monday, October 8, 2012 5:57:33 AM UTC+8, Rex Kerr wrote:

On Sun, Oct 7, 2012 at 5:02 PM, Shelby <she...@coolpage.com> wrote:

The development of the last few posts of mine is that in an eager language, the only way to represent the Universe, is by its coinductive dual form. Thiis coinductive form is no less the universe for an eager language, than the inductive form is in a lazy language. And so in an eager language, the CoUniverse is the Universe. Our Universe is a contradiction, it has both inductive and coinductive forms simultaneously. Anything that is infinite will have this contradiction. This is why bottom is a contradiction in the Curry-Howard correspondence.

Why is it not the case that the CoUniverse is the CoUniverse and the Universe is the Universe?  [...]  You _can_ identify this peculiar type with the universe via an isomorphism--that's fine--but where we part company is that you want to call this the universe.  It's not.  It is it's very own thing, a conjunction of all types, and instead of searching for a name that describes it, you want to use the name for its dual.

 

I am proposing to name it CoUniverse, not its dual Universe. I am saying that in the context of an eager language, the CoUniverse is the form of the universe. The CoUniverse is the coinductive formation of the universe. It does not have the same properties in an eager setting as the inductive universe has in a lazy setting.

But it is not less the universe, because our universe has a coinductive form from an eager perspective (where we declare everything inductively), and our universe simultaneously exists in an inductive form from a lazy perspective (where declare everything coinductively).

So I could choose the name Universe, as long as it was understood that this was the coinductive form of the universe. I preferred CoUniverse in order to make it clear.

 
In particular, you have built a type that claims instances of it can do anything and everything that any other type can do.  This is _not a property of the universe_ since, for example, it doesn't make any sense to negate the universe as negation isn't defined on most things in it. 
 

You are arguing against properties of the universe when it is expressed inductively. The universe also simultaneously exists in a coinductive form.

You have stated it above. The coinductive form claims to be able to do anything that any other type can do (has a disjunction of all fields and is the subtype of them all). Doesn't our universe also do everything that can be done in it?

If you define the universe inductively in a lazy language, then the Universe (bottom) claims to be all types. So here the universe is defined to be the types. And in the coinductive form the universe is defined to do what ever its types can do. Those are just dual ways of expressing the same universe. The expression is driven by the evaluation strategy of the language, eager or lazy.

 

 

If you name bottom something less than the universe (or at least less than the subtype of all types in eager or supertype of all types in lazy), then the name is not correct.

I think you're missing something, but I don't have time to check.  Laziness ought not change the typing relationship, only whether something can be "instantiated" when it can't actually be computed.

Laziness flips everything from inductive to coinductive (or vice versa).

 

 

 

 

I want to name the category of objects that the coalgebra of the type contains. The bottom type does not contain nothing. Nor is the use cases of the bottom giving it a semantic of nothing (as I enumerated in a prior message).

Well, I don't think that's a good idea.

But I haven't seen a good reason for naming something nothing, when it is the universe.

I haven't even seen a use case where bottom is semantically nothing.

I think that's because you're trying to name things on the basis of what the fields/methods are, and I'm trying to name the on the basis of what the set of instances is.

In an eager language, the set of instances of bottom is degenerate. All the information about the universe it in the type of bottom in an eager language.

In a lazy language, all the information about bottom is the set of types it is inhabited by (all of them).

You are trying to choose a name based on the wrong evalution strategy for Scala.

That is why Nothing does not have any correct semantics for the use cases.

 

  That is, when you name something Int, do you say, "Well, this type has methods +,-,* and is inhabited by an additive and multiplicative zero, etc. so I will call it Int", or do you say, "Well, this has elements 0,1,-1,2,-2,... which are the integers, and therefore I will call it Int"?

No because Int is defined inductively in an eager language.

The universe (bottom) is defined coinductively in an eager language and inductively in a lazy language.

 

The naming conventions we use, I argue, are most of the what-instances-can-be-here.  For example, Int and a hypothetical UnsignedInt would have exactly the same methods, but in one case you interpret the 0xFFFFFFFF as -1 and in the other as 4294967295 (when converting to other types).  In your interpretation, since the fields/methods are the same for the two types they ought to get the same name.

So, anyway, I reject all this "let's call the universal conjunction type Universe" business.  That's not how we normally name types, and naming it using the opposite convention from normal isn't likely to yield much insight as to how to use it.

That is because you are nearly always naming inductive types (except for Stream, CoMonad, and a few other exotics, like bottom).

 

  I don't think "Nothing" is necessarily the best, since as we've both pointed out it's not the only possible uninhabited type, but it's way, way better than Universe.

Strongly disagree. For all the reasons I have explained in this reply and the reply before this one.

 

  There are no instances in Nothing.

Irrelevant.

 

  You don't find a Universe in there; if you could instantiate it, it would be the dual of the universe and have really interesting properties but it wouldn't be the universe.

Wrong for the reasons I have explained in this reply.

 

  And in Scala you can't even instantiate it.  So calling it Universe is a really bad idea.

That would be claiming that lazy languages can instantiate the universe and eager ones don't have any representation form of the universe. We know intuitively that can be true. I explained above in this reply how eager languages do have a universe and it is the coinductive form.

 

  Universal would hit nearer the mark as it wouldn't confuse name-via-dual vs. name-via-instances so badly,

Wrong. That is the top type. Universal is referring the instances in it. It is for inductive subtypes. Universal does not mean Universal. Dictionary says so.

 

but I don't like that this implies that it might be possible to have one of these magic Universal things (which would work by, I suppose, keeping a Universe in its pocket and picking out just the right element from the universe to fit any given context it found itself in).

If a non-terminating function returns CoUniverse, then it is clear that it returns no instance, but it can be assigned to any structural type that has any of the fields of any type in the universe. So that is telling you is your function that catches the exception (the return value) could be any method in the program. So it is mathematically congruent to what an exception can do.

Well, yes, in that sense it is, if you adjust your blinders exactly the right way.  But this isn't a particularly useful property to notice.  (In any particular program, an exception can only be caught by things in the stack trace, which produce way less diversity than anything in the universe, typically.  And you completely ignore the fact that exceptions carry a payload; they're not just control flow.)

The payload is determining who will catch the exception and what message they will receive. It has nothing to do with the fact that any method in the program could be the one that catches, which is what the return value of CoUniverse is declaring. You are conflating orthogonal issues.

 

 

 

, so maybe it's useful for exception handling or something.

An exception does not return a "can't make an instance" to the caller. It never returns to the call. And it returns an indeterminant state to some catch block. It has exposed the catch block to all possibilities, i.e. all types in the universe, thus is has returned the universe.

Did you not notice that in the JVM, the catchable value has type Throwable?  Saying it has "returned the universe" is just not correct.  First, it doesn't return normally, so saying that it has returned is wrong.  Second, that value which is given is a Throwable and isn't the universe.

The return value of an exception is the coinductive form, not what is being return, but where it is being returned to.

Have you read about the equivalence of programs using exception handling and transformation of that program using Either?  This is the useful duality to think about.  "Where it is being returned to" is not the useful type information; rather it is "what is being returned".  I can't find the reference at the moment; maybe you've seen the paper (or something that refers to it)?

I do remember that paper. But can't remember the content of it. I don't think that transformation changes the fact that the function throwing the exception can't control which function in the universe is going to catch the exception. The function is giving up that control, which I posit is what the CoUniverse declares as a return value.

[Shelby]

On Monday, October 8, 2012 6:47:24 AM UTC+8, Shelby wrote:

Wrong. That is the top type. Universal is referring the instances in it. It is for inductive subtypes. Universal does not mean Universal. Dictionary says so.

 

Typo: second "Universal" should be "Universe"

[John Nilsson]

This is more or less how I understands it too. But somewhere I got the
impression that other kinds (no pun intended) of types could exists in
this framework, but Bottom, by some logic I didn't get, could only be
structural. Which, I tried to show, has consequences on those other
types ending up in the Boolean universe only having one type.

I agree that this isn't consistent with Scala, and I guess there is
some utility in having four types instead of one. However I am open to
the possibility that reducing it to one type provides some attractive
properties regarding closure.

BR,
John

[Shelby]

If the disjunction of the type names true and false is allowed to be a structural type, then disjunctions don't work correctly as return values, as I stated in a recent message (realizing it after replying to you previously on this).

So I think we have to disallow structural types for first-class disjunctions. If so, then Top would not equal Bottom in your example, because Bottom (a conjunctive type) is a structural type and the disjunction would be the disjunction of the type names true or false.

[John Nilsson]

On Sat, Oct 6, 2012 at 7:12 PM, Shelby <she...@coolpage.com> wrote:
>> B) If your point is that Universe can't be instantiated because it must
>> have all possible members I think you are wrong. Wouldn't such an instance
>> simply be the equivalent of a dynamicly typed object responding to every
>> possible message?
>
> Oh sure if you want to throw away static typing, then you can model the
> universe with runtime semantics, but still your code is a coinductive
> algebra, because you can't respond to every possible message, without
> knowing the structure of every possible message. You end up with default
> cases that don't respond or throw exceptions.

Lets revisit this. There was no reason for me refer to dynamic types
here, I was thinking of an implementation technique like using a
DynamicProxy to implement a static type. The type implemented is still
static though. So to rephrase:

If we have a type Universe, defined as the structural type including
all possible member signatures, would it really not be possible to
provide an implementation of that type?

We do know the structure of every possible message it's simply some
identifier and some parameters, all we need is to return a value of
the correct type. And by definition we have a perfectly valid response
to all messages: this.

BR,
John

[Shelby]

On Monday, October 8, 2012 6:39:34 AM UTC+8, Rex Kerr wrote:

In Shelby's framework (as I understand it), you only have one type.  Top, True.type, False.type, and Bottom are all the same type, since they all have the same interface.  (I don't think this is either a useful way to think about types or consistent with Scala's type system.)

I am thinking structural types can't be allowed for first-class disjunctions. So then we will still have the four types. 

Why would we want to allow structural types to be assigned to disjunctions of named types? This is saying that every disjunction includes by default the type with no name.

Also I think maybe I misunderstood the math that Andriaan implied. Wouldn't the disjunction of the named types, be the conjunction of the fields for each named type separately, not all fields lumped separately from their type names? If yes, then afaics structural types are not incompatible with first-class disjunctions.

[John Nilsson]

On Mon, Oct 8, 2012 at 1:14 AM, Shelby <she...@coolpage.com> wrote:
> Also I think maybe I misunderstood the math that Andriaan implied. Wouldn't
> the disjunction of the named types, be the conjunction of the fields for
> each named type separately, not all fields lumped separately from their type
> names? If yes, then afaics structural types are not incompatible with
> first-class disjunctions.

Hmm, ok that looks like it would resolve some issues
My point was exactly that a simple structural type can't really be
sub-type of a nominal type, because it could inhabit objects violating
the nominal type contract.


So we would have fields(Bottom) = { true.type.∨, true.type.∧,
true.type.¬, false.type.∨, false.type.∧, false.type.¬ }
and I guess, by extension, fields(Top) = {}

Two problems with this though.
1. The Bottom type doesn't really prohibit any implementations. But at
least it won't be true or false. I also guess your point about finite
universes applies too.
I still think it's simpler to say that x:Bottom iff x:true.type ∧
x:false.type though, so I still doesn't see why you insist on Bottom
to be purely structural.

2. I guess we've now lost dynamic dispatch, in this new Boolean
universe we can only call methods on instances of true.type or
false.type. Is this a feature? Do we add a Boolean type to the
universe? How do we define it?

BR,
John

[Shelby]

On Monday, October 8, 2012 7:45:18 AM UTC+8, John Nilsson wrote:

On Mon, Oct 8, 2012 at 1:14 AM, Shelby wrote:
> Also I think maybe I misunderstood the math that Andriaan implied. Wouldn't
> the disjunction of the named types, be the conjunction of the fields for
> each named type separately, not all fields lumped separately from their type
> names? If yes, then afaics structural types are not incompatible with
> first-class disjunctions.

Hmm, ok that looks like it would resolve some issues

The above was not intended to apply to bottom.

 

My point was exactly that a simple structural type can't really be
sub-type of a nominal type, because it could inhabit objects violating
the nominal type contract.

Good point.

I thinking we don't get a structural type. I am thinking we get a type without a name, but each the fields are tagged with the name of the type they appeared in. Then we get what I was starting above, plus we get the correct result for bottom too.

 

So we would have fields(Bottom) = { true.type.∨, true.type.∧,
true.type.¬, false.type.∨, false.type.∧, false.type.¬ }
and I guess, by extension, fields(Top) = {}

Yeah I think that is what I was thinking now, with name of the type tagged to each field.

 

Two problems with this though.
1. The Bottom type doesn't really prohibit any implementations. But at
least it won't be true or false. I also guess your point about finite
universes applies too.

Infinite bottom would not have any instances.

 

I still think it's simpler to say that x:Bottom iff x:true.type ∧
x:false.type though, so I still doesn't see why you insist on Bottom
to be purely structural.

Maybe I am not following you, but I am just trying to incorporate Andriaan's point that the conjunction of types as the disjunction of the type's fields.

 

2. I guess we've now lost dynamic dispatch, in this new Boolean
universe we can only call methods on instances of true.type or
false.type.

I don't understand.

[Shelby]

On Monday, October 8, 2012 10:10:45 AM UTC+8, Shelby wrote:

On Monday, October 8, 2012 7:45:18 AM UTC+8, John Nilsson wrote:

On Mon, Oct 8, 2012 at 1:14 AM, Shelby wrote:
> Also I think maybe I misunderstood the math that Andriaan implied. Wouldn't
> the disjunction of the named types, be the conjunction of the fields for
> each named type separately, not all fields lumped separately from their type
> names? If yes, then afaics structural types are not incompatible with
> first-class disjunctions.

Hmm, ok that looks like it would resolve some issues

The above was not intended to apply to bottom.

 

My point was exactly that a simple structural type can't really be
sub-type of a nominal type, because it could inhabit objects violating
the nominal type contract.

Good point.

I thinking we don't get a structural type. I am thinking we get a type without a name, but each the fields are tagged with the name of the type they appeared in. Then we get what I was starting above, plus we get the correct result for bottom too.

Typos: s/starting/stating/

s/I thinking/I am thinking/

s/each the fields/each of the fields/

John I think you have pointed out that bottom has all the instances of structural types. Because if bottom is defined to be the conjunction of all types, then it must include structural types in the conjunction. But since the conjunction of types includes the disjunction of their fields, then we have the fields for the structural type in bottom's type. Thus instances of structural types can be assigned to bottom. Thus bottom is no longer a subtype of all types.

In short, the structural type (name) doesn't disappear from the conjunction of type names, because it doesn't have a name and thus matches any type of any name.

So I think we can conclude that structural types are unsound. I have always had the intuition that equating a named type to an unnamed type is unsound.

And this makes it more firm in my mind that the conjunction of named types, have the disjunction of their fields, but these fields remain tagged by the name of the type they appear in. The reason is because the semantics of our typing system is that we don't match fields from named types with fields from other named types. Structural types don't have this restriction, the semantics of structural types is matching fields by ignoring the name of types, so structural types are unsound.

[Shelby]

The implication of the prior reply below, is that there is no basis from which to say the universe is an inductive form, more so than it is a coinductive form.

We humans appear more comfortable thinking about inductive types, where we enumerate subtypes (or succeeding instances) with a morphism from a prior supertype (or initial object). So it we think intuitively about the inductive form of the universe's instances, where we add them to a set using a succeeding function Axiom of Infinity.

But the contradiction of the universe is that the inductive algebra of the infinite universe (taken as a whole, not the parts which is instead is the top type in an eager language), is that we can not build that inductive algebra in an inductive (eager) language.

So this tells us that the universe is not an inductive form in an inductive language. But it must still exist in an inductive expression, and it does in the coinductive representation.

Vice versa the above two paragraphs for a lazy language.

Corollary is that a lazy language does not have inductive subtyping (specifically virtual inheritance). It has coinductive subtyping, which afaics is why we have a very different mechanism for expressing covariant relationships in Haskell as compared to the inductive languages:

https://groups.google.com/d/msg/scala-language/PIhmEeMg-Ms/2rdvRNz8vn8J

[Ryan Hendrickson]

> John I think you have pointed out that bottom has all the instances of
> structural types. Because if bottom is defined to be the conjunction of
> all types, then it must include structural types in the conjunction. But
> since the conjunction of types includes the disjunction of their fields,
> then we have the fields for the structural type in bottom's type. Thus
> instances of structural types can be assigned to bottom. Thus bottom is
> no longer a subtype of all types.

I can't make enough sense out of most of this discussion to believe or refute it, but this statement is certainly wrong. You can't assign a value x inhabiting a structural type A to another structural type B without proof (or type-system-bypassing assertion) that all of the members of B are also present in x. If Bottom is (a subtype of) the conjunction of all structural types, and thus contains all members, then to say that x inhabits *some* structural type is certainly not sufficient to prove that x has every member ever and thus could be an inhabitant of Bottom. I think you've been tripped up on your own type-to-member subset contravariance argument.

> And this makes it more firm in my mind that the conjunction of named
> types, have the disjunction of their fields, but these fields remain
> tagged by the name of the type they appear in. The reason is because the
> semantics of our typing system is that we don't match fields from named
> types with fields from other named types. Structural types don't have
> this restriction, the semantics of structural types is matching fields
> by ignoring the name of types, so structural types are unsound.

You could design an unsound type system this way, but Scala's type system is not this. The rules governing the subtyping relation between named types and structural types are quite clear: named types relate between each other by closing over explicit ‘extends’ declarations, and structural types extend that relation to include additional constraints based on a well-defined members function from types to sets of (name, method type) pairs. They absolutely do not ignore the names of types (even though the members function also absolutely does not tag its range with type names); try for yourself:

trait Named {
def foo: Int
}

type Structural = {
def foo: Int
}

implicitly[Named => Structural] // proves Named is a subtype of Structural
implicitly[Structural => Named] // will fail, proving that Structural is not a subtype of Named






(please forgive me my corporate legal disclaimer)

----------------------------------------

This message is intended exclusively for the individual(s) or entity to
which it is addressed. It may contain information that is proprietary,
privileged or confidential or otherwise legally exempt from disclosure.
If you are not the named addressee, you are not authorized to read,
print, retain, copy or disseminate this message or any part of it.
If you have received this message in error, please notify the sender
immediately by e-mail and delete all copies of the message.

[Shelby Moore]

>> John I think you have pointed out that bottom has all the instances of
>> structural types. Because if bottom is defined to be the conjunction of
>> all types, then it must include structural types in the conjunction.
>> But
>> since the conjunction of types includes the disjunction of their
>> fields,
>> then we have the fields for the structural type in bottom's type. Thus
>> instances of structural types can be assigned to bottom. Thus bottom is
>> no longer a subtype of all types.
>
> I can't make enough sense out of most of this discussion to believe or
> refute it, but this statement is certainly wrong. You can't assign a value
> x inhabiting a structural type A to another structural type B without
> proof (or type-system-bypassing assertion) that all of the members of B
> are also present in x.

I thought I did prove it above. Let me explain more.

> If Bottom is (a subtype of) the conjunction of all
> structural types, and thus contains all members,

Do you means 'fields' when you write 'members'?

I think it helps to understand my logic, by first considering what top
means for structural types.

Top is the disjunction of all types (including the "unnamed name" because
unnamed types can never be subtypes of named types), thus the type of top
is the disjunction of the type names and has the conjunction of all sets
of fields of those types. Thus logically top can have any type name, or
"unnamed named" structural type, and has no sets of fields.

This works because all types will have no fields or more fields than top,
thus will contain a the same or narrower set of instances. Any set with
more rules that the instances must fulfill, is either the same or narrower
set.

Bottom is the conjunction of all types, thus the type of bottom is the
conjunction of the type names (not including the "unnamed name" because
unnamed types can be supertypes by matching only fields) and has the
disjunction of all sets of fields of those types. Thus logically bottom
can't have any type name, can have any unnamed type (since the conjunction
of type names does not exclude it, structural types can match other
structural types if the fields match in this contravariant direction), and
can have any set of fields.

Thus every structural type is also bottom, because it is not excluded by
type name and its fields are not less narrow than bottom, because bottom
is the disjunction of any set of fields. Remember a disjunction is not all
things in the disjunction simultaneously, rather it is any one of them.
Thus since bottom has the disjunction of all sets of fields, then it
matches the fields for any type. But normally the conjunction of type
names disallows types from inhabiting bottom, but this is not the case for
the unnamed structural types. (See Ryan's example below of how unnamed
types can be supertypes of named types, but not vice versa)

The proof is that by erasing the names, the disjunction and conjunction of
the type names (for top and bottom respectively) is equivalent for unnamed
types. Top and bottom are equivalent for structural types.

> then to say that x
> inhabits *some* structural type is certainly not sufficient to prove that
> x has every member ever and thus could be an inhabitant of Bottom.

Since I don't know what you meant by 'member', I can't state what is wrong
with your logic here.

> I think
> you've been tripped up on your own type-to-member subset contravariance
> argument.

I don't think so. Until I know what you meant by 'member', I can't explain
what is the possible misunderstanding.

>
>> And this makes it more firm in my mind that the conjunction of named
>> types, have the disjunction of their fields, but these fields remain
>> tagged by the name of the type they appear in.

I continue to assert this, until someone shows otherwise. I note below
that for example that method fields input the type as `this`, which is a
form of tagging.

>> The reason is because
>> the
>> semantics of our typing system is that we don't match fields from named
>> types with fields from other named types.

I don't think this has been refuted either yet.

>> Structural types don't have
>> this restriction, the semantics of structural types is matching fields
>> by ignoring the name of types, so structural types are unsound.

What is shown below is that structural types ignore type names in one
direction of covariance, but not the other.

I have incorporated this fact in my proof above. You actually helped me,
because now I can say that in the contravariant direction, then an unnamed
type can be a member of the conjunction of the named types (i.e. bottom).

>
> You could design an unsound type system this way, but Scala's type system
> is not this.

I was referring to Andriaan Moors idea (linked below) for the more
generalized type system in a possible overhaul of Scala.

https://groups.google.com/d/msg/scala-language/z89k3_8U528/laUOSrFDpM4J

> The rules governing the subtyping relation between named
> types and structural types are quite clear: named types relate between
> each other by closing over explicit ‘extends’ declarations,

I had assumed that in Scala today `extends` is only a subtyping relation
when there are two names to compare. I now see below that Scala will never
allow an unnamed type to be the subtype of a named type, because there is
no `extends` in the structural structural type.

So this makes good sense. We can use structural types to access the
instances of matching named types, but we can't used named types to access
the instances of matching structural types.

> and structural
> types extend that relation to include additional constraints based on a
> well-defined members function from types to sets of (name, method type)

> pairs.).

> They absolutely do not ignore the names of types

You showed below that they do ignore names in the one direction of
covariance but not in the other (contravariance).

> (even though the
> members function also absolutely does not tag its range with type names);

Afaics, the methods of named types are tagged, because the methods input
`this`.

In any case, you resolved the original problem I was concerned about,
where I was thinking a structural type could be returned in a future
first-class disjunction of named types. Clearly that can not be, because
of your example below. A named typed can hold an instance of an unnamed
type (because you showed below that an unnamed type is never a subtype of
a named type, unless it provided an explicit `extends` in its
declaration).

[Shelby Moore]

Typos.

> Top is the disjunction of all types (including the "unnamed name" because
> unnamed types can never be subtypes of named types),

That is unnamed types that did not have an explicit `extends` declaration.

> can't have any type name, can have any unnamed type (since the conjunction
> of type names does not exclude it, structural types can match other
> structural types if the fields match in this contravariant direction),

can match other types if fields match... (not just structural types)

The point is that the conjunction of the named types does not exclude a
structural type in this contravariant direction.

> type name and its fields are not less narrow than bottom,

And its fields are not more restrictive than bottom (the instances are not
less narrow)

> of your example below. A named typed can hold an instance of an unnamed

A named type can NOT hold...

[Shelby]

On Tuesday, October 9, 2012 1:07:18 AM UTC+8, Shelby wrote:

In any case, you resolved the original problem I was concerned about,
where I was thinking a structural type could be returned in a future
first-class disjunction of named types.

Just to be clear, you resolved one issue.

But afaics, you have not resolved my claim that structural types are unsound, because they inhabit Bottom.

[Alex Repain]

Shelby, I think you are losing a fair number of us in this debate. If you want to prove some things, and think you have proven some, could you state these proofs in an adequate formal language, so we can take our time to understand them without fearing losing tracks ? In short, if you think you've proven new things, you should definitely try writing a paper about it. If it's not new things, please reference your statements. I think it will be an improvement for all of us, if not, you will probably end up talking to yourself.

I'd like to go to the bottom of this, but either my brain say no young padawan, you must first learn the way of the Force, or I stumble upon your posts - they all reads almost the same to me , and I can't seem to penetrate them. Please formalize all of this :).

2012/10/8 Shelby Moore <she...@coolpage.com>

[Alex Repain]

Sorry for the double-post but don't take me wrong, I definitely appreciate the effort and time you put in trying to explain your theory to us, but at the level of (non-)comprehension, I think you should use a better medium than mailing lists.

2012/10/8 Alex Repain <alex....@gmail.com>

[Shelby]

I agree.

It is getting different to wrap one's head around the entire discussion.

I am curious what if anything I missed from Ryan Hendrickson's point about "member"ship.

[Shelby]

On Tuesday, October 9, 2012 3:08:43 AM UTC+8, Shelby wrote:

I am curious what if anything I missed from Ryan Hendrickson's point about "member"ship.

 I now think Ryan is correct. Structural types don't inhabit bottom.

He also showed why structural types are not unsound with the first-class disjunction, because it doesn't make sense to allow a named type to hold an instance of a unnamed type (that didn't inherit that named type with an `extends`). Thus it is not possible to return such an unnamed structural type from a function that returns a first-class disjunction of named types (which was my concern before).

Those resolved my questions about unsoundness of structural types.

They do NOT impact my logic that bottom is the coinductive universe.

I will try to explain why I think structural types don't inhabit bottom and what my confusion was.

The reason that the conjunction of types includes the disjunction of the fields, or dually the disjunction of types includes the conjunction of the fields, is because the set of inhabiting instances is more *narrow* as the type's fields are *wider*. Thus there is an inverse relationship (narrow vs. wide) between the logical mapping of the types and the fields of the types.

I had stated that bottom is like a structural type, because the conjunction of its types, is like having no names yet having all the fields. This was an attempt to paint a familiar picture for the structure of the type of Bottom. This was clearly a wrong analogy, because as Ryan showed, unnamed types can never be the subtype of named ones. This was a wrong attempt at simplifying the description of the structure of bottom. Bottom is the conjunction of all types, named and unnamed, and that means it includes the disjunction of all the (permutations of the sets of) fields in the universe. There is no simpler analogy that is correct. So the structural type analogy was a red-herring and introduced noise into my point about bottom being the coinductive representation of the universe.

Now back to the main point about bottom being a coinductive representation of the universe.

There is no disagreement that bottom's type has a disjunction of all the operations in the universe, and no disagreement that bottom is a conjunctive/coinductive type with universal extent (note that is not the same as a universal extent with disjunctive/inductive type, which is Top). The disagreement in this discussion has been whether the instances of bottom dictate its name and semantics. I have argued that since there are no instances of bottom, that its type dictates its name and semantics.

We name Top the Universal type in computer science, because it is an inductive type, so the name applies to the instances. For coinductive types, we can't name the instances, we can only name the concept, because the instances are not composed from initial object (e.g. `extend`ing a type), but rather decomposed from a final object (e.g. decomposing the type of Bottom into all types in the universe).

I went further to explain how in an eager (i.e. inductive) language, there is no way to express an infinite thing inductively, as we normally do for most types in an eager language. And I explained how the duals are the case in a lazy (coinductive) language.

So in my mind, I clearly won the logic w.r.t. to the name of Bottom. Nothing is wrong. And the only correct names are All, Universe, CoUniverse, Bottom, SubOfAll, and perhaps Never is not so severely incorrect as Nothing is.

Now I agree it would help to formalize of all that.

[Ryan Hendrickson]

> We name Top the Universal type in computer science, because it is an
> inductive type, so the name applies to the instances. For coinductive
> types, we can't name the instances, we can only name the concept,
> because the instances are not composed from initial object (e.g.
> `extend`ing a type), but rather decomposed from a final object (e.g.
> decomposing the type of Bottom into all types in the universe).

I think I'm starting to understand your perspective? Ex falso, quod libet <=> from Bottom, the Universe. Since for any type A, the type Bottom => A is trivially inhabited, you can treat a value of type Bottom as any type (in effect, destruct Bottom to that type, the same way you'd destruct an (A, B) into an A or a B). This is why you keep emphasizing that Bottom is a coinductive type and that a value inhabiting Bottom is like the entire universe of possible values--even though this is only the case because there can in fact be no value inhabiting Bottom. Do I basically have it?

> I went further to explain how in an eager (i.e. inductive) language,
> there is no way to express an infinite thing inductively, as we normally
> do for most types in an eager language. And I explained how the duals
> are the case in a lazy (coinductive) language.
>
> So in my mind, I clearly won the logic w.r.t. to the name of Bottom.
> Nothing is wrong. And the only correct names are All, Universe,
> CoUniverse, Bottom, SubOfAll, and perhaps Never is not so severely
> incorrect as Nothing is.

You're still not winning me on this one, although now I think I can mount a counterargument. We've collectively settled on naming types from what you might call a contravariant perspective: types like Any, Either, and Nothing are named after the constraint they place on values that can inhabit them.

def setTop(x: Any) // could take Any value
def setSum(x: Either[A, B]) // could take Either an A or a B
def setProduct(x: Pair[A, B]) // can only take an A and a B
def setBottom(x: Nothing) // could take Nothing--there is no (legal) way to execute this function

Naming Bottom All would be taking the dual perspective--the constraint placed on *you* when provided a value of that type.

def getBottom: Universe // you can treat this value as anything in the Universe (because, of course, you'll never get it)

But our other type names don't work that way:

def getTop: Any // you definitely can't treat this value as Anything you want
def getSum: Either[A, B] // you actually need to handle *both* the A and B cases, not Either of them
def getProduct: Pair[A, B] // you don't need to use A and B together if you don't want to

I can indeed imagine a covariantly-named alternate universe where we've decided on the other convention:

def getTop: Unknown // you can't assume anything about this value
def getSum: Both[A, B] // you should handle this value non-deterministically as A and B
def getProduct: Or[A, B] // you can use the A Or the B (or both)
def getBottom: Universe // you can treat this value as anything in the Universe

I'm not sure if there's anything a priori superior about Any/Nothing over Unknown/Universe, but I would hate to have to try explaining to anyone that a foo(x: Any) can take any argument you want, but a foo(x: Universe) can't be invoked because Universe is named for a type that can be destructed to any other type, which clearly couldn't be represented in our type system. Clearly you disagree, but I think there's an objective argument to be made for consistency. (In particular, I think it's natural--as I suppose I've revealed in my naming scheme above--for the contravariant name for Top/Sum/Product/Bottom to be a synonym of the covariant name for the dual type. Which is just my justification for believing that Universe is roughly synonymous with Any, or at the very least close enough that giving those names to the two most opposite types in the type system is not likely to help anyone's intuition when learning this stuff.)

[Shelby Moore]

>> We name Top the Universal type in computer science, because it is an
>> inductive type, so the name applies to the instances. For coinductive
>> types, we can't name the instances, we can only name the concept,
>> because the instances are not composed from initial object (e.g.
>> `extend`ing a type), but rather decomposed from a final object (e.g.
>> decomposing the type of Bottom into all types in the universe).
>
> I think I'm starting to understand your perspective? Ex falso, quod libet
> <=> from Bottom, the Universe. Since for any type A, the type Bottom => A
> is trivially inhabited, you can treat a value of type Bottom as any type
> (in effect, destruct Bottom to that type, the same way you'd destruct an
> (A, B) into an A or a B).

As you know, Bottom never has a value, and I want to be mathematically
precise.

Your example is more like a Stream read function, which is coinductive
because we input a Stream, and get back a new Stream and a value. For a
Stream, we only know what all of its contents were when we stop
destructing it.

I am saying that the coinductive function for Bottom destructs its type
only and not its nonexistent value. We only know the all the contents of
the type of Bottom, when we stop adding new types to the universe, i.e.
never.

> This is why you keep emphasizing that Bottom is
> a coinductive type and that a value inhabiting Bottom is like the entire
> universe of possible values--even though this is only the case because
> there can in fact be no value inhabiting Bottom. Do I basically have it?

You had the destruct idea of coinduction, but you are applying to a
nonexistent value of bottom.

Whereas I am remaining mathematically precise and applying the coinductive
function to Bottom's type (which exists). So in every instance where we
declare a type at compile-time, we have applied the coinductive function
for Bottom.

I also proved in one my earlier messages in this thread, that the
inductive definition of Universe as constructed from an initial type Top
and adding new types inheritance is equivalent the Axiom of Infinity for
sets, and proved that this is the categorical dual for coinductive model
of bottom I stated above.

So there you have a mathematical proof that the inductive and coinductive
representations of the infinite set both exist and are categorically dual.

I think explained that in an eager evaluation strategy language, the only
way to represent the infinite set is the coinductive one. And dually in a
lazy language (e.g. Haskell), the only way to represent the infinite set
is the inductive one.

In the Curry-Howard correspondence, Bottom corresponds to the a "logical
contradiction" of the fundamental axioms. Well we see that the Axiom of
Infinity is a fundamental contradiction, because when our
frame-of-reference is inductive (i.e. eager) evaluation strategy, then we
can not represent the universe inductively, but we can represent it
coinductively. And dually, for a coinductive (i.e. lazy) evaluation
strategy, then we can not represent the universe coinductively, but we can
represent it inductively.

So therefore, bottom is always the universe, either an inductive or
coinductive representation (and the dual of our frame-of-reference).

>> I went further to explain how in an eager (i.e. inductive) language,
>> there is no way to express an infinite thing inductively, as we
>> normally
>> do for most types in an eager language. And I explained how the duals
>> are the case in a lazy (coinductive) language.
>>
>> So in my mind, I clearly won the logic w.r.t. to the name of Bottom.
>> Nothing is wrong. And the only correct names are All, Universe,
>> CoUniverse, Bottom, SubOfAll, and perhaps Never is not so severely
>> incorrect as Nothing is.
>
> You're still not winning me on this one, although now I think I can mount
> a counterargument. We've collectively settled on naming types from what
> you might call a contravariant perspective: types like Any, Either, and
> Nothing are named after the constraint they place on values that can
> inhabit them.
>
> def setTop(x: Any) // could take Any value
> def setSum(x: Either[A, B]) // could take Either an A or a B
> def setProduct(x: Pair[A, B]) // can only take an A and a B

Agreed, I said this many times already. But I also pointed out that those
types are all inductive types. And thus they have values. And thus we can
name them based on the values that inhabit them.

> def setBottom(x: Nothing) // could take Nothing--there is no (legal) way
> to execute this function

And this where you argument falls apart. And I will make the same point I
have made numerous times already.

We can not name a coinductive type by its values, because it does not have
any values.

And thus all the valid use cases for Bottom, are concerned with
destructing its type and not its nonexistent value.

In an earlier exchange with Rex Kerr, I enumerated some use cases and
explained why they involving the semantics of the coinductive type of
Bottom and the nonexistent value of bottom has no bearing whatsoever on
the semantics.

For example, List[Nothing] is not a list of members with type Nothing. The
fact that it is chosen to be an empty list has no dependence at all on
Bottom being empty. The reason bottom is used in that position, is because
it is the subtype of all types, and thus we can assign an empty list to
any type of list.

I also addressed the use case for nonterminating functions:

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

> Naming Bottom All would be taking the dual perspective--the constraint
> placed on *you* when provided a value of that type.

I argued against `All` for bottom, because it is ambiguous with Top.

> def getBottom: Universe // you can treat this value as anything in the
> Universe (because, of course, you'll never get it)

Great. You intuitively got one of the semantics of returning universe from
a nonterminating function.

I think returning the universe is also saying that if this function
returns (via exception), then it will be returning to any function (type)
in the universe. I have not formalized that intuition mathematically yet.

> But our other type names don't work that way:
>
> def getTop: Any // you definitely can't treat this value as Anything you
> want
> def getSum: Either[A, B] // you actually need to handle *both* the A and
> B cases, not Either of them
> def getProduct: Pair[A, B] // you don't need to use A and B together if
> you don't want to

Because they are not coinductive types.

> I can indeed imagine a covariantly-named alternate universe where we've
> decided on the other convention:

Yeah it is Haskell or any lazy evaluation strategy language.

> def getTop: Unknown // you can't assume anything about this value
> def getSum: Both[A, B] // you should handle this value
> non-deterministically as A and B
> def getProduct: Or[A, B] // you can use the A Or the B (or both)
> def getBottom: Universe // you can treat this value as anything in the
> Universe
>
> I'm not sure if there's anything a priori superior about Any/Nothing over
> Unknown/Universe,

Granted for Unknown vs. Any is mostly subjective choice. There are tradeoffs.

For Nothing vs. Universe, the semantics are broken with Nothing, but not
with Universe.

> but I would hate to have to try explaining to anyone
> that a foo(x: Any) can take any argument you want, but a foo(x: Universe)
> can't be invoked

Yeah for the same reason you can't return the *whole* universe:

Definition:
u·ni·verse
Noun:
"All existing matter and space considered as a whole"

I think you are conflating with the well-known name for Top in computer
science:

Universal type

u·ni·ver·sal
Adjective:
"Of, affecting, or done by all things in the world"

I know people conflate definitions, but is that the fault of the person
who is trying to use the english language correctly as I am here?

> because Universe is named for a type that can be
> destructed to any other type, which clearly couldn't be represented in our
> type system.

To remind them of the coinductive nature of the type, I suggested CoUniverse.

I am also okay with SubOfAll.

I think making your argument based on non use cases is weak. Please argue
the use cases of bottom instead.

> Clearly you disagree, but I think there's an objective
> argument to be made for consistency.

Yeah, and that is don't conflate the naming for inductive and coinductive
types.

You thought you were being consistent, because you were treating bottom as
an inductive type, even when it is clear from its use cases that it is not
and that the semantics are broken by doing so.

> (In particular, I think it's
> natural--as I suppose I've revealed in my naming scheme above--for the
> contravariant name for Top/Sum/Product/Bottom to be a synonym of the
> covariant name for the dual type. Which is just my justification for
> believing that Universe is roughly synonymous with Any,

Yeah because you are conflating inductive and coinductive, you are
conflating definitions of Universe (the whole thing) and Universal (the
things in the whole), and because you did not I guess look at my proof
w.r.t. to the Axiom of Infinity for sets.

It is very clear that the inductive representation of the infinite set can
not be represented in an eager language, only in a lazy language like
Haskell can it. Instead in an eager language we have a top type that is
inductive. Whereas in Haskell, the bottom is inductive and the top is
coinductive.

> or at the very
> least close enough that giving those names to the two most opposite types
> in the type system is not likely to help anyone's intuition when learning
> this stuff.)

It is likely to help greatly, because then the names will agree with the
semantics of the use cases.

Apologies I did not proof read this before sending this. I don't have the
patience. Any typos will not be corrected with a followup.

[Ryan Hendrickson]

Hmm. Seems my declaration of understanding was premature. I think I shall revert back to lurking on this thread, but thank you for another attempt at explaining and I'm sorry for retreading what I see now is old ground.

[Rex Kerr]

On Mon, Oct 8, 2012 at 8:24 PM, Shelby Moore <she...@coolpage.com> wrote:

We can not name a coinductive type by its values, because it does not have
any values.

Er, "None", "Nothing", "Zilch", "Nada", "Empty", "Uninhabited", "Absent", ....

We name things by the fact that there are none of them all the time.

Maybe you find this displeasing.  Some don't.  So this is a bike-shed style argument at this point.

For example, List[Nothing] is not a list of members with type Nothing. The
fact that it is chosen to be an empty list has no dependence at all on
Bottom being empty.

It has plenty to do with that--otherwise your so-called empty list might start out with a spurious element!  You need both that property and the subtype-of-everything property in order to form Nil.  List[Nothing] is the perfect fit because the type alone guarantees both properties (and is highly suggestive of the it-is-empty property but not the subtype-of-everything property).

  --Rex

[Shelby Moore]

> Hmm. Seems my declaration of understanding was premature. I think I shall
> revert back to lurking on this thread, but thank you for another attempt
> at explaining and I'm sorry for retreading what I see now is old ground.

Obviously I am not lucid enough, so that is my fault, not yours.

And your feedback is helping me understand where my
explanation/understanding is not lucid. I wish I was more clairvoyant, so
the process was less verbose and arduous.

On Tuesday, October 9, 2012 8:24:39 AM UTC+8, Shelby wrote:
[...]

>> but I would hate to have to try explaining to anyone
>> that a foo(x: Any) can take any argument you want, but a
>> foo(x: Universe) can't be invoked
>

> But it is for the same reason you can't return the *whole* universe:

>
> Definition:
> u·ni·verse
> Noun:
> "All existing matter and space considered as a whole"
>
> I think you are conflating with the well-known name for Top in
> computer science:
>
> Universal type
>
> u·ni·ver·sal
> Adjective:
> "Of, affecting, or done by all things in the world"

[...]

>> because Universe is named for a type that can be destructed
>> to any other type, which clearly couldn't be represented
>> in our type system.

[...]

> I think making your argument based on non use cases is weak.
> Please argue the use cases of bottom instead.

More I think about it, that non use cases also favor Universe over Nothing.

A function that inputs an instance of Nothing, can only mean that it is
inputting a value of the null or the empty set. Because we rule out other
possibilities, due the fact that we know from the semantics of our
language, that we can never input a non-instance.

Whereas, inputting the instance of the Universe can only mean that the
construction is impossible. There is no other possible meaning.

The problem with the definition of Nothing is that it is not unambiguous
in that non use case. Whereas, the definition of Universe is unambiguous.

If the user conflates Universal and Universe, i.e. has muddled thinking
about an instance of something in the universe, versus an instance of the
whole universe, well I say they need to be more precise with definitions.

Computer programming is the very precise application of logic. Anything
else is a bug.

Why proliferate chaos by being ambiguous with our terms from the start?

============================

> As you know, Bottom never has a value, and I want to be mathematically
> precise.
>
> Your example is more like a Stream read function, which is coinductive
> because we input a Stream, and get back a new Stream and a value. For a
> Stream, we only know what all of its contents were when we stop
> destructing it.

Coinductive types are very non-intuitive for us, because the structure of
the final object is not known until we stop destructing.

We are accustomed to saying "constructor" creates/initializes something,
and "destructor" destroys/finalizes it. With a coinductive type, those
roles are transposed.

The Stream is an example that we are destructing (decomposing) the Stream
*instance*, until we finally construct it. At the end of the program (or
final use of that Stream instance), we know what its contents are/were, as
we have read all of the contents.

So a Stream example is useful for illuminating the duality/distinction
between an inductive and coinductive type.

> The coinductive function for Bottom destructs its type only and not its

> nonexistent value. We only know the all the contents of the type of
> Bottom, when we stop adding new types to the universe, i.e.
> never.

A Stream has a coalgrebra (i.e. the function that destructs/decomposes it)
that operates on the values of the Stream *instance*. So the coinduction
domain is over *instances*.

Bottom has a coalgrebra that operates on the types of the Bottom *type*.
So the coinduction domain is over *types*.

An example of an *instance* that is constructed inductively is the
immutable collection. Its initial object is the empty set of instances,
and then we can add (but not remove because immutable) instances.

An example of a *type* that is constructed inductively is the natural
numbers. The initial object is the type for 0, and the succeeding function
(the algebra) creates the type for the next number. Note that an instance
of the natural numbers will have only one of its member types.

http://www.utdallas.edu/~gupta/courses/apl/lambda.pdf#page=4 (see sec 2
Arithmetic)

Another example of a *type* that is constructed inductively is Top (i.e.
Any in Scala). The initial object is the type for empty set of types or
nothing. The algebra is that every time we declare a new type in the
universe of programs, it's added to the disjunction with Top. Note again
that aninstance of Top will have only one of its member types.

I showed that the inductive representation of the infinite set is given by
the algebra in the Axiom of Infinity:

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

Shelby wrote:
"successor function, x union {x} elemof I, that proceeds from any
instantiable initial object x towards the infinite set"

Note that is an algebra that has its domain over *instances* not types.
Thus clearly we can never instantiate something that is infinite, at least
not in an inductive/eager evaluation strategy language, such as Scala. We
can actually instantiate an infinite algebra is a lazy evaluation strategy
language, such as Haskell (because the infinite recursion will never be
evaluated).

So with the above examples, I hope it is lucid that in an inductive
(eager) language, we can have *types* that are composed of infinite
members, but we can't have instances that have infinite values. In a
coinductive (lazy) language, we get the dual of all the concepts.

So in order to express the infinite set in an inductive language, we have
two types, Top and Bottom. Top is the *inductive* universAL type, meaning
we can *construct* one type from the infinite set of types. Bottom is the
*coinductive* universE type, meaning we can *decompose/destruct* all types
from the infinite set of types. The significance of Top is only one type
at a time, and Bottom is all types simultaneously (in the coinductive
sense of decomposition).

Top's inductive algebra is we add a new type to Top's type every time we
declare a new type in the universe of programs. Bottom's coinductive
coalgebra is that we add a new type to Bottom's type every time we declare
a new type in the universe of programs.

At my above linked post, I had attempted a proof of the categorical
duality of the inductive universe with Axiom of Infinity algebra, and the
coinductive universe given by Bottom.

[Shelby Moore]

On Tuesday, October 9, 2012 11:48:19 AM UTC+8, Rex Kerr wrote:
>> We can not name a coinductive type by its values, because it does not
>> have any values.
>
> Er, "None", "Nothing", "Zilch", "Nada", "Empty", "Uninhabited", "Absent",
> ....
>
> We name things by the fact that there are none of them all the time.

It is not a subjective argument to say that a type should be named to
match its semantics for all of its use cases.

I already explained/claimed that neither Nothing (nor your alternatives
above) match the semantics in any of the use cases for bottom:

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

Implied in your logic is that we can name a type based on the *instances*
that inhabit it, even if the semantics of ALL the cases where we use the
type are based on the structure of the *types* that inhabit it.

Imagine if we applied the converse, and named all types based on their
type structure and not its *instances*, thus we would rename Top
"Disjoint", "Disjunction", or "Universal", etc..

> Maybe you find this displeasing. Some don't. So this is a bike-shed
> style argument at this point.

Some people like to create logical inconsistencies, but that doesn't mean
I should agree with it. If someone shows me it is a subjective debate,
then I will concede.

> For example, List[Nothing] is not a list of members with type Nothing. The
>> fact that it is chosen to be an empty list has no dependence at all on
>> Bottom being empty.
>
> It has plenty to do with that--otherwise your so-called empty list might
> start out with a spurious element!

The semantics of List[T] is that T is the member type. T has no way of
specifying to List[T] that members of T should not be instantiated. This
is why Scala's implementation of List[T] can throw an exception, because
it necessarily allows `head` to be null. The more correct (compile-time
safe) and alternative way of implementing List[T] is to make the Head[T] a
subtype of List[T].

Thus List[Bottom] only has the semantics that it is a subtype of any
List[T]. W.r.t. to the semantics of List[T] (the immediate semantics of
concern, not the derivative semantics), Bottom is not being used to say
anything about the existence of member instances, rather it is only to
enforce the type.

Now it follows that if the member type is bottom, then the list can't have
any elements. But that is not the immediate logic involved, because
List[T] doesn't have any elements either (or it has null elements which is
the wrong way of implementing it, because it allows runtime errors instead
of catching them at compile-time).

I think you and Ryan have both made the point that why should we name
things based on complex secondary reasoning. So I am using your point to
make my point.

> You need both that property and the
> subtype-of-everything property in order to form Nil.

Yeah but Nil and List[Nothing] are not the same type and have different
semantics, as I explained above.

When you get to the end of Nil's declaration, then you know Nil doesn't
have instances. But if you just have List[Nothing], there is no immediate
specification that it is empty. You can reason it out as a secondary logic
process. I think we all agree to choose names which are direct to the
point of the immediate scope of their use case.

> List[Nothing] is the
> perfect fit because the type alone guarantees both properties

Nothing says nothing about being a subtype of everything, which is the
immediate semantics needed for List[Nothing].

The fact that Nil must necessarily be empty, is a secondary realization.

> (and is
> highly suggestive of the it-is-empty property but not the
> subtype-of-everything property).

Great. So you admit it does not address the immediate semantics, only the
derivative secondary semantics.

So are we disagreeing?

[Rex Kerr]

On Tue, Oct 9, 2012 at 9:23 AM, Shelby Moore <she...@coolpage.com> wrote:

On Tuesday, October 9, 2012 11:48:19 AM UTC+8, Rex Kerr wrote:
>> We can not name a coinductive type by its values, because it does not
>> have any values.
>
> Er, "None", "Nothing", "Zilch", "Nada", "Empty", "Uninhabited", "Absent",
> ....
>
> We name things by the fact that there are none of them all the time.

It is not a subjective argument to say that a type should be named to
match its semantics for all of its use cases.

Yes it is, especially since that's not what is done in many other cases and, as you admit, people like to build up elements inductively.  You can't with CoUniverse, but that doesn't mean that you should match the semantics instead of matching the contents.  If it was true that from the name alone _all semantics were intuitively clear_ then you'd have an objective argument.  But this isn't true for pretty much _any_ of the types in Scala or any other language; you have to learn details of the type system etc. etc..  If we could assume people had a solid grounding in type theory, then we'd just label Top Top and Bottom Bottom (assuming that those are the universally accepted names) and be done with it, but we can't.

So it's subjective.  You prefer that we name things after when the contents start growing less informative.  I don't; I prefer to maintain the "the name of the type tells you what things you can find which are that type" consistency.  I don't find either particularly hard to reason about, but the latter better matches what concerns I have most of the time.

For example, a little while ago I wrote an exception handling class ("Tri") in response to Bruce Eckel's wish that there was something with both the properties of Try and of Either (i.e. your failure case can either be something typed to your specification or a Throwable).  After application of various methods, one of the alternatives will become uninhabited.  So, I thought: "well, there's obviously nothing in the Bad branch any more, let's make the type Nothing" and then thought through the issues with it actually being the Bottom type and made sure it was okay (it's a tradeoff, but I decided that it was better that way).  The type name was highly suggestive of what to do in that case, which would not have been true if the type were named for its has-all-interfaces property.

It's not that I don't want types to be as suggestive as possible of their use cases, all else being equal.  The issue is that you cannot suggest all use cases anyway, and knowing which way the suggestion goes (are you suggesting things about the elements of that type, or about the properties of the type itself?) is important so consistency is a good thing, all else being equal (which it also is not).  So there are tradeoffs, which different people may prefer to resolve in different ways.

The only way to turn this from a subjective to an objective argument is to do some sort of study--train people both ways, for example, and rate various types of mistakes and show a clear advantage for one over the other.  Otherwise it really is just personal preference.

I don't have any more to say about this; if I haven't made myself clear yet, I very much doubt I'll be able to do so in the amount of time I have free to try, and if you still disagree that it is a subjective rather than an objective choice, again, I don't know what else I could say that might be convincing where this is not (and as you've now made the same point three or so times w.r.t. naming, I suspect that I have a pretty clear idea of what your point is but still don't agree).

  --Rex

P.S. I agree that it takes some reasoning to realize that List[Nothing] has no elements, but I disagree that this reasoning is as bad as List[Universe], where you first have to realize that it is impossible, and then decide that you meant CoUniverse, and then remember that CoUniverse refers to Bottom, which is uninhabited in an eager language, and then reason that List[Universe] must be uninhabited.  Going for subclassing, List[Universe] still doesn't tell you that Universe is the bottom type, you still have to do the Universe -> CoUniverse -> "Oh, that's Bottom" reasoning.  (SubOfAll is good this way, I agree.)  But this side of the reasoning is just a lot easier, so you need less help--or at least I do.  Others may disagree, which again, highlights the subjectivity involved.

[Ryan Hendrickson]

Ah, tempted into delurking again. :-) I still can't follow your Axiom of Infinity argument but I think it's because I'm getting tripped up on the preliminaries.

> An example of an *instance* that is constructed inductively is the
> immutable collection. Its initial object is the empty set of instances,
> and then we can add (but not remove because immutable) instances.

In other words, the functor over types T => Either[Nil, (A, T)] is the signature of an initial algebra over List[A], and that algebra defines the induction for creating lists from either Nil or a head and tail. I'm comfortable with this idea.

> An example of a *type* that is constructed inductively is the natural
> numbers. The initial object is the type for 0, and the succeeding function
> (the algebra) creates the type for the next number. Note that an instance
> of the natural numbers will have only one of its member types.
>
> http://www.utdallas.edu/~gupta/courses/apl/lambda.pdf#page=4 (see sec 2
> Arithmetic)

This is interesting. I'd like to drop down into the Scala type system, because I'm fairly confident that I understand it whereas I'm not familiar with the framework you're using.

So encoding the natural numbers at the type level looks something like this in Scala:

sealed trait Nat
trait Zero extends Nat
trait Succ[N <: Nat] extends Nat

Is Nat, the literal named type in the type system, the inductively-constructed type to which you refer? Or are you talking about a *kind* (or a 2-type or something--not sure what the canonical term is for such a beast) that Zero, Succ[Zero], Succ[Succ[Zero]]... all inhabit (in some non-Scala kind system that is richer than the simply typed lambda calculus)? Or is there something else you could be talking about?

What do you mean when you say that an instance of the natural numbers will have only one of its member types? Are you saying that a value instance inhabiting the type Nat can only inhabit one of the types Zero, Succ[Zero], Succ[Succ[Zero]]...?

I assume a sharp distinction exists between the ‘inhabits’ relations (one between values and types, one between types and kinds) and the ‘is subtype of’ relation (between types only) (and I don't know what relation to which you refer when you talk about members of types; it seems like a conflation of inhabits and subtype but I could be missing something). The relationship between Zero, Succ[Zero], Succ[Succ[Zero]]... and Nat seems to be the ‘is subtype of’ relation; in particular, nothing new is added to Nat when someone uses a new type in their program of the form Succ[...Succ[Zero]...]. Nat does not need to be constructed, only declared, and then other types can be declared to be in relation to it. By contrast, types like Succ[...Succ[Zero]...] are constructed, which makes me think that you are actually talking about an inductive kind in a richer kind system. Am I getting closer?

> Another example of a *type* that is constructed inductively is Top (i.e.
> Any in Scala). The initial object is the type for empty set of types or
> nothing. The algebra is that every time we declare a new type in the
> universe of programs, it's added to the disjunction with Top. Note again
> that aninstance of Top will have only one of its member types.

This statement has me even more confused for basically the same reasons as above. What is ‘the type for empty set of types’? Surely a type-of-types (kind, 2-type) is not the same sort of thing as a type like Top? What does it mean for an instance of Top (which I would think means any value whatsoever) to have only one of its member types (surely instances can inhabit many types, and if by member you mean ‘is subtype of’ then every type is a member of Top)? And why does it make more sense to think of Top as being ‘constructed’, as opposed to declared and then when other types are declared, the ‘is subtype of’ relation is extended in a way that is always compatible with Top being Top?

[Shelby Moore]

>> It is not a subjective argument to say that a type should be named to
>> match its semantics for all of its use cases.
>
> Yes it is, especially since that's not what is done in many other cases
> and, as you admit, people like to build up elements inductively.

So logically this reduces to that you are saying there is no objectivity
at all for bottom, it is merely a popularity contest and imprecise and
ambiguous usage is preferred if it is more popular.

[...]

> If it was true that from the name alone
> _all semantics were intuitively clear_ then you'd have an objective
> argument.

So you punted on the only possible objective priority:

>> Nothing says nothing about being a subtype of everything,
>> which is the immediate semantics needed for List[Nothing].
>>
>> The fact that Nil must necessarily be empty, is a secondary realization.

And you have required secondary reasoning to be intuitive, which is
impossible because secondary reasoning will never be consistently about
bottom's effect, so thus you choose subjectivity and ambibuity.

> But this isn't true for pretty much _any_ of the types in Scala
> or any other language; you have to learn details of the type system etc.

Yeah that is why I am saying the the only form of possible precision and
lack of ambiguity is to make sure each local type sub-expression is
definitionally correct.

> etc.. If we could assume people had a solid grounding in type theory,
> then
> we'd just label Top Top and Bottom Bottom (assuming that those are the
> universally accepted names) and be done with it, but we can't.

I don't think Nothing helps at all. I speak from my own experience when I
first saw List[Nothing]. I was trying to figure out how the List[Null] was
a subtype of List[T] for all T. And why Nothing was chosen as a name for
null. Because logically I was studying the local relationship, because
that is the way we analyze code in precise detail, is to work from the
inner expressions outwards.

And at that time, I knew nothing about bottom types. I was merely learning
and analyzing the way covariant type parameters behave.

Rather I think you are thinking that people jump immediately to
memorization or secondary reasoning, "ah never mind what the covariant
relationship is, just sort of wink and imagine that if we put Nothing in a
list then it must be empty".

I don't believe in the programming by guesses and misses approach, even
though I've read this is the way most people try to program, before the
flunk out.

But you might be correct. The market for Scala might be those types of
people:

http://pages.citebite.com/h6e0p5y2tlpw

(ok I lost my logic and was just ranting a bit, hehe)

> So it's subjective. You prefer that we name things after when the
> contents
> start growing less informative. I don't; I prefer to maintain the "the
> name of the type tells you what things you can find which are that type"
> consistency. I don't find either particularly hard to reason about, but
> the latter better matches what concerns I have most of the time.

I understand you always want to name a type based on its values, because
you feel this is more consistent, in spite of my examples showing that for
the immediate local reasoning, it is not more consistent.

> For example, a little while ago I wrote an exception handling class
> ("Tri")
> in response to Bruce Eckel's wish that there was something with both the
> properties of Try and of Either (i.e. your failure case can either be
> something typed to your specification or a Throwable). After application
> of various methods, one of the alternatives will become uninhabited. So,
> I
> thought: "well, there's obviously nothing in the Bad branch any more,
> let's
> make the type Nothing" and then thought through the issues with it
> actually
> being the Bottom type and made sure it was okay (it's a tradeoff, but I
> decided that it was better that way). The type name was highly suggestive
> of what to do in that case, which would not have been true if the type
> were
> named for its has-all-interfaces property.

I won't be able to agree that is a valid counter claim, until I see the
code. Devil is in the details, I can't just take your word for it that
your usage had the correct local semantics of Nothing.

> It's not that I don't want types to be as suggestive as possible of their
> use cases, all else being equal. The issue is that you cannot suggest all
> use cases anyway,

I assert that the local reasoning for bottom will never be about its
values. Never. I want to see code for a counter claim.

I am nearly certain of that, because you can't ever assign a Nothing or
input it as a value.

The local reasoning will always be about the coinductive type of bottom
(i.e. that it is the subtype of all types).

[...]

> The only way to turn this from a subjective to an objective argument is to
> do some sort of study--train people both ways, for example, and rate
> various types of mistakes and show a clear advantage for one over the
> other. Otherwise it really is just personal preference.

Disagree. If we don't have an objective math, then a user study won't help
us (because the secondary reasoning use cases are ambiguous).

The only objective math I can think of, is the local reasoning must be
definitionally correct.

> I don't have any more to say about this; if I haven't made myself clear
> yet, I very much doubt I'll be able to do so in the amount of time I have
> free to try,

Agreed I don't want to go on and on either.

I think the final thing in my mind is if you have counter-claim for usage
case where local reasoning is not about the type of bottom.

But I think you don't want to agree to that objective rule any way. I
suppose because you find Nothing meets some secondary semantics better
from your perspective. You could use a type alias.

I think the consistency of local reasoning (the only thing that can be
consistent) should objectively be the default.

[...]

> P.S. I agree that it takes some reasoning to realize that List[Nothing]
> has
> no elements, but I disagree that this reasoning is as bad as
> List[Universe], where you first have to realize that it is impossible,

The secondary reasoning may not be better for Universe, but the local
reasoning about Universe's type is better. And that the only objective
priority I can think of. Secondary reasoning will be different in
different use cases, so we end up with ambiguity any way.

[...]

[Rex Kerr]

On Tue, Oct 9, 2012 at 2:11 PM, Shelby Moore <she...@coolpage.com> wrote:

> For example, a little while ago I wrote an exception handling class
> ("Tri")
> in response to Bruce Eckel's wish that there was something with both the
> properties of Try and of Either (i.e. your failure case can either be
> something typed to your specification or a Throwable).  After application
> of various methods, one of the alternatives will become uninhabited.  So,
> I
> thought: "well, there's obviously nothing in the Bad branch any more,
> let's
> make the type Nothing" and then thought through the issues with it
> actually
> being the Bottom type and made sure it was okay (it's a tradeoff, but I
> decided that it was better that way).  The type name was highly suggestive
> of what to do in that case, which would not have been true if the type
> were
> named for its has-all-interfaces property.

I won't be able to agree that is a valid counter claim, until I see the
code. Devil is in the details, I can't just take your word for it that
your usage had the correct local semantics of Nothing.

Well, it's hard to resist requests for code, since I agree that code's the important thing.

  // V is the type of the value that you want (in Good)
  // P is the type of the problem-reporting object you may generate (in Bad)
  // Throwable is also possible (it's Ugly)

  sealed trait Tri[+V,+P] {
    // ...
    def acceptAll[U >: V](f: P => U): Tri[U,Nothing] = this match {
      case Bad(p) => try { Good(f(p)) } catch { case t if Recoverable(t) => Ugly[U,Nothing](t) }
      case x => x.asInstanceOf[Tri[U,Nothing]]
    }
    // ...
  }
  final case class Good[V,P](value: V) extends Tri[V,P] { /* ... */ }
  final case class Bad[V,P](problem: P) extends Tri[V,P] { /* ... */ }
  final case class Ugly[V,P](thrown: Throwable) extends Tri[V,P] { /* ... */ }

"acceptAll" turns any bad values into good ones; after this you are certain there is nothing left in the Bad category.  Hence, Nothing.  Note covariance in P, so this is also the correct subtyping relationship.

  --Rex

[Alec Zorab]

As far as naming goes, I am reminded of Simon Peyton-Jones' observation that calling monads "warm fluffy things" might have made a lot of lives a lot easier.

Sometimes formal correctness becomes secondary to easing broader understanding.

[Shelby]

On Wednesday, October 10, 2012 2:27:34 AM UTC+8, Rex Kerr wrote: 

  // V is the type of the value that you want (in Good)
  // P is the type of the problem-reporting object you may generate (in Bad)
  // Throwable is also possible (it's Ugly)

  sealed trait Tri[+V,+P] {
    // ...
    def acceptAll[U >: V](f: P => U): Tri[U,Nothing] = this match {
      case Bad(p) => try { Good(f(p)) } catch { case t if Recoverable(t) => Ugly[U,Nothing](t) }
      case x => x.asInstanceOf[Tri[U,Nothing]]
    }
    // ...
  }
  final case class Good[V,P](value: V) extends Tri[V,P] { /* ... */ }
  final case class Bad[V,P](problem: P) extends Tri[V,P] { /* ... */ }
  final case class Ugly[V,P](thrown: Throwable) extends Tri[V,P] { /* ... */ }

"acceptAll" turns any bad values into good ones; after this you are certain there is nothing left in the Bad category.  Hence, Nothing.  Note covariance in P, so this is also the correct subtyping relationship.

It is non-intuitive to declare a function that inputs Nothing, i.e. Tri[U,Nothing].acceptAll, because the only way to call it to encourage a downcasting runtime error.

def test( f: Nothing => Int ) = f(0.asInstanceOf[Nothing])

test( (x) => x )

java.lang.ClassCastException: java.lang.Integer cannot be cast to scala.runtime.Nothing$

If you've thrown away P, why return a Tri[U,Nothing] and not a U?

So I see you are trying to think about Nothing in terms of its value, but it is getting you into trouble in your design.

I think this supports my argument even more forcefully. The name Nothing is encouraging you to deviate from using it correctly only in typing relationships. You are apparently trying to shoehorn it into a role for which it isn't appropriate and leads to unsoundness in the design of the API.

[Rex Kerr]

On Tue, Oct 9, 2012 at 4:22 PM, Shelby <she...@coolpage.com> wrote:

On Wednesday, October 10, 2012 2:27:34 AM UTC+8, Rex Kerr wrote: 

  // V is the type of the value that you want (in Good)
  // P is the type of the problem-reporting object you may generate (in Bad)
  // Throwable is also possible (it's Ugly)

  sealed trait Tri[+V,+P] {
    // ...
    def acceptAll[U >: V](f: P => U): Tri[U,Nothing] = this match {
      case Bad(p) => try { Good(f(p)) } catch { case t if Recoverable(t) => Ugly[U,Nothing](t) }
      case x => x.asInstanceOf[Tri[U,Nothing]]
    }
    // ...
  }
  final case class Good[V,P](value: V) extends Tri[V,P] { /* ... */ }
  final case class Bad[V,P](problem: P) extends Tri[V,P] { /* ... */ }
  final case class Ugly[V,P](thrown: Throwable) extends Tri[V,P] { /* ... */ }

"acceptAll" turns any bad values into good ones; after this you are certain there is nothing left in the Bad category.  Hence, Nothing.  Note covariance in P, so this is also the correct subtyping relationship.

It is non-intuitive to declare a function that inputs Nothing, i.e. Tri[U,Nothing].acceptAll, because the only way to call it to encourage a downcasting runtime error.

It outputs nothing as a type parameter.  If you try to call twice in a row, then you will indeed need to supply f: Nothing => U, which should be a sign that what you're doing is not a good idea.
 

def test( f: Nothing => Int ) = f(0.asInstanceOf[Nothing])

0 is not Nothing, it's zero (the identity element for +).  That this blows up in your face should be no more surprising than any 0.asInstanceOf[String] or any other nonsensical cast blowing up in your face.  ("Wait, why didn't it give me the empty string?!?!")
 

If you've thrown away P, why return a Tri[U,Nothing] and not a U?

Because it might be a Throwable instead of a U.  The code says so, even in this heavily abridged version.
 

So I see you are trying to think about Nothing in terms of its value, but it is getting you into trouble in your design.

I don't think you've understood the design yet, so I don't think you're in a position to conclude that.

Also, you can of course make this discussion tautologically resolve in your favor by firmly misinterpreting any type declaration of "Nothing" and doing something nonsensical, and then saying that since you did something nonsensical the design is broken.  Hopefully you see the logical flaw in that approach.  You have come perilously close already with casting zero.

  --Rex

[Shelby]

On Wednesday, October 10, 2012 1:13:58 AM UTC+8, Ryan Hendrickson wrote:

Is Nat, the literal named type in the type system, the inductively-constructed type to which you refer? Or are you talking about a *kind* (or a 2-type or something--not sure what the canonical term is for such a beast) that Zero, Succ[Zero], Succ[Succ[Zero]]... all inhabit (in some non-Scala kind system that is richer than the simply typed lambda calculus)? Or is there something else you could be talking about?

Looks like you got it. 

0 = Zero

1 = Succ[Zero]

2 = Succ[Succ[Zero]]

Then we have to definition the minus and other operators in terms of those types.

Kinds has nothing to do with what I was talking about.

 

What do you mean when you say that an instance of the natural numbers will have only one of its member types?

val x: Nat will not contain all the infinite numbers. It will only contain one of them at a time.

>> Another example of a *type* that is constructed inductively is Top (i.e.
>> Any in Scala). The initial object is the type for empty set of types or
>> nothing. The algebra is that every time we declare a new type in the
>> universe of programs, it's added to the disjunction with Top. Note again

>> that an instance of Top will have only one of its member types.

>
> This statement has me even more confused for basically the same reasons as above.

> What is ‘the type for empty set of types’?

In the context of Top, it would be the empty disjunction. I don't think it can be declared in Scala?

(obviously Top is a built-in type, so we can not entirely emulate it)

> Surely a type-of-types (kind, 2-type) is not the same sort of thing as a type like Top?

Afaics, don't ponder the use of a Succ[_] kind to represent the natural numbers as having any bearing on what I was talking about. It just so happens that is the way you represented the successor function (the inductive algebra). But I think you could also do it with functions, as the article I linked showed.

> What does it mean for an instance of Top (which I would think means any value whatsoever) to have

> only one of its member types (surely instances can inhabit many types, and if by member you mean

> ‘is subtype of’ then every type is a member of Top)?

Top is constructed inductively because it is given by an inductive logical relation-- the disjunction of all declared types. So everytime we declare a type, we are adding another type, i.e. conceptually equivalent to calling the inductive algebra that takes the prior disjunction and returning the new disjunction with another type in it.

You can't really write down Top with Scala code. It is a conceptual operation. But you could write down the code for the successor function.

> And why does it make more sense to think of Top as being ‘constructed’, as opposed to declared

It makes sense to think of it as both.

The ML language has a complete proof of its entire type system. And this proof relies on showing the inductive algebra for each built-in type.

[Shelby]

On Wednesday, October 10, 2012 4:46:48 AM UTC+8, Shelby wrote:

The ML language has a complete proof of its entire type system. And this proof relies on showing the inductive algebra for each built-in type.

Apologies double-post.

See page 16:

http://www.cs.cmu.edu/~rwh/plbook/book.pdf

[Shelby]

On Wednesday, October 10, 2012 4:38:52 AM UTC+8, Rex Kerr wrote:

On Tue, Oct 9, 2012 at 4:22 PM, Shelby <she...@coolpage.com> wrote:

On Wednesday, October 10, 2012 2:27:34 AM UTC+8, Rex Kerr wrote: 

  // V is the type of the value that you want (in Good)
  // P is the type of the problem-reporting object you may generate (in Bad)
  // Throwable is also possible (it's Ugly)

  sealed trait Tri[+V,+P] {
    // ...
    def acceptAll[U >: V](f: P => U): Tri[U,Nothing] = this match {
      case Bad(p) => try { Good(f(p)) } catch { case t if Recoverable(t) => Ugly[U,Nothing](t) }
      case x => x.asInstanceOf[Tri[U,Nothing]]
    }
    // ...
  }
  final case class Good[V,P](value: V) extends Tri[V,P] { /* ... */ }
  final case class Bad[V,P](problem: P) extends Tri[V,P] { /* ... */ }
  final case class Ugly[V,P](thrown: Throwable) extends Tri[V,P] { /* ... */ }

"acceptAll" turns any bad values into good ones; after this you are certain there is nothing left in the Bad category.  Hence, Nothing.  Note covariance in P, so this is also the correct subtyping relationship.

It is non-intuitive to declare a function that inputs Nothing, i.e. Tri[U,Nothing].acceptAll, because the only way to call it to encourage a downcasting runtime error.

It outputs nothing as a type parameter.  If you try to call twice in a row, then you will indeed need to supply f: Nothing => U, which should be a sign that what you're doing is not a good idea.
 

def test( f: Nothing => Int ) = f(0.asInstanceOf[Nothing])

0 is not Nothing, it's zero (the identity element for +).  That this blows up in your face should be no more surprising than any 0.asInstanceOf[String] or any other nonsensical cast blowing up in your face.  ("Wait, why didn't it give me the empty string?!?!")

My point was that you shouldn't be instantiating a Tri[U,Nothing], because by doing so, you've created a function that does not make any sense. And the only way to call that function is to create a run-time error.

 

 

If you've thrown away P, why return a Tri[U,Nothing] and not a U?

Because it might be a Throwable instead of a U.  The code says so, even in this heavily abridged version.

So why not return Either[U,Throwable], so as to avoid that unsound function that inputs Nothing?

 

 

So I see you are trying to think about Nothing in terms of its value, but it is getting you into trouble in your design.

I don't think you've understood the design yet, so I don't think you're in a position to conclude that.

That is true, I am just looking at the soundness of the design, and not what it is doing.

But I think that is sufficient to conclude that returning Tri[U,Nothing] is not necessary, when you can return Either[U,Throwable].

 

Also, you can of course make this discussion tautologically resolve in your favor by firmly misinterpreting any type declaration of "Nothing" and doing something nonsensical,

Afaics, a function that inputs Nothing is nonsensical. The semantics of the language never allows you to call such a function, so why would create one?

[Rex Kerr]

On Tue, Oct 9, 2012 at 5:19 PM, Shelby <she...@coolpage.com> wrote:

My point was that you shouldn't be instantiating a Tri[U,Nothing], because by doing so, you've created a function that does not make any sense. And the only way to call that function is to create a run-time error.

 

Afaics, a function that inputs Nothing is nonsensical. The semantics of the language never allows you to call such a function, so why would create one?

I create a method that requires a function that cannot be called.  I do this for the same reason that I create a method that requires a value that cannot exist (e.g. a value of type Nothing): consistency of interface with a lack of meaningless boilerplate.

This is done all over the place in the Scala library: Nil.head, None.get, Vector.empty(0), Seq.empty.map((n: Nothing) => "uhoh").

Unless you do something silly like try to cast something to a type it is not, it's all perfectly typesafe inasmuch as anything is given that the arity of collections is not in general part of the type information.  Just because it's typed as a List[Int] doesn't mean it actually has anything in it; you only know that it _might_ have an int.  List[Nothing] surely does not have anything in it, because nothing is a Nothing. Option[String] might not have a string in it.
 

 

 

If you've thrown away P, why return a Tri[U,Nothing] and not a U?

Because it might be a Throwable instead of a U.  The code says so, even in this heavily abridged version.

So why not return Either[U,Throwable], so as to avoid that unsound function that inputs Nothing?

This is harder to tell from the source: because Tri (as with Try) is bulletproof in that it catches all exceptions during processing.  If you return an Either, any further processing loses its bulletproofness.

  --Rex

[Shelby Moore]

> On Tue, Oct 9, 2012 at 5:19 PM, Shelby <she...@coolpage.com> wrote:
>
>>
>> My point was that you shouldn't be instantiating a Tri[U,Nothing],
>> because
>> by doing so, you've created a function that does not make any sense. And
>> the only way to call that function is to create a run-time error.
>>
>
>
>> Afaics, a function that inputs Nothing is nonsensical. The semantics of
>> the language never allows you to call such a function, so why would
>> create
>> one?
>>
>
> I create a method that requires a function that cannot be called.

Problem is that you've shifted a compile-time check into a run-time check.

> I do
> this for the same reason that I create a method that requires a value that
> cannot exist (e.g. a value of type Nothing): consistency of interface with
> a lack of meaningless boilerplate.

Returning instead Either[U, Throwable] would make the code more
self-documenting.

And you get rid of that asInstanceOf downcast. (this tells you that you've
opened a run-time hole somewhere)

>
> This is done all over the place in the Scala library: Nil.head, None.get,
> Vector.empty(0), Seq.empty.map((n: Nothing) => "uhoh").

Yeah, that is why my library does instead:

class Head[T]( head: T, tail: Option[Head[T]]) extends List[T]

So it is impossible to call Nil.head and get a run-time exception.

>
> Unless you do something silly like try to cast something to a type it is
> not, it's all perfectly typesafe

When did run-time type checking become preferable to compile-time checking?

>> So why not return Either[U,Throwable], so as to avoid that unsound
>> function that inputs Nothing?
>>
>
> This is harder to tell from the source: because Tri (as with Try) is
> bulletproof in that it catches all exceptions during processing. If you
> return an Either, any further processing loses its bulletproofness.

You can use the return value to instantiate another Tri.

If that doesn't address your point, I would need to see some code.

I am confident there is a way to design the API that doesn't require
pushing compile-time checks into run-time checks.

[Shelby]

On Wednesday, October 10, 2012 6:51:59 AM UTC+8, Shelby wrote:

class Head[T]( head: T, tail: Option[Head[T]]) extends List[T]

Correction:

class Head[T]( head: T, tail: List[T] ) extends List[T]

object Nil extends List[Nothing]

[Rex Kerr]

On Tue, Oct 9, 2012 at 6:51 PM, Shelby Moore <she...@coolpage.com> wrote:

> I create a method that requires a function that cannot be called.

Problem is that you've shifted a compile-time check into a run-time check.

No I haven't.  I ask for a function that can't be called, and don't call it.  That's completely consistent.  The only way to get a run-time error out of it is to cast something incorrect, which you can do in any case.
 

Returning instead Either[U, Throwable] would make the code more
self-documenting.

Not if you understand that Tri is itself a sum type of three types (two generic, one throwable).  Either is a sum type of two types.  You don't have to build three from two.
 

And you get rid of that asInstanceOf downcast. (this tells you that you've
opened a run-time hole somewhere)

No, that's just for speed.  I could pattern match on the three cases, but it's faster to do the cast.

Really, I don't think you've understood the class at all.
 

>
> This is done all over the place in the Scala library: Nil.head, None.get,
> Vector.empty(0), Seq.empty.map((n: Nothing) => "uhoh").

Yeah, that is why my library does instead:

class Head[T]( head: T, tail: Option[Head[T]]) extends List[T]

So it is impossible to call Nil.head and get a run-time exception.

So you can't call head on lists?  That is, if you know the list is nonempty but your types don't know it, you must go to the overhead of pattern matching instead of just calling head?  Okay.

But that's not the case with typing Tri[U,Nothing].  The types won't let you get in trouble, any more than Nil does.

Nil.asInstanceOf[Head[Int]].head   // Oh noes!!!

 

>
> This is harder to tell from the source: because Tri (as with Try) is
> bulletproof in that it catches all exceptions during processing.  If you
> return an Either, any further processing loses its bulletproofness.

You can use the return value to instantiate another Tri.

Yay for meaningless boilerplate.  The other conversation was about how to consolidate error-handling mechanisms into one construct.

  --Rex

[Shelby Moore]

Rex, sincerely thank you very much for sharing your example of employing
Nothing with a semantics of "no value".

This helped me to decide forcefully against ever using the name Nothing in
my code.

We can agree to disagree, if the following rebuttal doesn't convince you.

Below will probably be my last rebuttal on this code example, even if you
reply again. I don't say this to indicate I am disinterested or
unappreciative-- quite to contrary, just that I have reached the
conclusion of my logic. And also we agreed not to go on and on. I will
give you the last word on this code discussion (unless I made an error
that I must correct).

> On Tue, Oct 9, 2012 at 6:51 PM, Shelby Moore <she...@coolpage.com> wrote:
>> > I create a method that requires a function that cannot be called.
>>
>> Problem is that you've shifted a compile-time check into a run-time
>> check.
>>
>
> No I haven't. I ask for a function that can't be called, and don't call
> it. That's completely consistent. The only way to get a run-time error
> out of it is to cast something incorrect, which you can do in any case.

There is no incentive to create a (possible at compile-time) value of
Nothing (which will crash at run-time), when no function is ever
instantiated asking for such an impossible value.

The point is that thinking about bottom in as "no value" is the incorrect
semantics for an eager programming language. It causes the programmer to
create constructs which are legal at compile-time, but illegal at
run-time.

The big hint is the use of a downcast (`asInstanceOf`) in your code. This
always means we have introduced a run-time hole some where (even if
manifests external to our API).

I understand that your rebuttal that it is possible to create an instance
of Nothing at compile-time regardless of whether your code instantiates a
function which inputs Nothing. But there is no reason for the programmer
to attempt this, until you've started to think about bottom as "no value",
which thus implies it must also have a value when input to a function.

If instead you only think of bottom according to "subtype of all types"
semantics, e.g. Universe or SubOfAll, then you never have an incentive to
use a downcast as your code does to shoehorn the semantics of "no value"
into the use case of bottom.

I don't say this to be defiant, because of some ego about the point I
raised. I have demonstrated at least 2 or 3 times in this thread (which
started in scala-language), that I readily admit my objective mistakes.

Rather I press this point, because I see objectively that there is no
benefit whatsoever to emphasizing "no value" semantics for bottom (at
least not in an eager language where all values are always evaluated,
unlike in lazy Haskell where declared values aren't evaluated until they
are needed).

The claimed benefits can cause the programmer to create incorrect
semantics, that break the compile-time contract (as the example you
provided). Or it can cause the programmer to emphasize secondary
reasoning, thus muddling the local reasoning for the person studying the
code for first time (as we discussed for List[Nothing]).

I understand you are using the Steve Jobs defense, "just don't hold it
that way". But for me, it is the slippery slope sliding away from
compile-time correctness. And for no benefit, lose-lose, not even
win-lose. Of course you will argue that its subjective and thus win-lose,
with opposing opinions. I rebut in advance that the objective case is for
consistent local reasoning and not introducing downcasts.

>> Returning instead Either[U, Throwable] would make the code more
>> self-documenting.
>>
>
> Not if you understand that Tri is itself a sum type of three types (two
> generic, one throwable). Either is a sum type of two types. You don't
> have to build three from two.

I understood that, but only after deeper study. Either[U, Throwable] is
more readily understood.

More importantly, you've already thrown away P, so why continue to cart it
around? Get rid of the baggage at the earliest possible time and narrow
the type (widen the set of instances thus more degrees-of-freedom), rather
than erroneously declaring there are instances of "no value" in an eager
language. The erroneous declaration was enabled by your use of
`asInstanceOf`-- you forced the compiler not to check your type.

>> And you get rid of that asInstanceOf downcast. (this tells you that
>> you've
>> opened a run-time hole somewhere)
>>
>
> No, that's just for speed. I could pattern match on the three cases, but
> it's faster to do the cast.
>
> Really, I don't think you've understood the class at all.

I don't see how you can assign an instance of Tri[U,P] where P is not
Nothing, to Tri[U,Nothing], without using a downcast.

val v: Tri[Int,Nothing] = Good[Int,Int](0)
error: type mismatch;
found : Good[Int,Int]
required: Tri[Int,Nothing]
val v: Tri[Int,Nothing] = Good[Int,Int](0)
^

You could create a new instance of Tri[U,Nothing], extracting the type of
U and the value of the constructor parameter from the Good or Ugly using
pattern matching. But with all that boilerplate just to achieve the same
as `asIntanceOf`. Why not just return a disjunction instead. I realize
Scala doesn't have a first-class disjunction, so is the fault of Scala,
not of my conceptual point.

>> > This is harder to tell from the source: because Tri (as with Try) is
>> > bulletproof in that it catches all exceptions during processing. If
>> you
>> > return an Either, any further processing loses its bulletproofness.
>>
>>
>> You can use the return value to instantiate another Tri.
>>
>
> Yay for meaningless boilerplate. The other conversation was about how to
> consolidate error-handling mechanisms into one construct.

If Scala has a first-class disjunction then no extra boilerplate, simply
return either Good or Ugly, and with P subsumed to Any. That is the
correct semantics. So then your acceptAll function is not an oxymoron.

The only reason you wanted to force Nothing, is because you wanted the
"cute" semantics that say "this type parameter is no longer used".
Unfortunately, that is not correct construct in an eager language. And
that is why I now hate Nothing even more than before you provided this
poignant example.

>> > This is done all over the place in the Scala library: Nil.head,
>> None.get,
>> > Vector.empty(0), Seq.empty.map((n: Nothing) => "uhoh").
>>
>> Yeah, that is why my library does instead:
>>
>> class Head[T]( head: T, tail: Option[Head[T]]) extends List[T]
>>
>> So it is impossible to call Nil.head and get a run-time exception.

Hopefully you had seen the correction I sent:

class Head[T]( head: T, tail: List[T] ) extends List[T]

object Nil extends List[Nothing]

> So you can't call head on lists?

And not on Nil either. Just on Head.

> That is, if you know the list is
> nonempty
> but your types don't know it, you must go to the overhead of pattern
> matching instead of just calling head? Okay.

Yes you must do everything in a compile-time safe way. That is the purpose
of a compiler imo.

> But that's not the case with typing Tri[U,Nothing]. The types won't let
> you get in trouble, any more than Nil does.
>
> Nil.asInstanceOf[Head[Int]].head // Oh noes!!!

My Nil has no head method.

Regards,
Shelby

[Derek Williams]

On Wed, Oct 10, 2012 at 5:24 AM, Shelby Moore <she...@coolpage.com> wrote:

The big hint is the use of a downcast (`asInstanceOf`) in your code. This
always means we have introduced a run-time hole some where (even if
manifests external to our API).

This is not a hole, this is a performance optimization like Rex stated. It is a legitimate use of asInstanceOf. It does the same thing as this:

sealed trait Tri[+V,+P] {
    // ...
    def acceptAll[U >: V](f: P => U): Tri[U,Nothing] = this match {
      case Bad(p) => try { Good(f(p)) } catch { case t if Recoverable(t) => Ugly[U,Nothing](t) }

      case Good(x) => Good(x)

      case Ugly(x) => Ugly(x)
    }
    // ...

  } 

The original code avoids the overhead of creating new objects in the other cases. That is all. There is no unsafe downcasting. This technique is used throughout the scala library as well:

https://github.com/scala/scala/blob/c61c18e042d0fa41a09fea29a8dcaa2e08a40a63/src/library/scala/util/Try.scala#L167

Perhaps you'd prefer something like this?

sealed trait Tri[+V,+P] {
    // ...

    def acceptAll[U >: V, P2](f: P => U): Tri[U,P2] = this match {
      case Bad(p) => try { Good(f(p)) } catch { case t if Recoverable(t) => Ugly[U,P2](t) }
      case Good(x) => Good(x)

      case Ugly(x) => Ugly(x)
    }
    // ...

  } 

Now there is no Nothing. Except that P2 would be inferred as Nothing anyways.

--

Derek Williams

[Rex Kerr]

On Wed, Oct 10, 2012 at 7:24 AM, Shelby Moore <she...@coolpage.com> wrote:

We can agree to disagree, if the following rebuttal doesn't convince you.

That will have to be the resolution.  I find your rebuttal completely unconvincing.  Most notably, but certainly not exclusively:
 

The big hint is the use of a downcast (`asInstanceOf`) in your code. This
always means we have introduced a run-time hole some where (even if
manifests external to our API).

This is wrong.  Type bounds can claim more than they can possibly logically contain.  In this case, a downcast to what they can actually logically contain is completely safe.

  final def libraryMethod(i: Int) = {
    val x: Any = i                   // Think before changing this line!
    val y: Int = x.asInstanceOf[Int] // Or separating this one from the one above!
    y
  }

Downcasts always mean you should pay attention.

  --Rex

[Russ Paielli]

I haven't been following this discussion much, but I am curious about what this could be useful for (casting an Int to an Any then back to an Int). Thanks.

--Russ P.

[Shelby Moore]

Derek, I am not rebutting per se, but I want to repeat what I already
wrote, because (and I hope this has amicable tone as intended) your reply
causes me to be unsure if you realized that you are repeating what I
already wrote to some degree. So I prefer not to guess what you argument
against my points would be. Thanks for participating in the issue.

Also I give Rex Kerr the last word on this reply, as promised.

On Wednesday, October 10, 2012 9:00:31 PM UTC+8, Derek Williams wrote:
> case Good(x) => Good(x)
> case Ugly(x) => Ugly(x)

That is what I suggested in my prior reply:

"You could create a new instance of Tri[U,Nothing], extracting the type of
U and the value of the constructor parameter from the Good or Ugly using
pattern matching. But with all that boilerplate just to achieve the same
as `asIntanceOf`. Why not just return a disjunction instead."

> That is all. There is no unsafe downcasting.

I already stated that I consider it to be an unsafe API, because creates
an instance that has a function acceptAll, that inputs a function that
takes a value of Nothing.

The only way to make a program compile with a call to a function that
inputs a value of Nothing, is to create a runtime error with a downcast.

What I said previously (or strongly implied) is that we should not build
APIs that are unsafe or unnecessarily encourage unsafe programming. And we
should build APIs that make sense, and thus are easy-to-understand.

Afaics, this Nothing noise is just distracting from the semantics and
creating nonsensical constructs such as instances of functions that input
Nothing. I am okay with using the types of functions that input Nothing in
type bounds, but not instantiating them.

I already suggested two solutions. One is to return a first-class
disjunction of U and Throwable. The other is to change to:

case Good(x) => Good[U,Any](x)
case Ugly(x) => Ugly[Throwable,Any](x)

> This technique is used
> throughout the scala library as well:
>
> https://github.com/scala/scala/blob/c61c18e042d0fa41a09fea29a8dcaa2e08a40a63/src/library/scala/util/Try.scala#L167

I don't know of any Scala library API that instantiates a function that
inputs a value of Nothing. If that code link is doing it, I didn't quickly
grasp it.

> Perhaps you'd prefer something like this?

> case Good(x) => Good(x)
> case Ugly(x) => Ugly(x)
>

> Now there is no Nothing. Except that P2 would be inferred as Nothing
> anyways.

No. I suggested subsuming to Any.

[Shelby Moore]

> Also I give Rex Kerr the last word on this reply, as promised.

I am losing my mind. I meant "last word on HIS reply". Meaning I won't
reply to what he wrote. I think we can leave it at that.

[Shelby Moore]

I noticed something else, that I hadn't thought of before.

> def acceptAll[U >: V](f: P => U): Tri[U,Nothing]

So this means I can do:

val v: Tri[Any,Any] = ...acceptAll...

So we might as well subsume to Any, since the Nothing can be easily throw
away by the consumer of the API.

Afaics, the advantage of returning Tri[U,Any] is not only do we lose the
function that inputs Nothing, but also the return value can not be
assigned to any concrete type parameter. So that is more like what you
trying to accomplish, then the function can't be call for any value of P
except Any.

Honestly I didn't spend more than 30 seconds, so I someone needs to check
if it compiles and if I am correct.

[Derek Williams]

I'm going to have the join the "agree to disagree" group here then. 'Nil.foreach' also takes a Nothing, and I'm quite fine with that since Nil is usually cast to some supertype of List[Nothing] before it's actually used.

And returning Any as a type parameter instead of Nothing makes about as much sense as 'case object None extends Option[Any]', which I also don't agree with. I'll just have to leave it at that I guess.

On Wed, Oct 10, 2012 at 2:37 PM, Shelby Moore <she...@coolpage.com> wrote:

Derek, I am not rebutting per se, but I want to repeat what I already
wrote, because (and I hope this has amicable tone as intended) your reply
causes me to be unsure if you realized that you are repeating what I
already wrote to some degree. So I prefer not to guess what you argument

...

 

--

Derek Williams

[Rex Kerr]

Oh, it's completely useless, but completely safe.  Shelby said that downcasting via asInstanceOf _always_ means that we've introduced a run-time hole.  I provided an example where there is no run-time hole, just to demonstrate that his claim was incorrect.

  --Rex

[Shelby Moore]

On Thursday, October 11, 2012 5:51:39 AM UTC+8, Derek Williams wrote:
> I'm going to have the join the "agree to disagree" group here then.
> 'Nil.foreach' also takes a Nothing, and I'm quite fine with that since Nil
> is usually cast to some supertype of List[Nothing] before it's actually
> used.

Hopefully you've seen my preferred encoding of List[T], Head[T], and Nil
in my recent message.

In the library I am building, Nil has no fields. It shouldn't be any other
way.

Compile-time safety, correctness, clarity, and lack of nonsensical
constructions.

> And returning Any as a type parameter instead of Nothing makes about as
> much sense as 'case object None extends Option[Any]', which I also don't
> agree with.

I have never used Try, so I have no understanding of what the return value
of acceptAll is going to be used for.

However, I presume that the point of throwing away P, is that we don't
intend to upcast away the Nothing (enabling to call acceptAll with a value
other than Nothing).

Thus I assume we only want to assign the Tri[U,Any] to a Tri[T >: U,Any].
So if that is a correct assumption, then you are incorrect to make the
analogy wherein you declared a None that would not be assignable any type
T >: Any.

> I'll just have to leave it at that I guess.

I'd like to too, but perhaps I have introduced clarity (or mistakes?) that
requires one last followup?

>
> On Wed, Oct 10, 2012 at 2:37 PM, Shelby Moore <she...@coolpage.com> wrote:
>
>> Derek, I am not rebutting per se, but I want to repeat what I already
>> wrote, because (and I hope this has amicable tone as intended) your
>> reply
>> causes me to be unsure if you realized that you are repeating what I
>> already wrote to some degree. So I prefer not to guess what you argument
>> ...
>>
>
> --
> Derek Williams
>

[Shelby Moore]

On Thursday, October 11, 2012 5:51:39 AM UTC+8, Derek Williams wrote:
>In the library I am building, Nil has no fields.

Correction, well at least no fields that input Nothing or return null or
immediately throw an exception.

It does have the fields of Monad, Applicative, Functor, Traversable,
MonoidLifted.

[Rex Kerr]

On Wed, Oct 10, 2012 at 7:24 PM, Shelby Moore <she...@coolpage.com> wrote:

I'd like to too, but perhaps I have introduced clarity (or mistakes?) that
requires one last followup?

Just mistakes, lots of mistakes.  The worst at the moment is confusing Top and Bottom in that you're confusing uninhabited options on a sum type with arbitrarily inhabited options.  I think that beats the "if I create a function I must also create a value to pass to it" nonsense.

If you want to look at the full code,
  http://pastebin.com/Lz0JgkGA

If you want to read the discussion that led to it,
  https://groups.google.com/forum/?fromgroups=#!topic/scala-user/kBhxMuzzXng

You are of course free to write your code the way you find most effective or pleasing, but I'm tired of trying to convey what ought to be pretty basic concepts to someone who seems unable or unwilling to grasp any alternative techniques or viewpoints.  If you can't figure out how to use Tri productively and type-safely, just don't use it.

  --Rex

[Shelby]

On Thursday, October 11, 2012 6:50:26 AM UTC+8, Rex Kerr wrote:

Oh, it's completely useless, but completely safe.  Shelby said that downcasting via asInstanceOf _always_ means that we've introduced a run-time hole.  I provided an example where there is no run-time hole, just to demonstrate that his claim was incorrect.

I think he was perhaps astutely implying that I probably meant _always_ qualified by operating on an unknown instance type, i.e. where the upcasting is propogated and interacts external to what you know and control.

[Rex Kerr]

Your comment isn't even relevant.  This is:

val x: Either[A,B] = ???
val f: A => B = ???
x match {
  case Left(l) => Right(f(l))
  case _ => x
}

Do you see any A's remaining?  Any possible way an A could remain?  I don't understand why this is so hard.

  --Rex

[Shelby Moore]

> On Wed, Oct 10, 2012 at 7:24 PM, Shelby Moore <she...@coolpage.com> wrote:
>> I'd like to too, but perhaps I have introduced clarity (or mistakes?)
>> that
>> requires one last followup?

Rex, this reply wasn't addressed to you, so I wasn't forcing you to
explain anything.

> Just mistakes, lots of mistakes. The worst at the moment is confusing Top
> and Bottom in that you're confusing uninhabited options on a sum type with
> arbitrarily inhabited options.

I don't know what you are thinking about here, but I do not see where I
have conflated Top and Bottom. You would have to show in code what you
mean. I bet you conflated some things I have written.

> I think that beats the "if I create a
> function I must also create a value to pass to it" nonsense.

What are you talking about?

Did I ever say your API had to create a value of Nothing?

Seems you might be the one conflating orthogonal things.

> ...I'm tired

We agreed to disagree. Now you come slander me. Cheap shots are not the
way to prove anything. Show the code that demonstrates your allegation
above.

> of trying to convey what ought to be pretty
> basic concepts

Rather I think I have been explaining to you some basic concepts. I still
don't think you get them.

> to someone who seems unable or unwilling to grasp any
> alternative techniques or viewpoints.

You are stubbornly clinging to your stance. I am to mine. Either it is
subjective or one of us is correct. If you have some allegations, then by
all means show it. Because you may find out that you were the one
conflating. Or we may find out that you are correct.

> If you can't figure out how to use
> Tri productively and type-safely, just don't use it.

It is not necessary for me to learn how to use all the APIs of your code
in order to have the sort of discussion that are having about one isolated
aspect of your code.

If you feel I am missing something, you can explain or your can agree to
disagree. But unproven slander is not acceptable, nor is it professional.

[Rex Kerr]

On Wed, Oct 10, 2012 at 8:03 PM, Shelby Moore <she...@coolpage.com> wrote:

> On Wed, Oct 10, 2012 at 7:24 PM, Shelby Moore <she...@coolpage.com> wrote:
>> I'd like to too, but perhaps I have introduced clarity (or mistakes?)
>> that
>> requires one last followup?

Rex, this reply wasn't addressed to you, so I wasn't forcing you to
explain anything.

As you can tell from my tone, I'm wholly tired of this discussion.  But if you're replying in a public forum about code that I wrote, it's a little silly to claim that it's not to me, no?  Granted, Derek seems to understand what's going on, so I could just leave it to him.
 

> Just mistakes, lots of mistakes.  The worst at the moment is confusing Top
> and Bottom in that you're confusing uninhabited options on a sum type with
> arbitrarily inhabited options.

I don't know what you are thinking about here, but I do not see where I
have conflated Top and Bottom. You would have to show in code what you
mean. I bet you conflated some things I have written.

  Good(x) => Good[U,Any](x)

This says, "I know I have a Good(x).  Therefore, I forget any details about what the error conditions might have been, and tell you that any possible thing might have gone wrong, even though I'm sure that nothing at all went wrong."

This is what happens when you confuse Top and Bottom types.
 

>  I think that beats the "if I create a
> function I must also create a value to pass to it" nonsense.

What are you talking about?

Did I ever say your API had to create a value of Nothing?

That was your argument against using Nothing.  That, and the run-time hole that doesn't exist unless you create a value of Nothing.  So, yes, you did--admittedly "must" is too strong, but your alarmed rejection of Nothing seemed pretty drastic.
 

You are stubbornly clinging to your stance. I am to mine. Either it is
subjective or one of us is correct. If you have some allegations, then by
all means show it.

How, exactly?  It's not like I haven't tried.  I've explained, posted code, and so on, and your respond e.g. by widening the type of the failure case when you are sure you have a success.  What if I pass this to code that knows how to fix errors of type String, if there is an error?  That is, it promises: forall y, if y is an error of type string, I will fix it (whatever that means).  This is true if the set is empty.  So I should be able to call that function.  Your typing prevents that.
 

If you feel I am missing something, you can explain or your can agree to
disagree.

Well, I'll try to maintain a more civil tone, if I reply at all.  That's usually a good thing to do regardless.

  --Rex

[Shelby Moore]

> On Wed, Oct 10, 2012 at 7:44 PM, Shelby <she...@coolpage.com> wrote:
>
>> On Thursday, October 11, 2012 6:50:26 AM UTC+8, Rex Kerr wrote:
>>
>>> Oh, it's completely useless, but completely safe. Shelby said that
>>> downcasting via asInstanceOf _always_ means that we've introduced a
>>> run-time hole. I provided an example where there is no run-time hole,
>>> just
>>> to demonstrate that his claim was incorrect.
>>>
>>
>> I think he was perhaps astutely implying that I probably meant _always_
>> qualified by operating on an unknown instance type, i.e. where the
>> upcasting is propogated and interacts external to what you know and
>> control.
>>
>
> Your comment isn't even relevant. This is:

Perhaps you missed my point.

Upcasting in an inductive (eager) language exposes your program to the
indeterminance of the entire Universe. It was implied that I meant
inputting and outputting publicly the types involved in the upcast.

Thus I don't see how your example below applies. I don't even see an
upcast below. I guess you are thinking about how an input type is erased
from the result. Afaics that is irrelevant to my point.

>
> val x: Either[A,B] = ???
> val f: A => B = ???
> x match {
> case Left(l) => Right(f(l))
> case _ => x
> }
>
> Do you see any A's remaining? Any possible way an A could remain?

No type A remaining in the result of the match expression.

That is unless B is an A, ha! I don't remember if Either uses Mile's
ambiguity rule:

http://www.chuusai.com/2011/06/09/scala-union-types-curry-howard/#comment-72

> I
> don't
> understand why this is so hard.

Okay I admit I've been obfuscating the erotic images. So now you know why
it is so hard, in both possible ways.

[Shelby Moore]

I have a new idea for you. See below. trait Tri[+V,+P <: Option[_]]

>> Rex, this reply wasn't addressed to you, so I wasn't forcing you to
>> explain anything.
>>
>
> As you can tell from my tone, I'm wholly tired of this discussion.

Mutual.

> But if
> you're replying in a public forum about code that I wrote, it's a little
> silly to claim that it's not to me, no? Granted, Derek seems to
> understand
> what's going on, so I could just leave it to him.

I wasn't saying you could not reply.

I was trying to finish with Derek and the thread.

I am willing to reengage below, if it necessary to clarify.

Hope I will not be misunderstood again.

>> > Just mistakes, lots of mistakes. The worst at the moment is
>> confusing
>> Top
>> > and Bottom in that you're confusing uninhabited options on a sum type
>> with
>> > arbitrarily inhabited options.
>>
>> I don't know what you are thinking about here, but I do not see where I
>> have conflated Top and Bottom. You would have to show in code what you
>> mean. I bet you conflated some things I have written.
>>
>
> Good(x) => Good[U,Any](x)
>
> This says, "I know I have a Good(x). Therefore, I forget any details
> about
> what the error conditions might have been, and tell you that any possible
> thing might have gone wrong, even though I'm sure that nothing at all went
> wrong."
>
> This is what happens when you confuse Top and Bottom types.

I most definitely did not confuse Top and Bottom above. That wasn't the
issue of confusion.

I had said the above was not my preferred proposal. I was proposing
initially to return a first-class disjunction of U and Throwable. And you
replied that you did not want boilerplate. So rather quickly I offered the
above alternative. In fact, I did not even write it down in code, I just
wrote an english description. So I just imaged the code in my head for a
brief moment.

I was thinking that since +P is covariant in the trait and in f: P => U
(input of an input), that P would somehow be bounded between Any and Any.
That is because I spent maybe 30 - 60 seconds on that suggestion. But
after thinking a bit longer now on it, I was conflating inputting an
impossible value of Nothing directly to f, conflated with inputting to
acceptAll (and it somehow getting into the input of f, haha).

Calling f obviously will allow any type to be input if P is Any.

So I have to revert only to my suggestion to return the disjunction of U
and Throwable. And yeah, I am sorry Scala doesn't have a first-class one
and Either is boilerplate. But for my purposes, I am going to use a
language with a first-class disjunction.

I have another idea if need at Tri output from acceptAll, you could
require P to be a subtype of Option. Then return Tri[U,Option[Nothing]]
from acceptAll. Then you would have what you want without the functions
that input a value of Nothing. Again you might complain about boilerplate,
but I think it would be a lot clearer to novices and close the semantic
weakness.

I just realized I have an inconsistency unrelated to any confusion of Top
and Bottom. Your acceptAll method is not inputting Nothing, rather it is
inputting a function that inputs Nothing. Thus the consumer of your API
does not have to create a value of Nothing ever. Nevertheless, I still
stand by my argument against Nothing, because where some other use case
made P contravariant, then the API could input Nothing into a method.

And I still don't understand what using Nothing instead of returning a
disjunction gains you, other than boilerplate problem of Either?

So since I don't know of any gain for using Nothing, and I don't see your
code being more comprehensible with a bunch of Nothing, as compared to
removing the type parameter from the return value (instead of filling it
with Nothing), then I remain against Nothing.

If you can show me how retaining the type parameter and using Nothing is
essential or even significantly beneficial as compared to returning a
disjunction from acceptAll, then I might start to see a use case for
Nothing.

>> > I think that beats the "if I create a
>> > function I must also create a value to pass to it" nonsense.
>>
>> What are you talking about?
>>
>> Did I ever say your API had to create a value of Nothing?
>>
>
> That was your argument against using Nothing.

In the case of your code for acceptAll, yes you are correct. I was
thinking generally where Nothing could be the type of the input for a
contravariant parameter.

So I was conflating your API and all possible APIs, because I am more
focused on the general question whether it is wise to encourage use of
name Nothing.

In my mind, I was thinking your API was inputting Nothing, not inputting a
function that input Nothing.

We have covered a lot of very intricate and lengthy details. And I was
more fresh earlier in the thread. I've had my mind mostly focused on the
big picture of Nothing, while also doing other very intense thinking work
on other things between our exchanges (documenting Applicative,
Traversable, and State monad):

http://copute.com/docs/

You know your code like that back of your hand. I just glanced at it, in
the midst of doing many other things. (as well as no food here, have to
drive 1 hour to eat, so I only been eating 1x or 2x per day, poor quality
white rice and vegetables only, get so hungry and only sleeping about 4
hours).

> did--admittedly "must" is too strong, but your alarmed rejection of
> Nothing
> seemed pretty drastic.

I am getting exhausted here. I was trying to shut down the debate, before
I fall apart here. Also suffering from peripheral neuropathy, which has
spread recently to my abdomen even face. I put as much time as I could,
and ran out of time, energy, food, etc... So yeah, the further we push it,
the worse my thinking, spelling, conciseness, etc.. because I am depleting
from every direction.

You know finite resources. The real world.

I am fairly confident that I have a strong point against Nothing, but I am
interested to know if there is a reason that Tri.acceptAll can't return
disjunction or use the Option idea.

>>
>> You are stubbornly clinging to your stance. I am to mine. Either it is
>> subjective or one of us is correct. If you have some allegations, then
>> by
>> all means show it.
>
>
> How, exactly? It's not like I haven't tried.

You have tried, and I didn't see any clear logic to reject using an
disjunction (or now Option) instead of Nothing.

So that is why I came a conclusion.

But when I said "nonsensical", I was thinking thinking about inputting a
value of Nothing. Now I realize that isn't true for your Tri, but yet
afaics it remains possible in general for use cases for Nothing.

> I've explained, posted
> code,
> and so on, and your respond e.g. by widening the type of the failure case
> when you are sure you have a success.
> What if I pass this to code that
> knows how to fix errors of type String, if there is an error? That is, it
> promises: forall y, if y is an error of type string, I will fix it
> (whatever that means). This is true if the set is empty. So I should be
> able to call that function. Your typing prevents that.

You are still talking about only one of my suggestions. And it was the one
I said I did not prefer. And it is the one I have now realized is
incorrect.

We still had the disjunction idea. And now I added the Option.

>> If you feel I am missing something, you can explain or your can agree to
>> disagree.
>>
>
> Well, I'll try to maintain a more civil tone, if I reply at all. That's
> usually a good thing to do regardless.

Sorry if I made you so frustrated.

I also want the final resolution.

Need to catch up on eating and stuff. And try to get over to my mountain
rental house where it is cooler and bring a cook/maid.

I am rambling because I am dizzy, I am so hungry.

[Shelby]

On Thursday, October 11, 2012 8:38:27 AM UTC+8, Shelby wrote:

Upcasting in an inductive (eager) language exposes your program to the

Errrr. Downcasting that should be.

 

upcast below. I guess you are thinking about how an input type is erased

Ditto.

[Shelby Moore]

> I have a new idea for you. See below. trait Tri[+V,+P <: Option[_]]

> I have another idea if need at Tri output from acceptAll,
> you could require P to be a subtype of Option. Then return
> Tri[U,Option[Nothing]] from acceptAll. Then you would have
> what you want without the functions that input a value of
> Nothing. Again you might complain about boilerplate, but I
> think it would be a lot clearer to novices and close the
> semantic weakness.

We have this standard in Scala for optional values.

Why would you choose to not use it?

We already get so many complaints about how Scala code is so hard to read.

Why can't we stick to the standard idioms?

What did you gain and what did you lose with this obscure use of Nothing?

[Shelby]

Rex and Derek,

It seems that Tri[U,Nothing] doesn't protect your API from anything, because this instance can be assigned to:

Tri[U,Any]

So as much as Rex criticized me for the error of suggesting the return of Tri[U,Any], your code has the same error no?

Returning Tri[U,Nothing] is no different than returning Tri[U,Any], because the consumer of your API can UPcast it to Tri[U,Any].

So as I said before, using Nothing (essentially a defacto DOWNcast, i.e. implied asInstanceOf), exposes your program to the entire Universe of indeterminance.

So now do you finally believe me that Bottom is Universe? (analyze how the Any and Nothing get interchanged between the covariant return position and covariant input of the function f, then you see clearly the categorical dual has bitten your code)

You see trying to pretend that bottom is an nonexistent value, just allows your design to end up with the Universe where you did not intend it to be.

I knew I was correct on the theory!

Am I wrong?

So for the same reason, Option[None] won't work. You have to use my original preferred suggestion-- return a disjunction with P discarded.

[Derek Williams]

On Wed, Oct 10, 2012 at 8:34 PM, Shelby <she...@coolpage.com> wrote:

Rex and Derek,

It seems that Tri[U,Nothing] doesn't protect your API from anything, because this instance can be assigned to:

Tri[U,Any]

It better be, that is by design. 

 

So as much as Rex criticized me for the error of suggesting the return of Tri[U,Any], your code has the same error no?

That's not an error. Returning a Tri[U,Any] means we must resort to runtime type checking at some point to figure out what that Any is.

 

Returning Tri[U,Nothing] is no different than returning Tri[U,Any], because the consumer of your API can UPcast it to Tri[U,Any].

Sure it is different. Take Either for example, first with it's default return types, which of course include Nothing:

scala> val right = Right(3)

right: Right[Nothing,Int] = Right(3)

scala> val left = Left("foo")

left: Left[java.lang.String,Nothing] = Left(foo)

scala> val result = if (true) right else left

result: Product with Serializable with Either[java.lang.String,Int] = Right(3)

Now that is no good. We got a Either[String, Int]! Lets fix this:

scala> val right: Either[Any, Int] = Right(3)

right: Either[Any,Int] = Right(3)

scala> val left: Either[String, Any] = Left("foo")

left: Either[String,Any] = Left(foo)

scala> val result = if (true) right else left

result: Either[Any,Any] = Right(3)

Now that's better, right?

The reason Rex's class returns Nothing as a type parameter on certain methods is to keep the types correct. Once you use Any, it's runtime checking to figure out what you got.

So as I said before, using Nothing (essentially a defacto DOWNcast, i.e. implied asInstanceOf), exposes your program to the entire Universe of indeterminance.

The opposite is true. At least with the examples Rex and myself are showing. 

 

So now do you finally believe me that Bottom is Universe? (analyze how the Any and Nothing get interchanged between the covariant return position and covariant input of the function f, then you see clearly the categorical dual has bitten your code)

Rex's code is type safe. If Any was used instead, it would not be anymore. And that would be a pain.

 

You see trying to pretend that bottom is an nonexistent value, just allows your design to end up with the Universe where you did not intend it to be.

I don't much care about the value of bottom, since it's nothing I have to deal with, only the type. I don't much care about the name that is used either, but I am comfortable with Nothing, and it does make it easier to teach then to explain to someone that if you try in instantiate bottom you will cause the universe to end or some such thing.

 

I knew I was correct on the theory!

Am I wrong?

About this? Yes. I don't have a strong enough theoretical foundation to judge your previous Bottom/Universe discussion, but I know the bit of code that Rex had posted was type safe, and correct. There are of course different ways of doing it, like you say. I assume from the little code you've posted that you'd rather see something like these types, if you were making the same classes:

sealed trait Tri

case class Good[A](value: A) extends Tri

case class Bad[A](value: A) extends Tri

case class Ugly(value: Throwable) extends Tri

And that is fine too. There are yet others that will say, "no, this is the correct way":

sealed trait Tri[G, B] {

  def fold[T](g: G => T, b: B => T, u: Throwable => T): T

}

object Tri {

  def good[G](value: G) = new Tri[G, Nothing] {

    def fold[T](g: G => T, b: Nothing => T, u: Throwable => T): T = g(value)

  }

  def bad[B](value: B) = new Tri[Nothing, B] {

    def fold[T](g: Nothing => T, b: B => T, u: Throwable => T): T = b(value)

  }

  def ugly(value: Throwable) = new Tri[Nothing, Nothing] {

    def fold[T](g: Nothing => T, b: Nothing => T, u: Throwable => T): T = u(value)

  }

}

And that is perfectly acceptable as well, and safe.

I only stepped into this discussion because I saw perfectly fine, innocent code being told it was wrong and incorrect, when it wasn't.

--

Derek Williams

[Shelby Moore]

>> So as much as Rex criticized me for the error of suggesting the return
>> of Tri[U,Any], your code has the same error no?
>>
>
> That's not an error.

acceptAll returns Tri[U,Nothing] by design I assume to enforce a contract
that P remains Nothing?

val v: Tri[Int,Any] = ...acceptAll[Int]...
v.acceptAll( (p : SomeType) => Int )

What happened to the guarantee of Nothing? (it was UPcasted away)

> Returning a Tri[U,Any] means we must resort to
> runtime
> type checking at some point to figure out what that Any is.

Six, one-half, or dozen.

1. If you never have UPcasting as shown above, then you will never have
Any unless it was returning from acceptAll. Thus Any and Nothing can be a
synonmous semantic marker.

2. If you ever have UPcasting as shown above, then you will never know
whether it was Nothing or Any returned from acceptAll or some other value
of P, thus the Nothing guarantee is an illusion.

So using Any or Nothing to mark the absense of P, is synonmous for both #1
and #2.

And #2 is the only safe case, thus Nothing is useless.

>> Returning Tri[U,Nothing] is no different than returning Tri[U,Any],
>> because the consumer of your API can UPcast it to Tri[U,Any].
>>
> Sure it is different. Take Either for example, first with it's default
> return types, which of course include Nothing:

Irrelevant strawman approaching below...please read above.

> scala> val right = Right(3)
> right: Right[Nothing,Int] = Right(3)
>
> scala> val left = Left("foo")
> left: Left[java.lang.String,Nothing] = Left(foo)
>
> scala> val result = if (true) right else left
> result: Product with Serializable with Either[java.lang.String,Int] =
> Right(3)
>
> Now that is no good. We got a Either[String, Int]! Lets fix this:
>
> scala> val right: Either[Any, Int] = Right(3)
> right: Either[Any,Int] = Right(3)
>
> scala> val left: Either[String, Any] = Left("foo")
> left: Either[String,Any] = Left(foo)
>
> scala> val result = if (true) right else left
> result: Either[Any,Any] = Right(3)
>
> Now that's better, right?
>
> The reason Rex's class returns Nothing as a type parameter on certain
> methods is to keep the types correct. Once you use Any, it's runtime
> checking to figure out what you got.
>
> So as I said before, using Nothing (essentially a defacto DOWNcast, i.e.
>> implied asInstanceOf), exposes your program to the entire Universe of
>> indeterminance.
>>
>
> The opposite is true.

Not that I see. Unless I missing something above.

> At least with the examples Rex and myself are
> showing.
>
>
>> So now do you finally believe me that Bottom is Universe? (analyze how
>> the
>> Any and Nothing get interchanged between the covariant return position
>> and
>> covariant input of the function f, then you see clearly the categorical
>> dual has bitten your code)
>>
>
> Rex's code is type safe.

See my rebuttal above.

> If Any was used instead, it would not be anymore.
> And that would be a pain.
>
>
>> You see trying to pretend that bottom is an nonexistent value, just
>> allows
>> your design to end up with the Universe where you did not intend it to
>> be.
>>
>
> I don't much care about the value of bottom, since it's nothing I have to
> deal with, only the type.

On that I agree. The empty value of bottom is never relevant (because it
is actually never empty in any use case).

> I don't much care about the name that is used
> either, but I am comfortable with Nothing, and it does make it easier to
> teach then to explain to someone that if you try in instantiate bottom you
> will cause the universe to end or some such thing.

That doesn't teach anything useful about bottom. Not being able to
instantiate has nothing to do with the use cases.

It being the subtype of all types is the only thing that matters in the
local reasoning of all use cases.

When the programmer codes with the semantic Nothing for bottom, then get
mistakes like have now in Tri, where it was forgotten that Tri[U,Nothing]
can be UPcasted away to Tri[U,Any].

Nothing is not a marker and should never be used as one. It is only a
(unbounded quantification) bound. And that is a very important distinction
as illustrated above.

>
>
>> I knew I was correct on the theory!
>>
>> Am I wrong?
>>
>
> About this? Yes.

How so? See rebuttal above.

> I don't have a strong enough theoretical foundation to
> judge your previous Bottom/Universe discussion,

I think if someone here did, they would readily tell you that it is easy
to predict that you will create code with semantic holes, when we
erroneously impute a Nothing placeholder semantic on bottom (because a
coinductive type can never hold its place in an inductive language).

> but I know the bit of code
> that Rex had posted was type safe, and correct.

Disagree. See rebuttal above.

> There are of course
> different ways of doing it, like you say. I assume from the little code
> you've posted that you'd rather see something like these types, if you
> were
> making the same classes:

I am fine with any strategy for the code that does not attempt to use a
Nothing semantic for bottom. I am not close enough to that code to pick a
strategy beyond that.

> I only stepped into this discussion because I saw perfectly fine, innocent
> code being told it was wrong and incorrect, when it wasn't.

If my rebuttal above is wrong, I need to know why.

[Derek Williams]

On Wed, Oct 10, 2012 at 10:51 PM, Shelby Moore <she...@coolpage.com> wrote:

>> So as much as Rex criticized me for the error of suggesting the return
>> of Tri[U,Any], your code has the same error no?
>>
>
> That's not an error.

acceptAll returns Tri[U,Nothing] by design I assume to enforce a contract
that P remains Nothing?

Oh, no. It's because there is no useful type to put there. Just like the 'strawman' Either example I put. Tri is a similar data structure to Either, so the comparison is quite apt. Tri is covariant in P, it is meant to upcast to the correct type. Just like Either is meant to upcast to the correct type in the example I gave that you dismissed.

Nothing is not being used as a marker, I'm not sure where that idea came from. It is there because it's the correct type.

I did a quick search to get the rest of the code for Tri:

http://pastebin.com/Lz0JgkGA

As you can see, you are able to do the following (explicit types are just for clarity):

def validateLength[A](str: A): Try[Int, String] =

  if (str.length > 5)

    Good(str.length)

  else

    Bad("String was too short")

val myGoodValue: Try[String, Nothing] = Good("foo")

val myBadValue: Try[Int, String] = myGoodValue flatMap validateLength

val myRecoveredValue: Try[Int, Nothing] = myBadValue acceptAll (_.length)

val myFinalValue: Try[String, String] = myRecoveredValue flatMap { len =>

  if (len % 2 == 0)

    Good("Length is even")

  else

    Bad("Length is odd")

}

I really fail to see what is incorrect here? all explicit types I added could be left out. This is a very similar usecase to Either. Actually in this example I'm not taking advantage of the third state, so this is exactly like Either.

--

Derek Williams

[Shelby Moore]

Finally someone showed me how Tri is used. Thank you!

(assume you meant Tri below, not Try)

> val myRecoveredValue: Try[Int, Nothing] = myBadValue acceptAll (_.length)
>
> val myFinalValue: Try[String, String] = myRecoveredValue flatMap { len =>

UPcasting from Nothing to String gives same result (looked at flatMap
source code):

val myRecoveredValue: Try[Int, String] = myBadValue acceptAll (_.length)

val myFinalValue: Try[String, String] = myRecoveredValue flatMap { len =>

UPcasting from Nothing to anything that is not a subtype of String, will
not compile:

val myRecoveredValue: Try[Int, Any] = myBadValue acceptAll (_.length)

val myFinalValue: Try[String, String] = myRecoveredValue flatMap { len =>

So the point I have been making is that Nothing (an nonexistent value) is
not the enforced semantics, and it entirely meaningless there.

There only enforced semantics is "subtype of all subtypes", i.e. Universe
or Bottom.

So is my point finally clear?

> I really fail to see what is incorrect here? all explicit types I added
> could be left out. This is a very similar usecase to Either. Actually in
> this example I'm not taking advantage of the third state, so this is
> exactly like Either.

The implied semantics (given by the meaning of the word nothing) that
Nothing marks an empty error condition in the Tri, is proven to be false,
by the fact that I can assign Tri[Int,Nothing] to a Tri[Int,String] and
the code still compiles and works the same.

The point is as I have been saying all along, and even what I said in my
prior reply to you. In fact, I have said this in the very early posts of
this thread. It just wasn't clear to you, without an example like the
above.

The use cases of bottom are never "nonexistent value".

We are always using bottom to indicate a type bound.

Thus bottom is not Nothing. I said this is my first post.

As for names for bottom that indicate the "subtype of all types", there
are some alternatives to choose from, e.g. Bottom, SubOfAll, Universe,
Never. I like Universe the best, but that is my subjective choice amongst
the set of any name that can reasonably mean a type bound.

[Shelby Moore]

Perhaps the following (from private email) is a better way to explain my
perspective on Nothing in the Tri use case.

With Derek's clear example of Tri's usage, then afaics I showed that P is
never enforcing a "non-existent value" semantic, rather it is only
providing a lower bound for the possible types on the error condition (as
seen by Q >: P in the flatMap method of Tri).

The consumer of the Tri API, can UPcast Nothing to any lower bound (e.g.
String as I showed). The lower bound will have to agree with the lower
bound of any error conditions the consumer wishes to apply with for
example flatMap.

I can't find any semantic where the Nothing is enforcing some
"non-existent value". As well, the consumer of the API isn't going to see
the word Nothing. When studying the API versus just using it from examples
(i.e. not for the average programmer), one will need to be thinking about
bottom as the "subtype of all types" in order to understand the code.
Afaics, thinking about a "non-existent value" won't help them.

P.S. Rex and I are amicable in private email. I do not know yet if we
still disagree on the above.

[Derek Williams]

On Thu, Oct 11, 2012 at 7:43 AM, Shelby Moore <she...@coolpage.com> wrote:

The implied semantics (given by the meaning of the word nothing) that
Nothing marks an empty error condition in the Tri, is proven to be false,
by the fact that I can assign Tri[Int,Nothing] to a Tri[Int,String] and
the code still compiles and works the same.

I marks an empty error condition, but you can upcast to "maybe there is an error condition", in order to do some useful work. Just like you can upcast anything to Any to say "I have no idea what type this value is". So it's trivial to make the type more vague, but more work to make the type more specific.

I think my point is, I could have a String, typed as a String, but upcast it to Any, and now my type is not enforcing that the value is a String.

If you want to see scaladoc of what I'd consider Nothing enforcing the lack of a value, look at the scaladoc for None. Nothing all over the place in the api there.

And when it comes to the name for bottom, I don't really much care, as you should be able to just 'import scala.{Nothing => Universe}' if that floats your boat.

--

Derek Williams

[Shelby Moore]

_|_ will refer to "the bottom type"

Tangentially, I agree there is nothing wrong with the code for Tri. It is
correctly typed. We cleared that up previously.

Our discussion remains about what is the meaning of _|_ as it is being
used in the Tri use case, and thus what is the correct name for _|_.

below...

>> The implied semantics (given by the meaning of the word nothing) that
>> Nothing marks an empty error condition in the Tri, is proven to be
>> false,
>> by the fact that I can assign Tri[Int,Nothing] to a Tri[Int,String] and
>> the code still compiles and works the same.
>>
>
> I marks an empty error condition, but you can upcast to "maybe there is an
> error condition", in order to do some useful work. Just like you can
> upcast
> anything to Any to say "I have no idea what type this value is". So it's
> trivial to make the type more vague, but more work to make the type more
> specific.
>
> I think my point is, I could have a String, typed as a String, but upcast
> it to Any, and now my type is not enforcing that the value is a String.

A) The meaning of the P type parameter in Tri, is to hold the restrictions
on the future problem **types** that can be returned.

_|_ is used in an instance of Tri where the set of possible future problem
**types** is still infinite.

This semantics is due to the Q >: P in flatMap, and thus the only type
that fits is the "subtype of all types".

B) Afaics, you and Rex are essentially arguing that the above correct
semantic is equivalent to the semantic that says Tri[_,Nothing] means
there is no problem **type** specified yet.

But afaics B is not equivalent semantics to A because:

1. _|_ is only nothing w.r.t. to instances, not w.r.t. to types.

2. Nothing gives no indication that the set of types is still open.

The correct semantic for an intuitive name would be
"NothingYetAllAreAllowed".

But that specialized name won't work in all use cases for _|_.

#1 even causes an intuitive problem because if the problem is "nothing"
then how can I change it to "something" and what is the type of that
"something" I can change it to?

Also, when creating that Tri API, one needs to know that _|_ is the
"subtype of all types" in order to correctly design and understand how the
API works.

Also, afaics the programmer will never see the name for _|_ when
interacting with the Tri API.

> If you want to see scaladoc of what I'd consider Nothing enforcing the
> lack
> of a value, look at the scaladoc for None. Nothing all over the place in
> the api there.

object None extends Option[Nothing]

Says the **type** of the instance boxed by Option is nothing. Type is
nothing?

Incorrect semantics. The library designer will need to go study and find
out that Nothing is "subtype of all types".

And if you are arguing it is more intuitive for the consumer of the API,
they never see Option[Nothing]. They only see None.

(well I guess the compiler messages might print Option[Nothing])

> And when it comes to the name for bottom, I don't really much care, as you
> should be able to just 'import scala.{Nothing => Universe}' if that floats
> your boat.

Yeah :) I also said some eons ago in this thread that we can just declare
an alias :D

Any way, I wasn't seriously asking Scala to change the name. (I stated
this before)

I wanted to test if I have an objective case against Nothing.

I also thought it was pretty cool theoretically that _|_ is the universe.
I also thought the connection to inductive (eager) and coinductive (lazy)
duality was inspired and potentially helpful for seeing the bigger picture
of type theory.

[Derek Williams]

I am sure any argument I make is something better argued by someone better versed in theory, and nothing I say below is anything you haven't heard before. I'm just going to write it out anyways, for fun :)

On Thu, Oct 11, 2012 at 11:24 AM, Shelby Moore <she...@coolpage.com> wrote:

_|_ will refer to "the bottom type"

I can agree to that for sure. 

 

Our discussion remains about what is the meaning of _|_ as it is being
used in the Tri use case, and thus what is the correct name for _|_.

Ah, I missed the bit in the middle of this thread which showed how the conversation got from the definition of bottom to correctness of Rex's example. 

 

A) The meaning of the P type parameter in Tri, is to hold the restrictions
on the future problem **types** that can be returned.

I think this might be the part where we are diverging. I consider P to be the most specific type common to the set of types that P currently represents (my vocabulary is failing me here, sorry. I hope my point is understandable).

 

_|_ is used in an instance of Tri where the set of possible future problem
**types** is still infinite.

The set of future problem types might be infinite, but the set of current problems types is empty, and the most specific type of the empty set is _|_.

 

This semantics is due to the Q >: P in flatMap, and thus the only type
that fits is the "subtype of all types".

I still prefer to think of it in terms of sets, where Q must contain P. So if P was _|_, then any other type contains P. If P was not _|_, that would add bounds to the types that Q could be.

 

B) Afaics, you and Rex are essentially arguing that the above correct
semantic is equivalent to the semantic that says Tri[_,Nothing] means
there is no problem **type** specified yet.

Correct

 

But afaics B is not equivalent semantics to A because:

1. _|_ is only nothing w.r.t. to instances, not w.r.t. to types.

Which I disagree with. When selecting the correct possible type for some expression, the most specific common type of the set of possible types is used. As the set of possible types increases, the common type generally moves towards Any (Top). So the common type of all possible types is Any. And as the set of possible types becomes smaller, the common type generally moves towards _|_, eventually reaching _|_ when the set of possible types is empty.

 

2. Nothing gives no indication that the set of types is still open.

I guess it depends how you think of types? I consider a type to be a restriction, and so Nothing reads to me like a total lack of restrictions, where Any is the restrictions of all types.

 

The correct semantic for an intuitive name would be
"NothingYetAllAreAllowed".

But that specialized name won't work in all use cases for _|_.

#1 even causes an intuitive problem because if the problem is "nothing"
then how can I change it to "something" and what is the type of that
"something" I can change it to?

 "Nothing" is a blank slate. You can keep on restricting a type with Nothing, and it doesn't change the resulting type. I don't think that takes too big of a leap.

 

Also, when creating that Tri API, one needs to know that _|_ is the
"subtype of all types" in order to correctly design and understand how the
API works.

Sure. And like you say, it's more of a requirement for a library author creating an API. 

 

Also, afaics the programmer will never see the name for _|_ when
interacting with the Tri API.

> If you want to see scaladoc of what I'd consider Nothing enforcing the
> lack
> of a value, look at the scaladoc for None. Nothing all over the place in
> the api there.

object None extends Option[Nothing]

Says the **type** of the instance boxed by Option is nothing. Type is
nothing?

The exact name used for bottom is not something I'm too concerned with. NoType, NaT (Not a Type), EmptyType. Or just use _|_, which would at least make someone new to the concept say "I have no idea what that means, I am going to look that up", whereas a name like Nothing may not spark that curiousity.

 

Incorrect semantics. The library designer will need to go study and find
out that Nothing is "subtype of all types".

Sure. "programming is hard". There are harder things a library designer will need to learn. 

 

And if you are arguing it is more intuitive for the consumer of the API,
they never see Option[Nothing]. They only see None.

(well I guess the compiler messages might print Option[Nothing])

I agree. 

 

> And when it comes to the name for bottom, I don't really much care, as you
> should be able to just 'import scala.{Nothing => Universe}' if that floats
> your boat.

Yeah :) I also said some eons ago in this thread that we can just declare
an alias :D

Any way, I wasn't seriously asking Scala to change the name. (I stated
this before)

I wanted to test if I have an objective case against Nothing.

I also thought it was pretty cool theoretically that _|_ is the universe.
I also thought the connection to inductive (eager) and coinductive (lazy)
duality was inspired and potentially helpful for seeing the bigger picture
of type theory.

I could see some concept of "universe" being an instance of something that cannot be typed, since it could have no external restrictions. Empty set of restrictions. or Nothing. And from that you could say that we are going to then call that empty type Universe, since it's the only thing that has that type.

--

Derek Williams

[Raoul Duke]

On Thu, Oct 11, 2012 at 12:43 PM, Derek Williams <de...@fyrie.net> wrote:
> I guess it depends how you think of types? I consider a type to be a
> restriction, and so Nothing reads to me like a total lack of restrictions,
> where Any is the restrictions of all types.

heh, naming is hard, and i guess kinda is often a major problem. while
saying a variable is of a type restricts the values the variable can
take on, the type itself i do not see as a restriction, more as the
name of a population. so to me naively Nothing means no population.
:-)

sincerely.

[Alex Repain]

2012/10/11 Raoul Duke <rao...@gmail.com>

To me Nothing describes something that doesn't exist, the population of what is not existent, that is, the negation of all. It is somehow ironic that I found All as intuitive as Nothing to describe the Bottom type... But I really read that as an incarnation of false => true. Nothing => All (the other way round is less intuitive).

sincerely.

[Shelby Moore]

I will be very surprised if you still disagree with me after reading this
(unless I have made a mistake).

> I am sure any argument I make is something better argued by someone better
> versed in theory, and nothing I say below is anything you haven't heard
> before. I'm just going to write it out anyways, for fun :)

I think you are clarifying the discussion quite well, thank you for
replying. I think we might be close to an agreeable logic on this.

below...

>> A) The meaning of the P type parameter in Tri, is to hold the
>> restrictions
>> on the future problem **types** that can be returned.
>>
>
> I think this might be the part where we are diverging.

Agreed we are diverging on this.

I explain below that afaics, it is because you are conflating the
covariance of P w.r.t. Tri's subtypes, conflated with the covariance of
the semantics of P.

> I consider P to be
> the most specific type common to the set of types that P currently
> represents (my vocabulary is failing me here, sorry. I hope my point is
> understandable).

I am also thinking in terms of sets and use the terms narrowest and widest
interchangeably with most-specific and least-specific.

>> _|_ is used in an instance of Tri where the set of possible future
>> problem
>> **types** is still infinite.
>>
>
> The set of future problem types might be infinite, but the set of current
> problems types is empty, and the most specific type of the empty set is
> _|_.

The former is the contravariant semantics of the type P, and the latter is
the covariant semantics of the type Tri[_+P].

>> This semantics is due to the Q >: P in flatMap, and thus the only type
>> that fits is the "subtype of all types".
>>
>
> I still prefer to think of it in terms of sets, where Q must contain P. So
> if P was _|_, then any other type contains P. If P was not _|_, that would
> add bounds to the types that Q could be.

Agreed, that is an equivalent way of explaining subtyping.

>> B) Afaics, you and Rex are essentially arguing that the above correct
>> semantic is equivalent to the semantic that says Tri[_,Nothing] means
>> there is no problem **type** specified yet.
>
>
> Correct
>
>
>> But afaics B is not equivalent semantics to A because:
>>
>> 1. _|_ is only nothing w.r.t. to instances, not w.r.t. to types.
>>
>
> Which I disagree with.

I explain further below why thinking of Nothing with covariant semantics
would require it has instances.

> When selecting the correct possible type for some
> expression, the most specific common type of the set of possible types is
> used. As the set of possible types increases, the common type generally
> moves towards Any (Top). So the common type of all possible types is Any.
> And as the set of possible types becomes smaller, the common type
> generally
> moves towards _|_, eventually reaching _|_ when the set of possible types
> is empty.

Agreed, if the subtyping relationship is covariant.

However, see point #2 below.

>> 2. Nothing gives no indication that the set of types is still open.
>>
>

> I guess it depends how you think of types? I consider a type to be a
> restriction, and so Nothing reads to me like a total lack of restrictions,
> where Any is the restrictions of all types.

Your perspective applies if the subtyping relationship is covariant.

Your semantic perspective is only valid for subtypes of Tri[_+P], not
subtypes of P! You have conflated the two. (which is the same semantic
mistake as Option[Nothing], List[Nothing], etc). Let me explain.

If we removed all the methods from Tri, P would have no (useful)
semantics. So the fact that it is declared to be +P, is not relevant until
we add some methods to define the semantics of P. The +P only declares
that P is covariant relative to subtypes of Tri. It says nothing about the
covariance of the semantics of P.

Afaics, the Q >: P in flatMap (reject, explain, etc) is what gives P its
relevant semantics. So this is saying the set of problems that we can
accept are the widest when P is the narrowest. Thus the semantics of P
(not of P relative to subtypes of Tri) are contravariant.

>> The correct semantic for an intuitive name would be
>> "NothingYetAllAreAllowed".
>>
>> But that specialized name won't work in all use cases for _|_.
>>
>> #1 even causes an intuitive problem because if the problem is "nothing"
>> then how can I change it to "something" and what is the type of that
>> "something" I can change it to?
>>
>
> "Nothing" is a blank slate. You can keep on restricting a type with
> Nothing, and it doesn't change the resulting type. I don't think that
> takes
> too big of a leap.

Yeah but afaics you will never find a case where _|_ is used in a
covariant semantics, because then it would be required that can be
instantiated.

The semantics of _|_ are always contravariant, which is why Nothing makes
no sense at all. It would be analogous to giving Any the name Nothing in
covariant semantics.

The reason is because a coinductive type can only be useful in an
inductive (eager) language, if we invert the covariance to its dual.

This is another way of proving that _|_ is the Universe.

>> Also, when creating that Tri API, one needs to know that _|_ is the
>> "subtype of all types" in order to correctly design and understand how
>> the
>> API works.
>>
>
> Sure. And like you say, it's more of a requirement for a library author
> creating an API.

So then correctness of definitions is more important than some incorrect
intuitive conflation of the covariance of the kind and the type parameter.

>> Also, afaics the programmer will never see the name for _|_ when
>> interacting with the Tri API.
>>
>>
>> > If you want to see scaladoc of what I'd consider Nothing enforcing the
>> > lack
>> > of a value, look at the scaladoc for None. Nothing all over the place
>> in
>> > the api there.
>>
>> object None extends Option[Nothing]
>>
>> Says the **type** of the instance boxed by Option is nothing. Type is
>> nothing?
>>
>
> The exact name used for bottom is not something I'm too concerned with.
> NoType, NaT (Not a Type), EmptyType.

None of those names can be the correct semantics ever. Do you now see why?

(unless you refute the logic I made about P's contravariant semantics)

> Or just use _|_, which would at least
> make someone new to the concept say "I have no idea what that means, I am
> going to look that up", whereas a name like Nothing may not spark that
> curiousity.

Yeah maybe _|_ is best, except if we are trying to make a mainstream
language, we are avoiding being blasted by Steve Yeggie's "type of type
types" and other criticisms of Scala's readability and learning curve.

Then again, we probably agree the novice will rarely see the _|_ type.

>> Incorrect semantics. The library designer will need to go study and find
>> out that Nothing is "subtype of all types".
>>
>
> Sure. "programming is hard". There are harder things a library designer
> will need to learn.

Consistency between names and semantics, can only help.

And for people who want to learn by studying the libraries.

>> Any way, I wasn't seriously asking Scala to change the name. (I stated
>> this before)
>>
>> I wanted to test if I have an objective case against Nothing.
>>
>> I also thought it was pretty cool theoretically that _|_ is the
>> universe.
>> I also thought the connection to inductive (eager) and coinductive
>> (lazy)
>> duality was inspired and potentially helpful for seeing the bigger
>> picture
>> of type theory.
>>
>
> I could see some concept of "universe" being an instance of something that
> cannot be typed, since it could have no external restrictions. Empty set
> of
> restrictions. or Nothing. And from that you could say that we are going to
> then call that empty type Universe, since it's the only thing that has
> that
> type.

Yeah you basically got the coinductive idea of it.

And when we use always in a contravariant semantics (as we are forced to
do with _|_ in an eager inductive language, because we can't make
instances of it), then it needs to be thought of as the least specific
(widest) type.

[Derek Williams]

Yeah, I think I used the wrong word there. I meant restrictions to mean more like the terms of a contract. It didn't survive the jarring transition of going from my thoughts to the screen, just like most of the rest that I wrote. :)

-- 

Derek Williams

[Raoul Duke]

On Thu, Oct 11, 2012 at 1:36 PM, Alex Repain <alex....@gmail.com> wrote:
> (the
> other way round is less intuitive).

i think the term intuitive should be banned from this thread, and
probably nigh all threads in the world ;-)

[Derek Williams]

On Thu, Oct 11, 2012 at 11:24 AM, Shelby Moore <she...@coolpage.com> wrote:

I also thought it was pretty cool theoretically that _|_ is the universe.
I also thought the connection to inductive (eager) and coinductive (lazy)
duality was inspired and potentially helpful for seeing the bigger picture
of type theory.

I think I can see your line of reasoning now, if I look at types in terms of subclassing. If Nothing is the subclass of all types then it should contain the function of all types. When I think in terms of types, I guess I don't really think about the relationships between them being due to subclassing, just that subclassing creates a relationship between 2 types. If that makes any sense.

--

Derek Williams

[Shelby]

+1 ;D

Type theory correctness, else just pull the arbitrary name out of our...

[Shelby]

On Friday, October 12, 2012 4:57:45 AM UTC+8, Derek Williams wrote:

On Thu, Oct 11, 2012 at 11:24 AM, Shelby Moore wrote:

I also thought it was pretty cool theoretically that _|_ is the universe.
I also thought the connection to inductive (eager) and coinductive (lazy)
duality was inspired and potentially helpful for seeing the bigger picture
of type theory.

I think I can see your line of reasoning now, if I look at types in terms of subclassing. If Nothing is the subclass of all types then it should contain the function of all types. When I think in terms of types, I guess I don't really think about the relationships between them being due to subclassing, just that subclassing creates a relationship between 2 types. If that makes any sense.

That is a very succinct way of explaining the duality of inductive (covariant) and coinductive (contravariant) types, using functions.

What is also interesting is how these all inverted to their opposite dual in Haskell, because it is lazy (coinductive) evaluation strategy language. Now you've shown why the eagerness of calling function operands, would impact the direction of covariance.

[Shelby]

A type is a membership rule in a set.

The rule can either be an algebra or a coalgebra, i.e. inductive constructive or coinductive destructive method of building subtypes of the set.

We are accustomed to inductive type rules, which defines a covariant relationship, e.g. "Sub adds fields extends from Super1 with Super2". The membership set gets narrower for Sub in the covariant direction. Top is a constructive type, because each time we add a type to the universe, top adds it to its disjunction. Top is analogous to if Super has multiple subtypes, it is a disjunction of all its possible subtypes and itself. j3vanek, the type of Super is not just Super:

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

Bottom is a destructive type (each type added to its conjunction), which defines a contravariant relationship, e.g. "Super1 or Super2 extends to Sub removes fields". The membership set gets wider for Sub in the contravariant direction. Every Sub is a conjunction of all its possible Super types and itself.

Since our eager evalution language lives in the covariance (inductive) semantics, we can't instantiate a coinductive type. Whereas in lazy evaluation Haskell, _|_ populates all instantiable types.

Covariance and thus Top and Bottom are relative to the evaluation strategy for the functions you use to model the universe, e.g. eager or lazy. The Church-Turning hypothesis says that recursion and lamba calculus are equivalent. Thus types can't be anything more than the relationships of the order of evaluating functions. We can express any pattern as a pattern of functions with a lazy or eager evaluation strategy.

[Shelby]

No one replied to my prior message, so I assume that made my logic clear?

Quoting below from a post I made else where, where a similar discussion continued.

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

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 is non-existent value.

Bottom is at the other end of the 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 is the root of all types! And the top type never has a value!

So you can't think about the infinite co-end of your 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 that is available in the coinductive (lazy) languages. And vice versa, in Haskell, top represents the entire universe that is available in our inductive (eager) languages, e.g. Ceylon, Java, Scala.

[Derek Williams]

On Sat, Oct 13, 2012 at 6:05 PM, Shelby <she...@coolpage.com> wrote:

No one replied to my prior message, so I assume that made my logic clear?

I think so. I have been too busy to invest any extra brain time to doing my own research on the topic (although I want to).

I find it interesting, and as far as correctness of your theory I don't have an opinion on that until I am able to research into the theory more. Until then, using Nothing as bottom, and also using it for non termination all sits right with me. Until it doesn't :)

Thanks Shelby.

--

Derek Williams

[Shelby]

Thank you also for helping me clarify my logic. Note I edited my prior reply as follows.

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

(you can also read the entire linked post, as it summarizes what I think Derek helped me clarify)

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).

[Shelby]

I have chosen `Unknown` and `Everything` for the top and bottom types respectively. The following link contains my logic:

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