Complementary Types in Ceylon

So this is my first post ever…

Maybe you are expecting for me to drop some lines about me, why I started a blog, and so… Sorry, this is not the entry you are looking for. I’ll do that later. I have something in my mind that should go out first.

A week ago, I spent some time in JBCN Conf with some mates. Here I finally found Gaving King, the creator of Hibernate, JBoss Seam, and currently working in Ceylon Language. I have been recently getting into Ceylon Language, and I really feel it like the platonic idea Java should chase. Ceylon does not only  have a lot of interesting features, but also is backed by a powerful company (JBoss), so definitely I want it in my knowledge base.

During Gavin’s speech, while talking about the language, an idea came to my mind. I dropped the question to Gavin, and he responded. But I am not that satisfied with the response.

And that’s what this entry is about.

Union and intersection types:

For those who still does not know about Ceylon, it have a (almost) unique feature that rocket boosts his expressibility; the so called union types  and intersection types. Let’s show an example:

void printTree(Leaf|Branch root) {
    switch (root)
    case (is Leaf) { print(root.item); }
    case (is Branch) {
        printTree(root.left);
        printTree(root.right);
    }
}

In this example, printTree is a function that receive a single tree node (root), whose type is Leaf|Branch (read Leaf or Branch). This is a union type. You can interpret it as “root class inherits from or is Leaf class, or inherits from or is Branch class”. This is really useful for limiting the type of an instance at both compile time and runtime.

Alternatively, you may find intersection types. As you may guess, it is the symmetric type definition. Let’s see another example:

interface Food {
	shared formal void eat();
}
interface Drink {
	shared formal void drink();
}
class Guinness() satisfies Food&Drink {
	shared actual void drink () {}
	shared actual void eat() {}
}
void intersections()
{
	Food&Drink specialStuff = Guinness();
	specialStuff.drink();
	specialStuff.eat();
}

Here, you can see the ‘specialStuff’ Guinnes satisfies both interfaces: Food and Drink. Again, we can rewrite the type of specialStuff to “any class that inherits from or is Food, and inherits from or is Drink”.

Complementary types:

Ok, now we have introduced union and intersection types. Lets go for the question dropped at the JBCNConf:

As Gavin agreed, the type system for Ceylon is based on set theory. As I recall from my student years, there where three main operations to be applied onto sets: union, intersection and complementary.

Then, if Ceylon type system is based in set theory, and it have union types and intersection types… why not having complementary types?

Let’s present complementary types with the same example as I try in JBCNConf: coalesce function.

{Element&Object*} coalesce({Element*} elements) => { for (e in elements) if (exists e) e };

In mortal’s language, coalesce’s contract (ignoring implementation) talks about a function that gets a sequence of Element(s) (having no constraint on their type), and return a sequence of Element&Object. In Ceylon, null is the only instance for Null class, and this class is NOT inheriting from Object class, so Element&Object type does not allow nulls. So we have a contract for a function accepting a sequence of objects of any type, and returns a sequence of objects of a type not accepting nulls.

Top of Ceylon’s type system. Thanks to Renato Athaydes (http://renatoathaydes.github.io/)

This sounds good… but this only works if EVERY possible object is either and Object or a Null. Taking a glimpse of Ceylon’s type hierarchy, we can see that, by default, this is true (Object and Null are the only children for Anything, the root of the type hierarchy). But, as far as I know, there is nothing forbidding creating a new class, and making it inherit directly from the Anything class! In this case, any instance in the input sequence for that new class (in other words, any instance not extending Object class) will also be removed from the list. That’s not the expected behaviour.

But having the complementary types (let’s note it with the ‘bang’ prefix), we can rewrite the coalesce function as follows:

{Element&!Null} coalesce({Element*} elements) => { for (e in elements) if (exists e) e };

This naturally describes the expected behaviour: getting a sequence of Elements of any type, and returning a sequence of those same element, but only retaining the ones whose class is outside Null class hierarchy (say retaining those that are not null).

This is not only more descriptive about the contract for coalesce, but also avoid the ‘unknown hierarchy’ problem: You don’t need to know the whole effective type hierarchy to define the contract, you only need to know what you want, and what you don’t want for the contract.

What is this good for?

We have seen a single use for the complementary type. But a single case is not worth the effort for adding this feature to the language.

We can find any other situations where complementary type may be useful for defining function contract. Let’s the community to find them. But where I find it really useful is not for the developer, but for the type checker.

There is one construction widely used in Ceylon (and many other languajes):type casting. Taking the example directly from Ceylon’s language documentation:

void switchOnEnumTypes(Foo|Bar|Baz var) {
    switch(var)
     // Type for var is Foo|Bar|Baz
    case (is Foo) {
        // Type for var is Foo
        print("FOO");
    }
    case (is Bar) {
        // Type for var is Bar
        print("BAR");
    }
    case (is Baz) {
        // Type for far is Baz
        print("BAZ");
    }
}

This is pretty straightforward when FOO, BAR and BAZ classes are disjoint. But if FOO, BAR and BAZ are interfaces, things may become complicated (mixing inheritance is good for many things, but can make other hard).

But introducing the concept of complementary type, we can rewrite the type-checker thoughts as for the following:

void switchOnEnumTypes(Foo|Bar|Baz var) {
    switch(var)
     // Type for var is Foo|Bar|Baz
    case (is Foo) {
        // Type for var is Foo
        print("FOO");
    }
    // Type for var is Foo|Bar|Baz & !Foo -> Bar|Baz
    case (is Bar) {
        // Type for var is Bar
        print("BAR");
    }
    // Type for var is Bar|Baz & !Bar -> Baz
    case (is Baz) {
        // Type for far is Baz
        print("BAZ");
    }
}

Other constructions may get some use about the complementary types. First coming to my mind, the if(is… ) else construction, but probably anything having a type check, and an else at the end.

Being evil

I will not say complementary types are innocuous. As Ceylon is very regular language, and types are always real, one may write the following:

!Integer notAnInt= ... ;
print(notAnInt.hash); // This should raise a compiler error
!Integer&Object  neitherAnInt = ... ;
print(neitherAnInt.hash); // This should be ok. 

The type of notAnInt and neitherAnInt are clearly defined. But having such an fuzzy variable definitions may drive to some edge cases that should be studied in detail. Most of them can probably be solved having an strict attachment to set theory, but I won’t be that bold to say all of them can be solved.

Open discussion

My idea with this post is not saying that Ceylon is incomplete without complementary types. Not even saying that they should be implemented in the type system.

The idea is to open a discussion about them. Are complementary types useful? Do they improve language expressiveness? Will trying to push them into language create non-decidable cases?

Let the community decide (and maybe language leaders have something to say).

One thought on “Complementary Types in Ceylon

  1. Many points raised on gitter channel about this post.
    First, my sentence “this only works if EVERY possible object is either and Object or a Null.”. That refers to the fact that the return type for the coalesce function only does work if types Object and Null are disjoint and COMPLETE (meaning Anythig = Object ⋃ Null).
    This is, in fact, one of the basis of Ceylon: Everything is an object (unless it is null).

    But this drove to a discussion about the top of the type hierarchy on Ceylon, deviated from the point of this post.

    So let me present two functions that, being a bit different, behave the same way:

    retainType({Element*} elements) => { for (e in elements) if (is Type e) e };

    and

    removeType({Element*} elements) => { for (e in elements) if (!is Type e) e };

    The return type for ‘retainType’ function is, no doubt, {Type*}.
    But there is no clear return type por ‘removeType’ function. Unless complementary types are used, best guess would be {Element*}, that is not very expressive. Using complementary types, result is {Element&!Type*}, that is exactly what we are expecting.

    So finally we found a real use to complementary types! That sound good!

    Even more, @Zambonifofex noted another interesting usage:
    “I guess complementary types could be used to prevent Finisheds of going into streams… It currently behaves weirdly if they do…”

    Hooray! Complementary types seems to be useful!

    Then Gaving King comes to the picture, and raised something as true as concerning:

    “but the argument isn’t that ~ isn’t a useful operation
    the argument is that undecidability arises, i.e. the typechecker can overflow its stack
    so it doesn’t really matter how many examples of usefulness you provide
    unless someone can show some conditions under which it is decidable, i
    it’s better to keep it out of the language”

    This is totally true. It really doesn’t matter if the complementary type is useful or not, if it is not decidable.

    The truth is that I am not even close to an expert about decidability. Gavin says ‘undecidability arises’ and he is probably right… but I don’t know. I will investigate about what defines the decidability, and why the type checker will find those cases. A new idea is gestating in my mind.

    Like

Leave a Reply to someth2say Cancel reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s