In Relation To

Back to home

Existential types and type constructors

Posted by    |       Ceylon

I just ran across a great usecase for existential types (like Java's wildcard types, which Ceylon doesn't and won't support). It's a little involved, and revolves around an advanced feature of Ceylon that other languages don't have: the typesafe metamodel. But let me see if I can get the idea across.

Metamodel references as indirection

In Ceylon, a metamodel reference like Entry<String,File> has a well defined type which captures the signature of the operation the declaration defines — in this case, instantiation of the Entry class. We can write: 

ConcreteClass<Entry<String,File>,String,File> stringFileEntryClass = Entry<String,File>;

It just so happens that the metamodel type ConcreteClass<T,P...> is defined to extend the function type Callable<T,P...>, so we can even write stuff like this: 

Entry<String,File> stringFileEntryClass(String s, File f) = Entry<String,File>;
...
Entry<String,File> entry = stringFileEntryClass("out", File(outputFilePath));

Which is just an indirected way of writing the following: 

Entry<String,File> entry = Entry("out", File(outputFilePath));

What's going on here is that stringFileEntryClass() is an alias for the first-class function reference Entry<String,File> which just instantiates an Entry<String,File>.

Nice, huh? This is what we're talking about when we say Ceylon is a higher-order language. We can use a reference to any named declaration as first-class value, with a correctly-defined type.

References to type constructors

But what if we want to use Entry as a first-class value without nailing down concrete arguments to its type parameters. Well, Entry by itself isn't a type, it's a type constructor — a function that accepts two types as arguments and produces a type — or in more pretentious terminology that I personally prefer to avoid, a higher kind.

So, the question is, if we have a metamodel object for a type constructor, can we correctly represent its type within Ceylon's type system? Well, unfortunately not, because Ceylon doesn't have existential types. In an imaginary language Existential Ceylon, this is how the type of Entry would be specified: 

ConcreteClassConstructor<Entry<U,V>,U,V> entryClassConstructor 
        given U satisfies Equality 
        given V satisfies Equality
    = Entry;

And here's the kind of thing we could do with it: 

Entry<U,V> entryClassConstructor<U,V>(Type<U> ut, Type<V> ut)(U u, V v) 
        given U satisfies Equality 
        given V satisfies Equality
    = Entry;
...
Entry<String,File> stringFileEntryClass(String s, File f) = entryClassConstructor(String,File);
...
Entry<String,File> entry = stringFileEntryClass("out", File(outputFilePath));

i.e. We get an extra additional level of indirection here, letting us pass type arguments as ordinary first-class values. (It's actually pretty incredibly cool that you could even imagine making this work in Ceylon.)

Unfortunately, in Ceylon we won't be able to write things like this, since we simply can't correctly define the type of the value Entry without support for existential types. As ever, language design is all about compromises.

References to operators

There's another situation in which this same limitation arises. Ceylon's operators are defined in terms of methods, in many cases parameterized methods, or methods of parameterized types. For example, the < operator is defined in terms of the method smallerThan() of Comparable<T>. Earlier today I was asking myself if Ceylon should support some syntax like (<) (borrowed from OCaml) for references to operators. But I realized that this suffers from the problem described above. The type of (<) simply can't be expressed without the use of existential types or some kind of left-to-right type inference, because of the type parameter of Comparable. So you'll never be able to write: 

names.sortedBy((<))

in Ceylon. The best you'll be able to do is something like this: 

names.sortedBy(smaller<String>)

UPDATE: Well, actually, there is a reasonable solution that occurs to me. We're considering supporting a left-to-right type inference for the special case of single quoted literals, which would be limited to syntactically occur only in places where left-to-right type inference is possible. So the following syntax would work out, I suppose: 

names.sortedBy('<')

Is this a deeper problem?

This got me thinking. Type constructor parametrization (what's often called support for higher kinds) is something we wonder if Ceylon should eventually support. I'm talking about method signatures like the following, where the parameter M is not a type parameter that accepts a type, but a type constructor parameter, that accepts a type constructor: 

M<U> map<M<T>,U,V>(U function(V v), M<V> inputs) 
        given M<T>() satisfies Iterable<T> & Addable<T> {
    variable M<U> outputs := M<U>(); 
    for (V input in inputs) {
        outputs:=ouputs.add(function(input)); 
    }
    return outputs;
}

A question that naturally arises from the above discussion is whether you can even have support for type constructor parametrization at all in a language without existential types.

Well, yes, it seems to me that you can. The reason is that type arguments — and by extension type constructor arguments — aren't passed as ordinary values, but specified statically in the special type argument list delimited by angle brackets. Ceylon, along other C-like languages, doesn't let you write the following: 

Interface<Sequence<String>> stringSequenceType = Sequence<String>;
Sequence<String> hello = singleton<stringSequenceType>("Hello");  //error: stringSequenceType isn't a legal type argument

So the compiler does not need to be able to assign a Ceylon type to a type constructor argument in order to perform the necessary type checking. At some level, the compiler would need to be able to determine assignability of a type constructor to a type constructor parameter, but it would be able to go outside the bounds of the usual type system for first-class values in order to be able to make this determination. (This is no different from what Java does with type arguments, of course, since types aren't first-class values in Java.)

Some speculation

Interestingly, Ceylon probably could have gone down a different path. Rather uniquely, the language has:

  • reified generics, and
  • a typesafe metamodel.

So there's no really strong reason why Ceylon needs to have the special angle-bracket syntax for type arguments. Types are first-class values in Ceylon. We could in theory just treat type arguments as any other kind of value. It might even wind up actually simplifying the type checker.

At least now we've discovered one reason for not going down that path. It would mean either:

  • abandoning forever the idea of supporting type constructor parameterization, or
  • introducing existential types.

Oh and...

.. don't worry if you don't understand this post. Nobody really needs or wants to know what existential types and type constructor parameterization are in order to be able to write a useful program. Which is a little fact that is really important to keep in mind when designing languages. It's better if the conceptual framework of a language stays close enough to the kind of things people want to be thinking about when writing programs in the language.

Back to top