Proposal: Negation Type

[soundlogic2236]

Disjoint types are supported by the compiler, but the only way to explicitly specify them is via a shared enumerated interface of both types. I propose a 'negation type', the notation I shall use for this will be that for any type T there exists a type !T, though alternative notations are of course reasonable. The following identities hold true:

1. T|!T covers Anything
2. T&!T is Nothing

The primary use cases I see for this are as follows:

Specifying type disjointness without a shared interface

interface Foo { ... }
abstract class DoesNotWorkWithFoo() satisfies !Foo { ... }

Nothing which satisfies DoesNotWorkWithFoo can satisfy Foo. This would be especially helpful for generic functions where we might want something like:

[T,Null]|[Null,U] strangeSplit<T,U>(T|U val) {
    return switch(val)
    case(is T) [val,null]
    case(is U) [null, val];
}

This doesn't work, since we have no way of saying that T and U should be disjoint. With negation types we could write the following:

[T,Null]|[Null,U] strangeSplit<T,U>(T|U val) given U satisfies !T {
    return switch(val)
    case(is T) [val,null]
    case(is U) [null, val];
}

Better flow typing

While the compiler reasons well in cases like the following:

interface Foo of Bat|Bar|Baz { }
interface Bat satisfies Foo { }
interface Bar satisfies Foo { }
interface Baz satisfies Foo { }

String sayWhatType(Foo obj) {
    if(is Bat obj) {
        return "I'm a bat";
    }
    else {
        switch(obj)
        case(is Bar) { return "I'm a bar"; }
        case(is Baz) { return "I'm a baz"; }
    }
}

correctly reasoning that if obj is a Foo but not a Bat, it must be a Bar or a Baz, if obj is not currently known to be of an enumerated type the information implied by being in the else clause of is simply discarded, meaning the following (admittedly somewhat silly example) does not work

interface MyRoot {}
interface Foo of Bat|Bar|Baz satisfies MyRoot { }
interface Bat satisfies Foo { }
interface Bar satisfies Foo { }
interface Baz satisfies Foo { }

String sayWhatType(MyRoot obj) {
    if(is Bat obj) {
        return "I'm a bat";
    }
    else if (is Foo obj) {
        switch(obj)
        case(is Bar) { return "I'm a bar"; }
        case(is Baz) { return "I'm a baz"; }
    }
    else {
        return "I'm from some non-foo root";
    }
}

With negation types, the compiler could infer even without MyRoot being an enumerated type that in the else clause obj satisfies MyRoot&!Bat, meaning the switch is exhaustive, as Foo&!Bat is covered by Bar|Baz

[RossTate]

I'm pretty sure some of this is doable, and I'm pretty sure some of it is not.

I'm pretty sure that we can have a !Name type (with no type arguments even when Name is generic), and we can determine that Name<...>&!Name is Nothing.

I'm pretty sure that we can't have Name|!Name> cover Anything.

On Fri, Jan 20, 2017 at 7:05 PM soundlogic2236 notifications@github.com wrote:

Disjoint types are supported by the compiler, but the only way to explicitly specify them is via a shared enumerated interface of both types. I propose a 'negation type', the notation I shall use for this will be that for any type T there exists a type !T, though alternative notations are of course reasonable.

The following identities hold true:

1. T|!T covers Anything

2. T&!T is Nothing

The primary use cases I see for this are as follows:

Specifying type disjointness without a shared interface

interface Foo { ... }

abstract class DoesNotWorkWithFoo() satisfies !Foo { ... }

Nothing which satisfies DoesNotWorkWithFoo can satisfy Foo. This would be especially helpful for generic functions where we might want something like:

[T,Null]|[Null,U] strangeSplit<T,U>(T|U val) {

return switch(val)

case(is T) [val,null]

case(is U) [null, val];

}

This doesn't work, since we have no way of saying that T and U should be disjoint. With negation types we could write the following:

[T,Null]|[Null,U] strangeSplit<T,U>(T|U val) given U satisfies !T {

return switch(val)

case(is T) [val,null]

case(is U) [null, val];

}

Better flow typing

While the compiler reasons well in cases like the following:

interface Foo of Bat|Bar|Baz { }

interface Bat satisfies Foo { }

interface Bar satisfies Foo { }

interface Baz satisfies Foo { }

String sayWhatType(Foo obj) {

if(is Bat obj) {

    return "I'm a bat";

}

else {

    switch(obj)

    case(is Bar) { return "I'm a bar"; }

    case(is Baz) { return "I'm a baz"; }

}

}

correctly reasoning that if obj is a Foo but not a Bat, it must be a Bar or a Baz, if obj is not currently known to be of an enumerated type the information implied by being in the else clause of is simply discarded, meaning the following (admittedly somewhat silly example) does not work

interface MyRoot {}

interface Foo of Bat|Bar|Baz satisfies MyRoot { }

interface Bat satisfies Foo { }

interface Bar satisfies Foo { }

interface Baz satisfies Foo { }

String sayWhatType(MyRoot obj) {

if(is Bat obj) {

    return "I'm a bat";

}

else if (is Foo obj) {

    switch(obj)

    case(is Bar) { return "I'm a bar"; }

    case(is Baz) { return "I'm a baz"; }

}

else {

    return "I'm from some non-foo root";

}

}

With negation types, the compiler could infer even without MyRoot being an enumerated type that in the else clause obj satisfies MyRoot&!Bat, meaning the switch is exhaustive, as Foo&!Bat is covered by Bar|Baz

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ceylon/ceylon/issues/6876, or mute the thread https://github.com/notifications/unsubscribe-auth/ABFj2wFLRbaONejKE8-76FqIWC2qfS5Eks5rUUvcgaJpZM4Lp4L2 .

[soundlogic2236]

That is an unexpected reply. Could you clarify both why things like !Iterable<Integer> wouldn't work, and why Type|!Type covering Anything wouldn't work?

[soundlogic2236]

Oh, a shorthand for saying 'exactly one of these types' would also be convenient as that is required for switch statements, but the expressions written out in full become very bulky. Exactly one of T1 and T2 expands out to: <T1&!T2>|<!T1&T2> while exactly one of T1, T2, T3 expands out to <T1&!T2&!T3>|<!T1&T2&!T3>|<!T2&!T1&T3>. This seems error prone and tedious. I am unsure of what notation would be good for this however, It could not be an ordinary operator, as "Exactly one of x, y, and z" is very different from "Exactly one of (Exactly one of x and y) and z" are very different-X&Y&Z is permitted in the latter but not the former. Such a thing could however be done purely as syntactic sugar, without any backend support simply by expanding out into the expanded form.

[gavinking]

@soundlogic2236 The reason Ceylon doesn't have complement types is that @RossTate told me long ago that they introduce undecidability into the type system.

[soundlogic2236]

Huh. That is interesting. I am extremely curious as to how, but am somewhat unsure of what to google. Do you happen to remember why?

[someth2say]

Se already tackled complementary types some years ago (see https://someth2say.wordpress.com/2015/07/12/complementary-types-in-ceylon/ ), and stopped at that same point. I remember Gavin convinced me about the undecidability problems this may drive to, but the details slipped my mind.

[lucaswerkmeister]

It should be noted that the spec already features complement types T~X, defined in §5.4.2 Assignability conditions. However, these are not denotable, reified types; T~X is a type operation that is immediately evaluated, and if there is not enough information about T and X, it is simply T, and the type T~X is discarded and not reevaluated when more information about the types becomes available.

[arseniiv]

Why don’t add disjointness constraint for type parameters instead? (#7259)