Open RossTate opened 10 years ago
This all sounds pretty interesting and useful to me.
@RossTate Do you have some definition about this "shape" concept and what it brings to compile-time decidability?
Sure. The idea is to limit recursive inheritance, which is the source of a lot of decidability problems. So, let's say that by default, classes and interfaces can't be inherited recursively, meaning you can't have something like Foo satisfies Bar<Foo>
for typical classes/interfaces Bar
. If you want to allow a class/interface to be inherited recursively, typically because it encodes some self type or type family, then you declare it a "shape", which has the cost of restricting how you might use that class/interface otherwise. A good example of something you would want to be a shape is Comparable
. The restriction, then, is that you can't use this shape as a type argument for any generic class/interface/method (which in Ceylon's case means it can't be used as a type for a function's parameter or return), which essentially leaves them for just being used as constraints. For example, you're not allowed to use the type List<Comparable<Integer>>
because its using the shape Comparable
as a type argument to List
. This is fine since we did a bunch of analysis on existing code and found that this restriction reflects how these kinds of classes/interfaces are already used in practice. And, by significantly restricting recursive inheritance, many problems become much easier to solve, with even naïve solutions being guaranteed to terminate. (Note that in Ceylon's case, shapes are essentially the classes/interfaces with an of P
clause where P
is one of the type parameters.) Does that answer the preliminary questions you have?
Yes, thanks
Awesome. @gavinking, do you have any questions?
There are some technical things to refine, such as how to deal with conditionally provided methods with the wrong variance, as in the equals
conditional method for Iterable
. But I wanted to understand your perspectives before going into those technicalities.
Heh, well, my perspective is that we're trying to get 1.0 and then 1.1 out and that this kind of thing will not happen before Ceylon 1.2. I can't really invest the time in thinking about this stuff right now...
Sorry!
That's fine. The only immediate action item, then, would be to ensure forward compatibility. Thus, in addition to the termination of subtyping/equivalence-checking problem, this is another reason to put the shape restriction in place, and maybe one others would be happier with.
I just thought about this a couple of days ago when I was writing some Vaadin code. In Vaadin's data binding model there is the interface Container and many subinterfaces like Container.Sortable, Container.Ordered etc.
It is pretty much impossible to write Container adapters in Java, because client code will use "instanceof" checks to determine which features a container supports. So I was immediately thinking "Ceylon must have a solution for this" and I even had the same syntax in mind. So I'm delighted to see that you also like this idea.
Hi @RossTate, do I understand correctly that this plan would disallow methods of the form:
void mymethod(Comparable<Integer> comparable) { ... }
but that it's fine because they can always be written as
void mymethod(T comparable) given T satisfies Comparable<Integer> { ... }
?
Right, although if you know of a practical use for your example I'd be interested to know.
@RossTate if, in conjunction with this proposal for "static
" polymorphism, we were to introduce shapes, perhaps with the following syntax:
interface Summable of this {
shared formal static this zero;
shared formal static this add(this x, this y);
shared this plus(this z) => add(this, z);
}
final class Integer satisfies Summable {
shared actual static Integer zero = 0;
shared actual static native Integer add(Integer x, Integer y);
}
shared Value sum<Value>({Value*} values)
given Value satisfies Summable {
variable value sum = Value.zero;
for (val in values) {
sum+=val;
}
return sum;
}
Then what precisely would be the restrictions that you would want to place on inheritance in order to guarantee decidability.
Remember that in the long discussion in #596 we got all hung up on the problem that the proposed restrictions at the time were going to disallow certain types that people considered useful. Would that still be the case, or have you found ways to make the relax the restrictions to something that everyone will consider acceptable?
Summable
would not be a "type", which particularly means it couldn't be used as a type argument to other typesInteger
had a subclass, say One
, then One satisfies Summable
would not necessarily hold (so using the same term for class/interface inheritance and shape satisfaction may be misleading)The static
stuff makes no difference, though you open a huge can of worms if you want to be able to locally override the default static
implementation (e.g. use reverse order in a tree map instead of the default order).
So in #596 I mentioned an alternative way to constrain inheritance in order to ensure decidability of various algorithms. Here I am going to show how that some constraint, the concept of "shapes", can enable cool new features.
Back in the day we had a huge discussion about how to do equality. We ended up just going with Java's equals(Object) technique, sacrificing types for sake of flexibility. One of the obstacles that led us there was the issue that many generic classes can only properly implement equality if their type arguments implement equality. This prescribes conditional inheritance, but that had various problems, one of which was decidability (implementation was another major one, but I think I've figured out how to get over that one). However, with shapes, conditional inheritance of shapes is decidable! So with shapes we can do the following (where
Equatable
is a shape):(Note that, due to variance, it's important that
equals
beactual
to maintain type soundness.)Here's another example (
Summable
is also a shape):Now, let's look back at
Iterable
andEquatable
. Many iterable collections have their own notion of equality. This has been kind of annoying because you get weird results when equating lists and sets in Java. A way to solve this is to use "adaptors", another technology made possible by the shape restriction. With an adaptor can locally override or install an implementation of a shape for a given type. For example,Then to use the adaptor, you do something like the following:
The
using
clause indicates to override the default implementation of the constraint with the given adaptor. In this case the adaptor isReverse
, and so the sorted list will be in decreasing order rather than the typical increasing order.You can do this with classes as well. For example, people often want hash maps to use reference quality rather than deep equality. To do that, you just do:
This seems snazzy to me, but I'm interested to hear your thoughts. Again, this all relies on the shape restriction for both compile-time decidability and run-time implementation reasons.