Self types and type families in Ceylon

Posted by    |      

I've just finished implementing support for self types and type families in the Ceylon type analyzer. I think this stuff is pretty cool, if ever so slightly esoteric.

Let's start with the simpler thing. A self type is a reasonably familiar idea to most of us who write Java code for a living, since we've all used Comparable from time to time. Let's translate Java's Comparable interface to Ceylon:

shared interface Comparable<Other> {
    shared formal Integer compareTo(Other other);
}

The type parameter Other is a self type. It represents the type of the class that implements Comparable. I'm not quite sure why Java's Comparable doesn't have a type constraint like the following on Other:

shared interface Comparable<Other>
        given Other satisfies Comparable<Other> { ... }

This constraint prevents us from forming nonsensical types like Comparable<Object>. So I think the constraint is useful.

Now let's add an operation to Comparable that treats Other as a self type:

shared interface Comparable<Other>
        given Other satisfies Comparable<Other> {
    shared formal Integer compareTo(Other other);
    shared Integer reverseCompareTo(Other other) {
    	return other.compareTo(this); //error: this not assignable to Other
    }
}

Oops! This doesn't compile. You see, Comparable<Other> is not a subtype of Other. We can write pathological classes like this one:

class NotAString() satisfies Comparable<String> { ... }

We need to properly capture in our code that Other is a self type, and that the only thing that can be assigned to Comparable<String> is String. We can't express this in Java, but in Ceylon we can now write:

shared interface Comparable<Other> of Other
        given Other satisfies Comparable<Other> { ... }

The new syntax of Other expresses the idea that the only direct subtype of Comparable<Other> we need to account for is Other. The compiler will now prevent us from defining a class like NotAString above. And now our code compiles:

shared interface Comparable<Other> of Other
        given Other satisfies Comparable<Other> {
    shared formal Integer compareTo(Other other);
    shared Integer reverseCompareTo(Other other) {
    	return other.compareTo(this);
    }
}

Well, that's nice, and occasionally useful, but the real reason for introducing this machinery is to be able to abstract over groups of types using a type family. Subtype polymorphism and parametric polymorphism (generics) let is write code that abstracts over a single unknown type without losing type safety. The notion of a type family generalizes that idea to several related unknown types.

Let's reuse (loosely) an example I found lying around on the internet.

In this example, the type family we're interested in is the family of Graphs, where a Graph consists of a Node type and an Edge type. Here's how we can express this type family in Ceylon:

abstract class Graph<ActualNode,ActualEdge>() 
    given ActualNode satisfies Node
    given ActualEdge satisfies Edge {
    
    shared formal class Edge(ActualNode from, ActualNode to) 
            of ActualEdge {
        shared ActualNode from = from;
        shared ActualNode to = to;
        shared Boolean touches(ActualNode node) {
            return from==node || to==node;
        }
    }

    shared formal class Node() 
            of ActualNode {
        shared default Boolean touches(ActualEdge edge) {
            return edge.touches(this);
        }
    }

}

Let's look carefully at the Node member class. The class is declared formal, meaning that subclasses of Graph must provide a concrete subclass of Node. If you don't understand this, please read about member class refinement in Ceylon. Graph also has a type parameter ActualNode, representing the concrete subclass of Node in a particular subclass of Graph. It's not a self type, it's a member-of-self type!

We're using the of clause to express that the type parameter ActualNode is the only direct subtype of the type Graph<ActualNode,ActualEdge>.Node. The difference in this case is that the type parameter belongs to a containing type Graph of the type Node (the type family). Notice how we make use of this relationship in the touches() method of Node, where this is assigned to a parameter of type ActualNode.

Now let's create a concrete group of types that realizes this family:

class BasicGraph() extends Graph<Node,Edge>() {
    
    shared actual class Node() 
            extends super.Node() {}
    
    shared actual class Edge(Node from, Node to) 
            extends super.Edge(from, to) {}
    
}

Easy. We just fill in the missing Node and Edge types.

Of course, this whole exercise wouldn't be worth doing if BasicGraph was the only kind of Graph, so let's add a second member of the family:

class OnOffGraph() extends Graph<Node,Edge>() {
    
    shared actual class Node() 
            extends super.Node() {
        shared actual Boolean touches(Edge edge) {
            return edge.enabled && super.touches(edge);
        }
    }
                
    shared actual class Edge(Node from, Node to) 
            extends super.Edge(from, to) {
        shared variable Boolean enabled := true;
    }

}

OK, now let's get to the cool part. BasicGraph and OnOffGraph are completely typesafe. I can't accidentally try to create an Edge of an OnOffGraph by passing two Nodes from a BasicGraph. The last line of the following code does not compile:

BasicGraph bg = BasicGraph();
BasicGraph.Edge bge = bg.Edge(bg.Node(), bg.Node());

OnOffGraph oog = OnOffGraph();
OnOffGraph.Edge ooge = oog.Edge(oog.Node(), oog.Node());

OnOffGraph.Edge evil = oog.Edge(bg.Node(), bg.Node()); //error: BasicGraph.Node is not assignable to OnOffGraph.Node

The compiler enforces the constraint that Edges and Nodes of BasicGraphs only mix with other Edges and Nodes of BasicGraphs, not with Edges and Nodes of OnOffGraphs.

And yet, it's still possible to write code that abstracts over all kinds of Graphs without losing that typesafety:

Edge createEdge<Node,Edge>(Graph<Node, Edge> g) 
        given Node satisfies Graph<Node,Edge>.Node 
        given Edge satisfies Graph<Node,Edge>.Edge {
    return g.Edge(g.Node(),g.Node());
}

BasicGraph.Edge e = createEdge(BasicGraph());
OnOffGraph.Edge e = createEdge(OnOffGraph());

Is that cool or what?

I mentioned above that I've already implemented this in the type analyzer, but it's not clear to me how much work is involved making this stuff work in the backend, so I'm not sure if this feature will be in the M1 compiler release or not.


Back to top