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