types like Sequential<Nothing> and Tuple<X,Nothing,Y> are empty

[gavinking]

The logic of §3.4.4 is based on the notion that types like Sequential<Nothing> and Tuple<X,Nothing,Y> are exactly Nothing. But nowhere is that rule asserted or made use of by the typechecker.

[lucaswerkmeister]

Isn’t Empty a nonempty subtype of Sequential<Nothing>?

[gavinking]

Sure. I guess I mean Sequence.

Sent from my iPhone

On 23 Jul 2015, at 12:59, Lucas Werkmeister notifications@github.com wrote:

Isn’t Empty a nonempty subtype of Sequential?

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

[vbeauPer]

I found out to discuss here will be better. So Empty is expected to be the result of Empty & [Nothing],

This starts from this union of 1 and 2 arguments functions : Anything(Nothing) | Anything(Nothing, Nothing) in canonical typing this is : Callable<Anything, [Nothing]> | Callable<Anything, [Nothing, Nothing]> which is included in Callable<Anything, [Nothing] & [Nothing, Nothing]> which is included in, due to contravariant ? Callable<Anything, Tuple<Nothing, Nothing, [] & [Nothing]> and then if [] & [Nothing] is equivalent to [], then we got unexpected thing... Callable<Anything, Tuple<Nothing, Nothing, []>> alias Anything(Nothing)

THEN Anything(Nothing, Nothing) is included in Anything(Nothing) ? I would prefer the reverse

[vbeauPer]

Well, then if calcul is true, type checker will fails in some checks. I found two workaround in order to corresponds to better result : for this I have to change Tuple definition : At this time it is just for Function application. 1) Tuple<in, out, in> then we obtain : Callable<Anything, Tuple<Anything, Nothing, [] | [Nothing]>> alias Anything(Nothing, Nothing=) just as expected !

2) Callable<out, out Tuple<out, in, out>> the result is the same !

I don't know if it's the right thing to do. But actually Callable is not consistent with [Nothing=] = [] | [Nothing]

[gavinking]

On Fri, Jul 24, 2015 at 12:36 PM, vbeauPer notifications@github.com wrote:

Well, then if calcul is true, type checker will fails in some checks.

What do you mean?

Gavin King gavin@ceylon-lang.org http://profiles.google.com/gavin.king http://ceylon-lang.org http://hibernate.org http://seamframework.org

[vbeauPer]

Then you should could write (with recursivity Anything() is supertype of all functions): Integer(Integer) add = (Integer x, Integer y) => x+y; but be unable to call add(x);

[gavinking]

THEN Anything(Nothing, Nothing) is included in Anything(Nothing) ?

Yes, but only because both these type expressions are different ways to write Anything(*Nothing), i.e. "the supertype of function types you can't actually invoke".

[vbeauPer]

I remember you that Anything(Nothing) is supertype of every function with one parameter. curry take a function with at least one parameter, then you will not able to call it. But the problem is that works for every type... you can always return to empty. At no time I have use that Nothing is a special case. You will have to admit it, otherwise you will not be able to use standard type checker for checking callable type (as it is one of your will).

[gavinking]

I remember you that Anything(Nothing) is supertype of every function with one parameter. curry take a function with at least one parameter, then you will not able to call it.

@vbeauPer That's just not right. Consider:

I [remind] you that Anything is supertype of every function with one parameter. curry take a function with at least one parameter, then you will not able to call it.

Or:

I [remind] you that Anything(*Nothing) is supertype of every function with one parameter. curry take a function with at least one parameter, then you will not able to call it.

Clearly neither of those statements are correct. Nor is your original version :-)

[vbeauPer]

sorry for the language fault. You can find here my assertion : (http://ceylon-lang.org/blog/2015/04/19/observable/)

Anything(Nothing) is the supertype of any function with one parameter.

I miss to describe some reasoning here : well, for me Anything(Nothing) <=> Anything(Nothing) as Nothing is not a sequence. so it includes Anything(); curry needs at least a function with one parameter Anything(Nothing+); you will not able to detect it if we can only specify Anything(Nothing*). Well, on the start I do not known I will catch such a problem. and so, for you, what is the result of [Integer] & [] ? if it is [] then it is the same problem. We can reasoning over R(A) if you want, but the result is sadly the same.

[lucaswerkmeister]

No, Anything(*Nothing) and Anything(Nothing*) are completely different things.

Anything(*Nothing), desugared Callable<Anything,Nothing>, is the type of a function whose parameter list type is Nothing. Since there are no instances of Nothing, there is no possible argument list of this function, and you can never call it.

Anything(Nothing*), desugared Callable<Anything,Sequential<Nothing>>, is the type of a function that takes zero or more arguments of type Nothing – its parameter list type is Sequential<Nothing>. Since Empty is a subtype of Sequential<Nothing>, it is possible to call this function:

f(*empty);
f(*[]);
f();
// also legal, though it will throw at runtime:
f(nothing);
f(nothing, nothing);
f(*[nothing, nothing, nothing]);

[gavinking]

sorry for the language fault.

Nono, don't apologize! I was just trying to be helpful. :)

[gavinking]

@vbeauPer it's very important to differentiate between the prefix and postfix * syntax.

• Prefix *, pronounced "spread", in either value expressions or type expressions—means take a packaged sequence of things and flatten them out into multiple things.
• Postfix *, in type expressions and parameter declarations—means accepts multiple things.

So:

Float(*[Float,Float])

means Float(Float,Float). But

Float([Float,Float]*)

Means Float(*[[Float,Float]*]), i.e. Callable<Float,Sequential<[Float,Float]>>.

[gavinking]

Note that T(*U[]) is the type T(U*).

[vbeauPer]

OK, so Nothing is subtype of [], so we can call *Nothing. logical but interesting. somehow can we consider it as a value ? (well it is not the point). thx for the explanation.

[gavinking]

OK, so Nothing is subtype of [], so we can call *Nothing.

Correct. Nothing is subtype of [Anything*], so I can spread Nothing in a function type expression.

Likewise, I can write this in a value expression:

    void fun(Integer* ints) {}
    fun(*nothing); 

Since Nothing is a suptype of [Integer*].

At runtime, of course, this code blows up when we try to evaluate nothing, so fun() is never called.

[vbeauPer]

well OK, but this does not change my assertions.

[gavinking]

Which assertion?

[vbeauPer]

that actually you are not able to describe Anything(Nothing, Nothing*) as curry needs it.

[gavinking]

But I never want to curry a function of type Anything(Nothing, Nothing*).

I want to curry a function of type Float(Integer, Integer*) or something like that.

[vbeauPer]

you want n functions curry ? one for each type classes ?

[gavinking]

you want n functions curry ? one for each type classes ?

Of course not. That's what I have generics for!

curry() doesn't use Nothing to abstract over function signatures!

[jvasileff]

A few questions:

Does this mean that it would be impossible to curry Anything(WebRequest, Nothing*)?

Because, more generally, Anything(Whatever, Nothing*) would not exists/would be immediately simplified to its supertype Callable<Anything, Nothing>?

And even more generally, it would be impossible to a) retain statically or b) test for dynamically, partial type information (through the use of Nothing) for any consumer with a special cased type as its type parameter?

And somewhat related, it would no longer be possible to have instances of Consumer<[Integer, Nothing]>, since that type would no longer exist?

On Jul 24, 2015, at 1:09 PM, Gavin King notifications@github.com<mailto:notifications@github.com> wrote:

But I never want to curry a function of type Anything(Nothing, Nothing*).

I want to curry a function of type Float(Integer, Integer*) or something like that.

— Reply to this email directly or view it on GitHubhttps://github.com/ceylon/ceylon-spec/issues/1387#issuecomment-124582556.

[gavinking]

Does this mean that it would be impossible to curry Anything(WebRequest, Nothing*)?

No, it still works just fine. You get an Anything(Nothing*)(String).

And somewhat related, it would no longer be possible to have instances of Consumer<[Integer, Nothing]>, since that type would no longer exist?

That type still exists and still has instances. It's just that the type is equivalent to Consumer<Nothing>.

[vbeauPer]

you want n functions curry ? one for each type classes ?

Of course not. That's what I have generics for! curry() doesn't use Nothing to abstract over function signatures!

Callable<Return,Tuple<Argument,First,Rest>> Well it works as of your assertion that [] & [Integer] is equivalent to Nothing (another mathematical abstraction an empty set intersection whatever set is empty set, nothing is only its content, but take care Nothing is something which are very contagious when your mistake) then you have String(Integer) | String (Integer, Integer) is in String(*Nothing) you do not even know that it has at least one Parameter. unless you have String(Integer) a supertype of String(Integer, Integer) and then curry does not work.

[jvasileff]

No, it still works just fine. You get an Anything(Nothing*)(String)

Well, today you can't curry Callable<Anything, Nothing>. So if [WebRequest, Nothing] is a subtype of Nothing, I'm still not seeing how this is possible. Or is [WebRequest, Nothing] not the the same as Nothing?

Now, on the JVM, it appears that curry returns a Callable that is reified with the statically known types, and not the types of the underlying function. So you can't test for or recover the Nothing at runtime, making it difficult to demo lost functionality on this.

That type still exists and still has instances. It's just that the type is equivalent to Consumer<Nothing>

Huh? Isn't that like saying we could take away String, but it still exists, because we still have Anything?

---

I think this change may cause some real lost functionality, and a few surprises, and I hope you'll give this one some time for issues to bubble up and be analyzed before committing to it.

Generally, I think it is good and useful to use Anything as a placeholder for "don't care" in covariant locations, and the same for Nothing in contravariant locations. But this change would take away the latter.

One trivial example of a surprising outcome:

    class Consumer<in T>() {}
    class Pair<out A, out B>(A a, B b) {}

    value c1 = Consumer<Pair<String, String>>();
    value c2 = Consumer<[String, String]>();

    print((c1 of Anything) is Consumer<Pair<Integer, Nothing>>); // false
    print((c2 of Anything) is Consumer<[Integer, Nothing]>);     // true!!!

[jvasileff]

This working code seems odd in the latest build:

    Anything(String, String) css = plus<String>;
    Anything(Nothing)(Integer) ci = curry(css of Callable<Anything, [Integer, Nothing]>);
    assert((ci of Anything) is Anything(Integer));

Edit: but I can't prove it to be practically unsound due to the way Callables work on the JVM, because:

    Anything(Nothing) cn = ci(55);
    assert(is Anything(String) cn); // this assertion fails
    cn("55");

[vbeauPer]

sorry, the curry signature has been somehow deleted.

[lucaswerkmeister]

sorry, the curry signature has been somehow deleted.

The <> got interpreted as HTML, you have to surround them with backticks (`) to prevent that. (e. g.Callable<Anything,Nothing>``)

[vbeauPer]

OK, I endly came to figure that for the [] & [Anything], they are disjoint simply that when you request for one you cannot have the other.

[gavinking]

@jvasileff

I'm still not seeing how this is possible.

Anything(WebRequest, Nothing*) is

Callable<Anything,Tuple<WebRequest,WebRequest,Sequential<Nothing>>> 

That's not the same type as Anything(Nothing*).

[jvasileff]

Ok, I erred with the trailing * which allows [] in my first post. What I meant was, I thought these would all be the same:

curry(nothing of Anything(String, Nothing));
curry(nothing of Callable<Anything, <Tuple<String, String, [Nothing]>>>);
curry(nothing of Callable<Anything, Nothing>); // error
curry(nothing of Anything(*Nothing)); // error
curry((nothing of Anything(*Nothing)) of Anything(String, Nothing));
curry(((nothing of Anything(*Nothing)) of Anything(String, Nothing)) of Anything(*Nothing)); // error

[gavinking]

@jvasileff not necessarily, no. The way you write the type can still affect type inference.

[jvasileff]

Hm, I guess it all works out. So some Nothings are more nothing than other Nothings. Clearly you can't assign a Tuple to a plain-old-infinitely-demanding-Nothing. But you can craft a Nothing that looks like a Tuple to satisfy curry. The Tuple Nothing appears to be a bit more contravariantly useful than the nothing-Nothing. But it's a ruse. And they're all exactly Nothing.

I'm still not excited about the reduced functionality and surprises though :smile:.

[gavinking]

Yes, sure, it works out AFAICS. Unlike the previous situation where there was inconsistent behavior where two types were judged equal in some cases and unequal in others.

[gavinking]

I checked that this isn't a performance killer. It's not. Closing.