Smoothing type functions and value functions

Maybe it is a bit late (8 month from last post!), but I re-read this post yesterday, and something came to my mind.

One of the roots of this post is depicting the similarity between value functions and type functions. While a value function defines the relation between input and output value types, a type function defines the relation between input and output type types. Smooth as silk!

But the way we express value functions and type functions don’t match that much. Let’s review the signature for defining functions in Ceylon:
– Named value function

Float addFloats(Float x, Float y) => x+y;

– Named type function:

alias Pair<Value> given Value satisfies Object => [Value,Value]; 

– Anonymous value function

(Float x, Float y) => x+y

– Anonymous type function

 <Value> given Value satisfies Object => [Value,Value] 

Looking for regularity

If the original post presents the homogeneity between type and value functions, I would like to propose homogeneity between those can be represented.

I can see two sources of irregularity:

Providing output types:

As far as I can see, “providing output type” can be understood as “providing a description for the output”.

Named value functions are the only ones that allow providing the output type (despite you can delegate it to the compiler). So I can’t really see a reason why I cant write anonymous value functions like “Float(Float x, Float y) => x+y”.

Even more, describing the output is not just providing a type, but providing the description (or the restrictions) the output must satisfy. So one should be able to ‘downcast’ the result to something like “Number(Float x, Float y) => x+y”, the same way we do when writing function headers.

For type functions, providing output type isn’t that straightforward. What is the type of the ‘type value’ on the right of the fat arrow? Digging a bit into Ceylon class hierarchy, we can see that Tuples satisfy Sequence, so in our example, we can use Sequence<Object>.

Clever reader may ask: “Why Sequence<Object>? Why not Sequence<Value>?” Running an analogy with value functions show the reason: Would you write “Sequence<x> gimmeASequenceWith(Float x)”? No! ‘x’ is a value, not a type! But you will use the restriction on the input to obtain the restriction on the output, like “Sequence<Float> gimmeASequenceWith(Float x)”.

Given that, we can rewrite the previous function definitions:
– Named value function: Allow optionally ‘downcasting’

Number addFloats(Float x, Float y) => x+y;

– Named type function: We can get rid of ‘alias’ keyword

Sequence<Object> Pair<Value> given Value satisfies Object => [Value,Value];

– Anonymous value function: Allow providing output type and optionally ‘downcasting’

Number(Float x, Float y) => x+y

– Anonymous type function: Allow providing output type

Sequence<Object><Value> given Value satisfies Object => [Value,Value] 

Note to self: This last definition clearly looks like a curried function! It can be understood as a type function that, given a type <Value> , returns another type function that, given a type <Object>, returns a Sequence type!

Locality for input restrictions:

One thing really disturbs me when writing code is locality. Definition should be close to defined, usage should be close to definition, etc… Without locality, you should go up and down the code, looking for the meta.

In value functions, definition for the parameters is just beside the parameter itself. In the value function example, definition for parameter ‘x’ is just besides it, in the form of the ‘Float’ type. Well done!

But in type functions, this is not the case. The restrictions on the input types should be provided ‘later’ with a given clause! This also means to verbosely repeating the name of the input type! What would you thing about the following value function definition?

    Number addFloats(x,y) given x satisfies Float & y satisfies Float => x+y;

The meaning is the same, but the definition look too verbose.So, what if we apply the concept of locality to type parameters in type functions?

    Sequence<Object> Pair<Object Value> => [Value,Value];

At first sight, it may seem confusing two types inside the “<>”. But when you realize that “Value” is not a type but a type value, things start to make a bit more sense. Maybe using a ‘variable-like’ name makes things clearer:

    Sequence<Object> Pair<Object X> => [X,X];

So getting back to the sample signatures, we can rewrite them again:
– Named value function:

Number addFloats(Float x, Float y) => x+y;

– Named type function:

Sequence<Object> Pair<Object Value> => [Value,Value];

– Anonymous value function:

Number(Float x, Float y) => x+y

– Anonymous type function:

Sequence<Object><Object Value> => [Value,Value] 

Summarizing:

So, if we accept all the proposed changes (output types for all and locality for input types), functions can be parsed by the following pseudo-grammar:
For value functions:

 [OutputType|'function'] FunctionName? '(' [InputType InputName]* ')' => ...

And for type functions:

 [OutputType|'alias'] FunctionName? '<' [InputType InputName]* '>' => ...

Really regular, isn’t it?

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).