Bug on typeChecker

[vincent beauseigneur]

That say it seems that I found a bug in type checking (1.1.1) (Perhaps on current development it works), thats's why I don't post :
I tried to works with my own typechecking understandings as Anything(Nothing*) as a subtype, I tried to work on supertype.
Therefore I check my comprehension of the different equally forms of function type with one or two parameters.
Then I figure out that for their supertype I can only works on enumerated cases, so I tried this :

alias OneParam => Anything(Nothing);
alias TwoParam => Anything(Nothing, Nothing);
alias OneOrTwoParam => OneParam|TwoParam;
alias OneOrTwoParamb => Callable<Anything, Tuple<Nothing, Nothing, []&[Nothing]>>;
alias OneOrTwoParamc => Callable<Anything, [Nothing] & [Nothing, Nothing]>;

OneOrTwoParam f1o2 = (Integer x, Integer y) => x+y;
 
OneOrTwoParamb f1o2b = f1o2;
OneOrTwoParamc f1o2c = f1o2b;
OneOrTwoParam f1o2d = f1o2b; // Specified expression must be assignable to declared type of f1o2d: OneOrTwoParamb (Callable<Anything,Tuple<Nothing,Nothing,Nothing>>) is not assignable to OneOrTwoParam (Anything(Nothing)|Anything(Nothing, Nothing))
OneOrTwoParamb f1o2e = f1o2c; // Specified expression must be assignable to declared type of f1o2e: OneOrTwoParamc (Anything(*Nothing)) is not assignable to OneOrTwoParamb (Callable<Anything,Tuple<Nothing,Nothing,Nothing>>)
Callable<Anything, [Nothing] & [Nothing, Nothing]> f1o2f = f1o2;

print(f1o2);
print(f1o2b);
print(f1o2c);
print(f1o2d);
print(f1o2e);
curry(f1o2); //Argument must be assignable to parameter f of curry: OneOrTwoParam (Anything(Nothing)|Anything(Nothing, Nothing)) is not assignable to Anything(Nothing, Nothing=)
curry(f1o2b);
curry(f1o2c); //Argument must be assignable to parameter f of curry: OneOrTwoParamc (Anything(*Nothing)) is not assignable to Anything(Anything, Anything*)
curry(f1o2e);
curry(f1o2f); //The ExpressionVisitor caused an exception visiting a InvocationExpression node: "java.lang.UnsupportedOperationException" at com.redhat.ceylon.model.typechecker.model.NothingType.collectSupertypeDeclarations(NothingType.java:25)

Here, I can transfert only standard form OneOrTwoParam to other forms, the reverse is not admitted. Even as param the validation dépends on the form.  

Furthermore, for OneOrTwoParamc the type checker fails differently as it is an alias or not.

curry() here, would never work as, at runtime we got only the upper bound known by compiler, forced here to be OneOrTwoParamb.

[vincent beauseigneur]

moreover []|[Nothing] is Nothing, so the form Callable<...> could not figure difference between OneParam|TwoParam and OneParam|NParam.

The type checker seems finding a difference with the sugar form and the Callable form as I can set a three params function in the second and not in the first.

[Gavin King]

Sorry, but I don't see any bug here.

I don't see why the type:

Anything(*Tuple<Nothing, Nothing, []&[Nothing]>)

Which, since [] and [Nothing] are disjoint, is actually just:

Anything(*Tuple<Nothing, Nothing, Nothing>)

Should be assignable to Anything(Nothing)|Anything(Nothing, Nothing).


Nor do I see why:

Anything(*[Nothing] & [Nothing, Nothing])

which is just:

Anything(*Nothing)

should be assignable to Anything(*Tuple<Nothing, Nothing, Nothing>).

It seems to me that the typechecker is doing the right thing here.

> --
> You received this message because you are subscribed to the Google Groups
> "ceylon-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ceylon-users...@googlegroups.com.
> To post to this group, send email to ceylon...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ceylon-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ceylon-users/08bf165a-687b-48b9-89bb-592fe480990e%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.



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

[vincent beauseigneur]

In all way, the last curry error (even if it should fail) isn't well formed.

Let's start with some definition, to see if I miss something.

Callable <Anything, Tuple<Nothing, Nothing, [Nothing*]>> corresponds to functions which have from 1 to undetermined number of parameters (so varargs). so you can call f(x), f(x,y)...

Anything(Nothing, Nothing*)

Callable <Anything, Tuple<Nothing, Nothing, Nothing>> corresponds to any functions which have at least 1 parameter. so you cannot call f(x)

(which are in fact Anything(Nothing)|Anything(Nothing, Nothing)|Anything(Nothing, Nothing, Nothing)|...)

Is it Anything(Nothing, *Nothing) ? I didn't find where spread operator could be used for type (by reading it, I don't understand difference with undetermined number of parameters).

Isn't Anything(Nothing) quite equals to Callable<Anything, Tuple<Nothing, Nothing, []>> ?

Then I just develop as in contravariant Consumer<A>|Consumer<B> <=> Consumer<A&B>, probably I have misunderstood here (does it work only if A and B are not disjoint ?, this could make sense, what the hell could union be impossible)

Then how do I write my code :

In a matter of fact I started from there, so :

Callable<Anything, [Nothing]>|Callable<Anything, [Nothing,Nothing]> <=> Callable<Anything | Anything, [Nothing] & [Nothing, Nothing]>

then I go on Tuple form : 

<=> Callable <Anything, Tuple<Nothing, Nothing, [] & [Nothing]>

When I first wrote this lines I didn't directly see that [] & [Nothing] <=> Nothing, then my tests.

well this means that [Nothing]&[Nothing,Nothing] in tuple form quite equals Tuple<Nothing, Nothing, Nothing> which differs from Tuple<Nothing, Nothing, Nothing[]> ([Nothing+]).

 

 thx for reading

[Gavin King]

On Thu, Jul 23, 2015 at 7:35 AM, 'vincent beauseigneur' via
ceylon-users <ceylon...@googlegroups.com> wrote:

> In all way, the last curry error (even if it should fail) isn't well formed.

In Ceylon 1.2, the error I get is:

Argument must be assignable to parameter f of curry:

Anything(*<[Nothing]&Nothing[2]>) (Anything(*Nothing)) is not
assignable to Anything(Anything, Anything*)


Which looks quite correct to me. Anything(*Nothing) is not a subtype
of Anything(Anything, Anything*). That's clear, isn't it?

So I assume you ran into an already-fixed bug in Ceylon 1.1.

[Gavin King]

On Thu, Jul 23, 2015 at 7:35 AM, 'vincent beauseigneur' via
ceylon-users <ceylon...@googlegroups.com> wrote:

> I didn't find where spread operator
> could be used for type (by reading it, I don't understand difference with
> undetermined number of parameters).

That's allowed in Ceylon 1.2.

R(*Args) means Callable<R,Args>

> Isn't Anything(Nothing) quite equals to Callable<Anything, Tuple<Nothing,
> Nothing, []>> ?

Yes, that's right.

> Then I just develop as in contravariant Consumer<A>|Consumer<B> <=>
> Consumer<A&B>, probably I have misunderstood here (does it work only if A
> and B are not disjoint ?, this could make sense, what the hell could union
> be impossible)
>
> Then how do I write my code :
> In a matter of fact I started from there, so :
> Callable<Anything, [Nothing]>|Callable<Anything, [Nothing,Nothing]> <=>
> Callable<Anything | Anything, [Nothing] & [Nothing, Nothing]>

Wait, wait, wait. What do you mean by "<=>" here? These types are not equal.

Be careful: Anything(Nothing)|Anything(Nothing,Nothing) is a subtype
of Anything(*Nothing), but the converse is not true.

> then I go on Tuple form :
> <=> Callable <Anything, Tuple<Nothing, Nothing, [] & [Nothing]>

Fully expanding the type

Anything(*[Nothing] & [Nothing, Nothing])

Gives me:

Callable<Anything, Tuple<Nothing,Nothing,Empty> &

Tuple<Nothing,Nothing,Tuple<Nothing,Nothing,Empty>>>

Now, let's consider the type Tuple<Nothing,Nothing,Empty> &
Tuple<Nothing,Nothing,Tuple<Nothing,Nothing,Empty>:

- it's actually just Nothing, since these types are disjoint, but,
ignoring that for a second,
- it's also a subtype of Tuple<Nothing,Nothing,Empty &
Tuple<Nothing,Nothing,Empty>>, which
- is just the type Tuple<Nothing,Nothing,Nothing>

Now, since Callable is *contravariant* in its second type parameter,
that means that

Anything(*[Nothing] & [Nothing, Nothing])

is a *supertype* of Anything(*Tuple<Nothing,Nothing,Nothing>).

Not a *subtype*. Perhaps you got tripped up by contravariance here?

So what we see is that both the following types:

Anything(*Tuple<Nothing,Nothing,Nothing>)
Anything(Nothing)|Anything(Nothing,Nothing)

Are subtypes of

Anything(*Nothing)

But neither is a supertype of this type.

Is that better?

> When I first wrote this lines I didn't directly see that [] & [Nothing] <=>
> Nothing, then my tests.
> well this means that [Nothing]&[Nothing,Nothing] in tuple form quite equals
> Tuple<Nothing, Nothing, Nothing> which differs from Tuple<Nothing, Nothing,
> Nothing[]> ([Nothing+]).
>
> thx for reading
>

> --
> You received this message because you are subscribed to the Google Groups
> "ceylon-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ceylon-users...@googlegroups.com.
> To post to this group, send email to ceylon...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ceylon-users.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/ceylon-users/074b0fb7-f704-45b8-9fa9-cf48222b845c%40googlegroups.com.

>
> For more options, visit https://groups.google.com/d/optout.

[Gavin King]

On Thu, Jul 23, 2015 at 9:36 AM, Gavin King <gavin...@gmail.com> wrote:

> Now, let's consider the type Tuple<Nothing,Nothing,Empty> &
> Tuple<Nothing,Nothing,Tuple<Nothing,Nothing,Empty>:
>
> - it's actually just Nothing, since these types are disjoint, but,
> ignoring that for a second,
> - it's also a subtype of Tuple<Nothing,Nothing,Empty &
> Tuple<Nothing,Nothing,Empty>>, which
> - is just the type Tuple<Nothing,Nothing,Nothing>
>
> Now, since Callable is *contravariant* in its second type parameter,
> that means that
>
> Anything(*[Nothing] & [Nothing, Nothing])
>
> is a *supertype* of Anything(*Tuple<Nothing,Nothing,Nothing>).
>
> Not a *subtype*. Perhaps you got tripped up by contravariance here?

Oooops, apologies, sorry, that's rubbish, indeed

Tuple<Nothing,Nothing,Empty> &
Tuple<Nothing,Nothing,Tuple<Nothing,Nothing,Empty>

is *exactly* the type Tuple<Nothing,Nothing,Nothing>, according to the
principal instantiation inheritance restriction, so indeed

Anything(*Nothing)

is the exact same type as:

Anything(*Tuple<Nothing,Nothing,Nothing>)

And the typechecker doesn't seem to recognize that, which is indeed a
bug, I suppose.

So it looks like it's actually a bug in the spec §3.4.4, which
implicitly assumes that types like Sequential<Nothing> or
Tuple<X,Nothing,Y> are empty. But nowhere does the spec or typechecker
actually introduce that rule.

[Gavin King]

https://github.com/ceylon/ceylon-spec/issues/1387

[vincent beauseigneur]

I finally get the update from the 21/07 which corrects the alias bug.

I try with intersection and find this :
Anything(Nothing) & Anything(Nothing, Nothing) should be a supertype of Callable<Anything, [Nothing] | [Nothing, Nothing]> but I can set each form to the other.

The first form should be the supertype.

if a Tuple<X,Nothing,Y> is empty, this makes sense in covariant or instanciable use, but in contravariant how will you type Anything(Nothing, Nothing) ?

[Gavin King]

OK, you win. I have fixed #1387, and your original code now compiles :-)

I will update the Ceylon spec to add these additional typing rules.

[vincent beauseigneur]

I don't mind to win if I was wrong. this time I took my time to be sure I do not mistake.

If you consider Tuple<X,Nothing,Y> is Nothing (as a matter of fact you cannot instantiate it) then you cannot represent supertype of function with determined number of parameter you transform all Anything(Nothing, Nothing), Anything(Nothing) into Anything(Nothing*).

The only way then to represent it then it's to union all Anything(*X) where X get over all end subtype which are not Nothing class.

Sorry, if my thoughts mislead you.

my last thought was that we cannot specifically represents functions with varargs. They are functions with zero AND one AND two parameters AND  ...

They are subtype of all functions with determined number of parameter (considering their return and param type). I do not find any use case, it is only thoughts. 

[Gavin King]

Alright, so this is fascinating.

To recap the source of all this: it's convenient to be able to
consider, say, [Integer] and [Float] as disjoint, allowing you to
write, for example:

[Integer]|[Float] num;
switch (num)
case (is [Integer]) { ... }
case (is [Float]) { ... }

That's already a bit useful, but it gets even more useful in cases
like [Integer]|[Integer,Float], etc.

Previously the way the spec handled this was to declare that if X and
Y are disjoint, then [X] and [Y] are disjoint (approximately speaking,
you can check the spec for the real definition). The justification for
this is that it's impossible to instantiate [Nothing], so there can be
no singleton which is simultaneously an [X] and a [Y].

Now, by the same reasoning [Nothing], which has no instances, should
actually be considered the same type as Nothing. Indeed we can prove
this: if I have disjoint X, and Y, then I can form the type [X]&[Y],
which is a the same type as [X&Y], due to principal instantiation
inheritance, which is the type [Nothing], since [X] and [Y] are
disjoint. Furthermore, we've just asserted that [X]&[Y] is also the
type Nothing, so [Nothing]==Nothing.

But the spec never addressed this identity, I never noticed it, and
the typechecker never implemented it. Furthermore - and this is a bit
embarrassing - this missing identity undermines some reasoning about
instantiations, breaking transitivity, as discovered by Vincent.

So I spent all yesterday trying to incorporate this identity into the
typechecker. I have a couple of *working* implementations, but
unfortunately the performance impact is terrible, so I'm still
struggling with this to make it perform.

Now Vincent points out a different potential problem. That now these
two functions have the same type:

void f(Nothing n)
void g(Nothing n, Nothing m)

Their types are Anything(Nothing) and Anything(Nothing,Nothing)
respectively, which according to this new identity are both equivalent
to Anything(*Nothing).

Now, it's not actually at all clear that this is really a problem. If
I have a Anything(Nothing) or a Anything(Nothing,Nothing), I can never
actually in practice form an argument list which would let me call the
function.

Currently I could *write*:

value ff = f;
value gg = g;
ff(nothing);
gg(nothing,nothing);

But of course *at runtime* neither f nor g would ever be invoked. So
in fact it's *actually not wrong* to consider Anything(Nothing) and
Anything(*Nothing) to be the same type. In both cases it's clear that
what I have is a function reference that I can never produce an
argument tuple for.

But yeah, a side-effect is that there is no longer a supertype of "all
functions which accept one parameter" or "all functions which accept
two parameters". So the question is: are those types useful?

Does anyone use them anywhere?

[Stephane Epardaud]

I don't understand how it's limited to tuples, is it somehow a special case because they're final?

http://seamframework.org

--
You received this message because you are subscribed to the Google Groups "ceylon-users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-users...@googlegroups.com.
To post to this group, send email to ceylon...@googlegroups.com.
Visit this group at http://groups.google.com/group/ceylon-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/CAP7PoCdjvVM3euiLsbhmqxtu2LyNXcr%2BGygocSF3wM1MVKX4VQ%40mail.gmail.com.

For more options, visit https://groups.google.com/d/optout.

--

Stéphane Épardaud

[Tako Schotanus]

On Fri, Jul 24, 2015 at 12:19 PM, Gavin King <gavin...@gmail.com> wrote:

But yeah, a side-effect is that there is no longer a supertype of "all
functions which accept one parameter" or "all functions which accept
two parameters". So the question is: are those types useful?

So if I understand correctly this would mean you can't have a type for functions of a specific number of unknown parameters, but you could still have one for any function having any number of unknown parameters, right?

The only uses I can imagine all need some kind of runtime type handling to do anything useful (calling a 1-parameter function without knowing what to do with its parameter doesn't seem very plausible).

I have no doubt someone can (and will) come up with a use-case, but I don't think it's a great loss of functionality (we're not making certain things impossible or much harder to do all of a sudden).

But I'm no type-system expert, so I'm sure there are some that will disagree. ;)

-Tako

[Gavin King]

Tuples and other sequences. It's a special case because they're
sealed/final in the language module.

> https://groups.google.com/d/msgid/ceylon-users/CAKU9E9vTMzzow2GtcWuu61R05Y%2B8EvdGsz4SkyEcy0%3DGaq5XAg%40mail.gmail.com.

> For more options, visit https://groups.google.com/d/optout.



--

[vincent beauseigneur]

Saying that Anything(Nothing) and Anything(Nothing, Nothing) are the same as Anything(Nothing*) implies :

that all functions have supertype Anything();

you can check it with replacing Anything with Integer : which then Integer() is a supertype of all functions returning Integer;

so all =, *, + in type definition will be useless.

As I point in 1387 (well I use a pseudo there, i will there too), for me it is more a problem in the initial definition.

Anything(Nothing) <=> Callable<Anything, in Tuple<out, out, out>>

This problem is in tuple with the rest type.

[Gavin King]

On Fri, Jul 24, 2015 at 1:55 PM, 'vincent beauseigneur' via
ceylon-users <ceylon...@googlegroups.com> wrote:
> Saying that Anything(Nothing) and Anything(Nothing, Nothing) are the same as
> Anything(Nothing*) implies :

No, that's not right. Anything() means Callable<Anything,Empty> which
is not a supertype of Callable<Anything,Nothing>.

[Stephane Epardaud]

Wouldn't the same reasoning apply to every generic type with `Nothing` as a type argument then? I don't see why it's so special. There are also no instances of `Box<Nothing>` for example:

final shared class Box<T>(shared T t){

}

--
You received this message because you are subscribed to the Google Groups "ceylon-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-users...@googlegroups.com.
To post to this group, send email to ceylon...@googlegroups.com.
Visit this group at http://groups.google.com/group/ceylon-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/CAP7PoCfFy02N30t%2B_7MsaZ%3DYdt%2BUEYQ3yb87X46%2Bj868U5knNg%40mail.gmail.com.

For more options, visit https://groups.google.com/d/optout.

--

Stéphane Épardaud

[Lucas Werkmeister]

final shared class Box<T>() {
    // I lied, not actually a box
}

Nothing¹ stops me from creating a Box<Nothing>(). In fact, we have an example of this in the language module: Empty is a Sequential<Nothing>. (The reasoning only applies to nonempty Sequences.)

¹ no pun intended

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/CAKU9E9sjdJh_r94T%3DOhcDMQ-gbXGq8vE%3DnfBGHj7ys6m8vDt_Q%40mail.gmail.com.

[Stephane Epardaud]

So if it's super special, can't ever be generalised outside of non-empty sequences, and has weird/unintuitive consequences, why are we adding this special case then?

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/55B22E8B.5010308%40googlemail.com.

For more options, visit https://groups.google.com/d/optout.

--

Stéphane Épardaud

[Gavin King]

> Wouldn't the same reasoning apply to every generic type with `Nothing` as a type argument then?

No, consider Empty, which is a `Sequential<Nothing>`. But it does, in
principle, apply to every generic class of form "class Box<T>(T t)"
where T appears in the parameter list.

> https://groups.google.com/d/msgid/ceylon-users/CAKU9E9sjdJh_r94T%3DOhcDMQ-gbXGq8vE%3DnfBGHj7ys6m8vDt_Q%40mail.gmail.com.

>
> For more options, visit https://groups.google.com/d/optout.



--

[Gavin King]

On Fri, Jul 24, 2015 at 2:33 PM, Stephane Epardaud
<stephane...@gmail.com> wrote:
> can't ever be generalised outside of non-empty
> sequences, and has weird/unintuitive consequences, why are we adding this
> special case then?

Well there are potential generalizations of this, though I have not
tried to formalize them.

The motivation is that switching over disjoint tuple types is
impossible without this.

Well, OK, sure, I could add some special warty special-casey reasoning
to the code that checks disjointness of switch branches, but that
seems much worse.

[Stephane Epardaud]

I don't see why it'd be worse. It seems about as arbitrary, with none of the side-effects ;)

http://seamframework.org

--
You received this message because you are subscribed to the Google Groups "ceylon-users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-users...@googlegroups.com.
To post to this group, send email to ceylon...@googlegroups.com.
Visit this group at http://groups.google.com/group/ceylon-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/CAP7PoCe_uXw-32zU2VGwGRxKB4xYs4dgL3OK8E67px7GRwzO_A%40mail.gmail.com.

For more options, visit https://groups.google.com/d/optout.

--

Stéphane Épardaud

[Gavin King]

Well the "side-effects" here are actually *correct*, in some cases
*useful*, even though some of them are surprising.

On Fri, Jul 24, 2015 at 2:53 PM, Stephane Epardaud

> https://groups.google.com/d/msgid/ceylon-users/CAKU9E9sdbpLFs9pQKKkbJdE7DrtPqpV3kp3zq8V1%3DH3muvwjSQ%40mail.gmail.com.

>
> For more options, visit https://groups.google.com/d/optout.



--

[Stephane Epardaud]

But they don't apply to every type similar to `Sequence` (which is even more special since that one is an interface and so we can't derive this behaviour from its parameter list), so it's still super special-casy, and it applies everywhere. Special-casing the switch OTOH only affects that.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/CAP7PoCeOhUHe4xSKB-REP%3DPTQq3P%2B4-LUDN%3DFdNhhWwOdZdPew%40mail.gmail.com.

For more options, visit https://groups.google.com/d/optout.

--

Stéphane Épardaud

[Gavin King]

Sure but special-casing switch isn't as *useful*. It's very nice that
the typesystem will now warn me that [Integer] & [String] is an empty
type.


If I write:

[Integer] int = ... ;
if (is [String] int) { ... }

I get a warning from the compiler.



On Fri, Jul 24, 2015 at 2:59 PM, Stephane Epardaud

> https://groups.google.com/d/msgid/ceylon-users/CAKU9E9uYvfs%3D1gcS5AGB%2BTf05ZrFgWmxKf2FKpE5QEoHaeEfAg%40mail.gmail.com.

[Stephane Epardaud]

Except people will want it for other types.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/CAP7PoCeY9Kmkad4sGMvZhDqw0AimeqZf6dP_0crOpscx1yAgMQ%40mail.gmail.com.

For more options, visit https://groups.google.com/d/optout.

--

Stéphane Épardaud

[Gavin King]

Well if and when they ask for it, we can investigate that.

On Fri, Jul 24, 2015 at 3:11 PM, Stephane Epardaud

> https://groups.google.com/d/msgid/ceylon-users/CAKU9E9uQpP6EvXQsevhHKXdc34Tf42XwW71Y%2BSMOMj1vXBwtpA%40mail.gmail.com.

[vincent beauseigneur]

On 24 July 2015 at 14:15, Gavin King <gavin...@gmail.com> wrote:

On Fri, Jul 24, 2015 at 1:55 PM, 'vincent beauseigneur' via
ceylon-users <ceylon...@googlegroups.com> wrote:
> Saying that Anything(Nothing) and Anything(Nothing, Nothing) are the same as
> Anything(Nothing*) implies :

No, that's not right. Anything() means Callable<Anything,Empty> which
is not a supertype of Callable<Anything,Nothing>.

in fact, [Nothing] & [Nothing, Nothing] are all sequentials so the result is sequential.

if we transpose in a mathematical issue the intersection between a line and a plan if the line is in the plan (Nothing is in Nothing) it is the line [Nothing]

if we intersect [] with [Nothing] the result is always [].

In the spec it is also specified that we can have a function type like String(Integer, Integer=) where Integer= is represented as in canonical [] | [Integer].

all this three could are contained in this type :

String (Integer) A;

String (Integer, Integer) B;

String (Integer, Integer) C = (Integer x, Integer y = 5) => (x+y).string; // implicit included in the union

if you canonize them

you have

Callable<String, [Integer]> | Callable<String, [Integer, Integer]> where as Integer= is defined, might be included in

Callable<String, [Integer] | [Integer, Integer]> BUT as it is covariant it is false

but actually it is included in

Callable<String, [Integer] & [Integer, Integer]>

for all agrees, we should have Arguments variant and Type still covariant, something like this :

Callable<out Return, out Arguments> given Arguments satisfies ArgTuple<in Arg>

As we have a special tuple implementation, we can avoid specialized return type.

[Gavin King]

On Fri, Jul 24, 2015 at 3:15 PM, vincent beauseigneur
<vbeaus...@yahoo.fr> wrote:
>
> On 24 July 2015 at 14:15, Gavin King <gavin...@gmail.com> wrote:
>>
>> On Fri, Jul 24, 2015 at 1:55 PM, 'vincent beauseigneur' via
>> ceylon-users <ceylon...@googlegroups.com> wrote:
>> > Saying that Anything(Nothing) and Anything(Nothing, Nothing) are the
>> > same as
>> > Anything(Nothing*) implies :
>>
>> No, that's not right. Anything() means Callable<Anything,Empty> which
>> is not a supertype of Callable<Anything,Nothing>.
>>
> in fact, [Nothing] & [Nothing, Nothing] are all sequentials so the result is
> sequential.
> if we transpose in a mathematical issue the intersection between a line and
> a plan if the line is in the plan (Nothing is in Nothing) it is the line
> [Nothing]
> if we intersect [] with [Nothing] the result is always [].

Nonononono.

[Nothing,Nothing] is not the type of any point! The type of a point is
[Float,Float], which is *not* an instance of [Nothing,Nothing]!


The whole issue here is that *there simply are no instances of*
[Nothing] or of [Nothing,Nothing]. Those type expressions don't really
represent anything very meaningful.

> In the spec it is also specified that we can have a function type like
> String(Integer, Integer=) where Integer= is represented as in canonical [] |
> [Integer].
>
> all this three could are contained in this type :
> String (Integer) A;
> String (Integer, Integer) B;
> String (Integer, Integer) C = (Integer x, Integer y = 5) => (x+y).string; //
> implicit included in the union
>
> if you canonize them
> you have
> Callable<String, [Integer]> | Callable<String, [Integer, Integer]> where as
> Integer= is defined, might be included in
> Callable<String, [Integer] | [Integer, Integer]> BUT as it is covariant it
> is false
>
> but actually it is included in
> Callable<String, [Integer] & [Integer, Integer]>

Well String(*[Integer]&[Integer,Integer]) is just a way to write
String(*Nothing).

So any function that returns String is a subtype of this type.

And, sure, String(*Tuple<Integer,Integer,[]|[Integer]>) is clearly a
subtype of this type.

Nothing wrong there.

> for all agrees, we should have Arguments variant and Type still covariant,
> something like this :
> Callable<out Return, out Arguments> given Arguments satisfies ArgTuple<in
> Arg>

No, that can't possibly be right; that would be saying that the
function (String x)=>x is an instance of String(Object) and can
therefore be invoked with an Integer argument.

[vincent beauseigneur]

> [Nothing,Nothing] is not the type of any point! The type of a point is
> [Float,Float], which is *not* an instance of [Nothing,Nothing]!

yeah you are right, but we found [Nothing, Nothing] in contravariant (where come all the problem)

so [Nothing, Nothing] is 'instance' of [Float, Float]

> Well String(*[Integer]&[Integer,Integer]) is just a way to write
> String(*Nothing).
>
> So any function that returns String is a subtype of this type.
>
> And, sure, String(*Tuple<Integer,Integer,[]|[Integer]>) is clearly a
>subtype of this type.
>
>Nothing wrong there.

Actually you'r right, and that is exactly where the problem is. You can not define String(Integer), as it is a way to write String(*Nothing).

Then you have to create an interface for specifying a function with a parameter ? that is really what you want ?

> > for all agrees, we should have Arguments variant and Type still covariant,
> > something like this :
> > Callable<out Return, out Arguments> given Arguments satisfies ArgTuple<in
> > Arg>
>
> No, that can't possibly be right; that would be saying that the
> function (String x)=>x is an instance of String(Object) and can
> therefore be invoked with an Integer argument.

sorry I meaned Arguments covariant and Type still contravariant.

if Type is contravariant, this works well. (ArgTuple<in>)

And quite to have new ArgTuple you even can describe default argument with OptionalArgTuple and VarArgsSequential (does not confuse with ArgsSequential)

[Gavin King]

On Fri, Jul 24, 2015 at 4:35 PM, vincent beauseigneur
<vbeaus...@yahoo.fr> wrote:
> so [Nothing, Nothing] is 'instance' of [Float, Float]

Well, strictly speaking, [Nothing,Nothing] is a *subtype* of
[Float,Float], but it's not an *instance* of anything, since it has no
instances!

Similarly, Nothing is a subtype of Float, of [Float], and of
[Float,Float], but quite clearly it's not an *instance* of any of
these types :-)

> Actually you'r right, and that is exactly where the problem is. You can not
> define String(Integer), as it is a way to write String(*Nothing).

No. That's not correct. String(Integer) and String(*Nothing) are
distinct types. String(Integer) is a *subtype* of String(*Nothing),
but it is not the same type.

We've defined that [Nothing] is Nothing.

We have most certainly *not* specified that [Integer] is Nothing! I
can prove it's not Nothing by writing [0], which executes and produces
a value.

> sorry I meaned Arguments covariant and Type still contravariant.

No, that's what I'm saying: it's completely incorrect for Arguments to
be covariant. If it were covariant, then String(Integer) would be a
subtype of String(Object), meaning that you could call a
String(Integer) by passing it a String. That's just not right.

[vincent beauseigneur]

> Well, strictly speaking, [Nothing,Nothing] is a *subtype* of
> [Float,Float], but it's not an *instance* of anything, since it has no
> instances!
>
> Similarly, Nothing is a subtype of Float, of [Float], and of
> [Float,Float], but quite clearly it's not an *instance* of any of

> these types :-)

That's why I used quote. But the need here really to have subtype of [Float, Float] not super type.

> No. That's not correct. String(Integer) and String(*Nothing) are
> distinct types. String(Integer) is a *subtype* of String(*Nothing),
> but it is not the same type.
>
> We've defined that [Nothing] is Nothing.
>
> We have most certainly *not* specified that [Integer] is Nothing! I
> can prove it's not Nothing by writing [0], which executes and produces
> a value.

The proof that [Nothing] is Nothing, this comes only from the assertion [Nothing] & [] is Nothing

and I was wrong here it is []. the same could be done with Integer ([Integer] & [] is []) so let's go as you seems needing to see it :

`String() | String(Integer)

Callable<String, []> | Callable<String, [Integer]>`

which is included in:

`Callable<String, [Integer] & [] >>`

which equals `Callable<String, []> which is String()`

well String(Integer) is of type String() ?

this assertion has no real reason to be.

> > sorry I meaned Arguments covariant and Type still contravariant.
>

> No, that's what I'm saying: it's completely incorrect for Arguments to
> be covariant. If it were covariant, then String(Integer) would be a
> subtype of String(Object), meaning that you could call a
> String(Integer) by passing it a String. That's just not right.

if type is contravariant you could always write Anything(Object) as a supertype !

see this is supertype of mine version :

Callable<Anything, ArgTuple<Nothing>>

as ArgTuple is here annotated out, we can use its own supertype ArgTuple<Nothing> as type is contravariant.

[vincent beauseigneur]

too help, a covariant type does not change the variant of the type. a contravariant change the variant.

well, I am not sure it means something so :

with `A<out B>`

we have `A<Anything> c A<Integer> c A<Nothing>` where c means contains

with `C<in D>`

we have `C<Nothing> c C<Integer> c C<Anything>` where c means contains

then

`A<C<Nothing>> c A<C<Integer>> c A<C<Anything>>`

as you see with A is Callable<out, out> and C is ArgType<in>

you have

`Callable<Anything, ArgType<Nothing>> c Callable<String, ArgType<Integer>> c Callable<Nothing, ArgType<Anything>>`

[Ross Tate]

Can I ask a historical question? What prompted the need for [Integer] and [String] to be disjoint? That is, what real world program was someone writing that called for recognizing this property?

Thanks.

P.S. I can formalize a general-purpose version of this for y'all if you'd like, but I'd first like to know why it's happening.

--
You received this message because you are subscribed to the Google Groups "ceylon-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ceylon-users...@googlegroups.com.
To post to this group, send email to ceylon...@googlegroups.com.
Visit this group at http://groups.google.com/group/ceylon-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ceylon-users/78c9fcb3-4100-408d-8707-47f3c58b148d%40googlegroups.com.

[Gavin King]

On Fri, Jul 24, 2015 at 5:12 PM, vincent beauseigneur
<vbeaus...@yahoo.fr> wrote:

> The proof that [Nothing] is Nothing, this comes only from the assertion
> [Nothing] & [] is Nothing

Wait, wait, wait. [] i.e. Empty and [Nothing] have *always* been
disjoint types, since tuple descends from Sequence, and Empty and
Sequence are the two disjoint cases of the enumerated type Sequential.

[Nothing] & [] == Nothing

Has always been true in all versions of Ceylon.

> `String() | String(Integer)
> Callable<String, []> | Callable<String, [Integer]>`
> which is included in:
> `Callable<String, [Integer] & [] >>`
> which equals `Callable<String, []> which is String()`
> well String(Integer) is of type String() ?
> this assertion has no real reason to be.

No, that's not correct. It's true that

Callable<String, []> | Callable<String, [Integer]>

has the principal instantiation

Callable<String, [] & [Integer]>

But this type is:

Callable<String, Nothing> i.e. String(*Nothing)

NOT NOT NOT:

Callable<String, []> i.e. String()

[] means Empty. It does not mean Nothing!

Empty and Nothing are totally distinct types!

[Gavin King]

As I said above: the ability to use a tuple type as the branch of a
switch. If tuple types aren't disjoint, they can never be used as a
switch case.

[vincent beauseigneur]

> No, that's not correct. It's true that
>
>    Callable<String, []> | Callable<String, [Integer]>
>
> has the principal instantiation
>
>    Callable<String, [] & [Integer]>
>
> But this type is:
>
>    Callable<String, Nothing> i.e. String(*Nothing)

well then I can do it with String(Integer) | String(Integer, Integer)  

when canonalized you got

String(Integer, *Nothing) which is quite equals to String(*Nothing) as only the first parameter is defined.

Then you cannot get what you expect i.e. :

String(Integer, Integer=)

With Callable<out, out> and ArgTuple<in>

you got that directly (well I use the same sugar as tuple but this corresponds to ArgTuple):

Callable<String, [Integer]> | Callable<String, [Integer, Integer]>

this results contains previous line, which is expected

Callable<String, [Integer] | [Integer, Integer]>

Callable<String, ArgTuple<Integer> >

OK There ArgTuple does not specify chained type

well for this to work you can add ArgTuple<in, out>, where out is only the type of the next ArgTuple

here we cannot do have ArgTuple<out, in, out> due to inheritance aspect (or you set the first always to Anything).

Callable<String, ArgTuple<Integer, [] | ArgTuple<Integer, []>>;

Actually it is not consistent  (there sugar is for Tuple and Callable<out,in>):

Callable<String, [Integer] & [Integer, Integer]> does not contains Callable<String, [Integer] | [Integer, Integer=]> (it is the opposite by definition)

if you get in spacial form you will see that [Integer] & [Integer, Integer] is [Integer] (a plan is in space, the intersection is a plan)

yeah [Float] & [Integer, Integer] is contained Nothing  (the opposite we can discuss but there is not the problem)

When you write Callable<String, [Float]> | Callable<String,[Integer, Integer]>

with Callable<out, out> we got :

Callable<String, [Float] | [Integer, Integer]>

Callable<String, ArgTuple<Float & Integer, [Integer=]> > alias String(Nothing, Integer =) which is naturally expected.

with actual form Callable<out, in> we got:

Callable<String, [Float] & [Integer, Integer]> alias String(*Nothing)

I will try make proof that [Integer] & [] is []. as in fact it is easy to say that something is Nothing (it is so often true), and undiscutable.

[Gavin King]

On Fri, Jul 24, 2015 at 6:58 PM, vincent beauseigneur
<vbeaus...@yahoo.fr> wrote:

> well then I can do it with String(Integer) | String(Integer, Integer)
> when canonalized you got
> String(Integer, *Nothing) which is quite equals to String(*Nothing) as only
> the first parameter is defined.

No, not quite:

String(Integer) | String(Integer, Integer)

has the principal supertype

String(*[Integer]&[Integer,Integer])

Which, as usual for all these types, is:

String(*Nothing)

Which is perfectly correct. There is no argument tuple that I can form
within the language which I can correctly pass to a function reference
of type:

String(Integer) | String(Integer, Integer)

This type means I might have a function with one parameters or I might
have a function with two parameters. If I try to pass two arguments,
that could be an error. Likewise if I try to pass one argument that
could be an error. Hence String(*Nothing), since it's impossible to
form an argument tuple.

(It's rather sweet that Ceylon's typesystem is capable of the above
reasoning, FTR.)

> Then you cannot get what you expect i.e. :
> String(Integer, Integer=)

No no no, that wouldn't be the correct type at all! That type says I
have a function that accepts either one or two arguments. That's
simply not what String(Integer) | String(Integer, Integer) says!

That's perhaps the source of all your confusion: you're identifying
String(Integer) | String(Integer, Integer) with String(Integer,
Integer=) but they're quite, quite different!

[vincent beauseigneur]

By searching completely for my deal, I may have found a way for Callable<out, in> (I let you check).

> That's perhaps the source of all your confusion: you're identifying
> String(Integer) | String(Integer, Integer) with String(Integer,

> nteger=) but they're quite, quite different!

well, sorry about that.

so we have String(Integer, Integer=) is subtype of String(Integer) | String(Integer, Integer) not supertype,

>    String(Integer) | String(Integer, Integer)
>
> This type means I might have a function with one parameters or I might
> have a function with two parameters. If I try to pass two arguments,
> that could be an error. Likewise if I try to pass one argument that
> could be an error. Hence String(*Nothing), since it's impossible to
> form an argument tuple.

> well then in my case I should have :

> OptionalArgTuple<in X, EmptyArg> which satisfies ArgTuple<X, EmptyArg> & EmptyArg which satisfies ArgTuple<Nothing, EmptyArg>

Yes I know, but as I said functions like curry would be very happy with this. 

Callable<String, ArgTuple<Integer, OptionalArgTuple<Integer, EmptyArgs>>

which should be subtype of

Callable<String, ArgTuple<Integer, EmptyArgs>> as OptionalArgTuple satisfies EmptyArg (notation []) all is good.

Callable<String, ArgTuple<Integer, ArgTuple<Integer, EmptyArg>> as OptionalArgTuple satisfies ArgTuple<Integer, EmptyArg> it also works.

if I miss nothing, I am able to take all possibilities (well with optional at the end as currently) :

String(Integer) | String(Integer, Integer) => Callable<String, ArgTuple<Integer, [] & ArgTuple<Integer, []>> 

String(Integer, Integer=) => Callable<String, ArgTuple<Integer, OptionalArgTuple<Integer, []>>

with special case that [Integer] & [] is [Integer] (used for optional)

take care then that String(Integer) & String(Integer, Integer) should be considered as String(Integer, Integer=)

With Callable<out, in> case probably there is quite the same trick to achieve this with using another Tuple type

by having something like this Tuple<out X, > which satisfies EmptyArg which satisfies Mandatory<out, > (I may have fail on naming it is perhaps the same above)

then [] means totally something else and there can admit [] & [Integer] is [];

Sorry, for this I let you test it, and determine what is the best.

take care then that String(Integer) | String(Integer, Integer) should be considered with a mandatory field.

as there is already special cases (=, *...) for optional Args, it seems to me that the first is more readable (you have one or two parameters, you have optional parameter).

With such classes Ceylon could really manage all sorts of Callable.

well let me show you that [] & [Integer] is (or could be) [] :

they all Ranged<out, out, in>, and as a matter of fact you didn't say that Ranged<Integer, X, Nothing> is nothing.

we have :

`Ranged<Integer, Nothing, []> & Ranged<Integer, A, [A]>

Ranged<Integer, A, [] & [A]>`

then if we admit that [] & [Integer] is Nothing
we admit also that
Ranged<Integer, A, Nothing> is also equivalent to Nothing as the Subrange is Nothing. (then may have lots of class which draw to Nothing)
on the contrary
Ranged<Integer, A, []>
only means []. then [] & [Integer] is a subrange of [].

I could not totally proof that [] & [Integer] is not only Nothing, but I proof that if is that so number of Class will become Nothing in some case, it is always possible to set to Nothing.

[vincent beauseigneur]

please instead of

> > well then in my case I should have :

> > OptionalArgTuple<in X, EmptyArg> which satisfies ArgTuple<X, EmptyArg> & EmptyArg which satisfies ArgTuple<Nothing, EmptyArg>

> Yes I know, but as I said functions like curry would be very happy with this. 

read this

Yes I know, but as I said functions like curry would be very happy with this. 

well then in my case I should have :

OptionalArgTuple<in X, EmptyArg> which satisfies ArgTuple<X, EmptyArg> & EmptyArg which satisfies ArgTuple<Nothing, EmptyArg>

[John Vasileff]

> On Jul 24, 2015, at 6:19 AM, Gavin King <gavin...@gmail.com> wrote:
>
>
> But yeah, a side-effect is that there is no longer a supertype of "all
> functions which accept one parameter" or "all functions which accept
> two parameters". So the question is: are those types useful?
>
> Does anyone use them anywhere?
>

I’m not ready to concede at all that it’s worthless to keep around, have knowledge of, or test for *partial* type information about a functions parameters.

But also, I think the area of concern is much more general, as this seems to affect *all* contravariant uses of Tuples.

John

[vincent beauseigneur]

I finally Figure the response : when you ask for one, you could simply do not have the other (even with null value).

[vBeauPer]

When I want to find something, I can go very far.
Well the problem that I pointed is just to find a way to describe supertype of function in an another way than union.
Starting from ceylon site that where Anything(Nothing) is supertype of function with one parameter
This conducts to specify that they are only Anything(*X, *Nothing) where X[], and each type in X[] are not Nothing. and *Nothing an unspecified number and type of parameter, and to specify that [Nothing] is Nothing.
so Anything(Integer, *Nothing) is supertype of all functions with at least one Integer parameter. for other supertype unions of function works well.
Actually it is difficult to work with a compile time typed Anything(Integer, *Nothing), transforming it with curry (for example) return an Anything(*Nothing)(Integer), strictly typed as is, so you cannot get back to a really Callable function.
In order to have better behaviour meta could permits you to call that function but you have to know what are the parameter number and type, for better only native trick.
But are function supertypes really needed ? (then you could call one with 'is' statement to retrieve your transformed function)
There are a usage for a List<Anything(Nothing)> here http://ceylon-lang.org/blog/2015/04/19/observable/

In the way, I was so concentrate on the canonical form that I lost that [] & [Integer] is Nothing.(you cannot have [] in an [Integer] variable)

The form that I described seems to fill all the needed description, but does not change the usage you can do with it.