gracelang / language

Design of the Grace language and its libraries
GNU General Public License v2.0
6 stars 1 forks source link

What does Self mean in Types? #172

Open apblack opened 5 years ago

apblack commented 5 years ago

The spec currently says

The reserved word Self (capitalised) refers to the type of the current object.

Issue #79 (now closed) contains previous discussion about Self, but neither it nor the above statement consider the meaning of Self in type declarations.

Consider these following declarations:

type Point1 = {
     …
     == (pt: Point1) -> Boolean
}

type Point2 = {
     …
     == (pt:Self) -> Boolean
}

We don't want the Self in Point2 to refer to the type of the current object. (That might be, for example, a module object that contains the type declarations.) Instead, we want Self to be a local variable of the type declaration Point2, and we want it to mean "this type here defined".

When we write

type ExtendedPoint = Point2 & SomethingElse

the argument to the ==(_) method in ExtendedPoint is still Self, which now means ExtendedPoint.

We are making a pun here, with a declaration like that of Point2 being both a type generator (a function returning a type), and the fixpoint of that generator, depending on the role that we want it to play. When we use Point2 in the definition of ExtendedPoint, we are treating it as a generator; similarly, ExtendedPoint is also a generator, containing a still-unbound Self. When we use Point2 or ExtendedPoint to specify the type of a variable, we are implicitly taking the fixpoint of the generator.

Thus, in the spec, we need to say that the meaning of Self depends on the context in which it is used. In an object constructor, it is the interface of self; in a type constructor, it is a name for the type being constructed.

The spec also says currently that "Self is prohibited as the annotation on parameters". We need to remove that restriction. It's true that if Self is used to type-annotate a parameter of a method, then objects that inherit that method will not be subtypes of their parent. But that's quite different from saying that one can't express such types; we need to be able to express them to write type constraints.