Constrained genericity

[KimBruce]

We need a syntax for constraints on type (generic) parameters. A lot of work has been done on this over the years, but no clearly satisfactory solution has emerged. (See https://go.googlesource.com/proposal/+/master/design/go2draft-generics-overview.md for the most recent design for Go and even more usefully, an analysis of support for generics in other languages.)

Here is a simple example of a class that requires a type parameter to contain a method m. The type HasM will (eventually) be used as a constraint on the type parameter T in class needsM:

type HasM = {
    m (n: Number) → Number
}

def a: HasM = object {
    method m(n: Number) → Number {n + 1}
}

type DoIt = {
    doIt (p: Number) → Done
}

// class safe only if T matches type HasM
class needsM ⟦T⟧ (d: T) → DoIt {
    method doIt(n: Number) → Done {
        print (d.m(n))
    }
}

print(needsM⟦HasM⟧(a).doIt(2))

While this is fine as far as it goes, a completely statically typed version of this code would require us to put a constraint on the type variable T in class needsM. We will write < for the constraint where T < HasM is only true if T has at least the methods in HasM.

How can we write these constraints? Here are three options. (1):

class needsM ⟦T⟧ (d: T) → DoIt 
       where T <* HasM {
    method doIt(n: Number) → Done { print (d.m(n)) }
}

or (2):

class needsM ⟦T where T <* HasM⟧ (d: T) → DoIt {
    method doIt(n: Number) → Done { print (d.m(n)) }
}

or (3):

class needsM ⟦T <* HasM⟧ (d: T) → DoIt {
    method doIt(n: Number) → Done { print (d.m(n)) }
}

The first of these has the advantage of keeping the header a bit cleaner, making it easier to see how to instantiate the type and regular parameters. It is probably closest to the original specification of type constraints in Clu. The second places the constraint closer to the introduction of T. The last is a more compact version of the second, and might even be used as an abbreviation of the second. It has the advantage that the constraint on type parameters immediately follows its introduction, more like the association of a type immediately after the introduction of a regular parameter. This is closest to the Java syntax for type constraints.

What if there are more than one type parameters and their constraints are recursive? Suppose we are given the following:

type Graph⟦E,N⟧ = {
    nodes → List⟦N⟧ 
    edges → List⟦E⟧
}

type EC⟦N⟧ = {
    fst → N
    last → N
}

type NC⟦E⟧ = {edges → List⟦E⟧}

class G⟦E,N⟧ → Graph⟦E,N⟧ { ...}

Of course we'd like to constrain E and N so they play nicely together. Copying above, our three options are (1):

class G⟦E,N⟧ → Graph⟦E,N⟧ 
    where E <* EC⟦N⟧
          N <* NC⟦E⟧
{ ...}

or (2)

class G⟦E,N where E <* EC⟦N⟧, N <* NC⟦E⟧ ⟧ → Graph⟦E,N⟧ 
{ ...}

or (3)

class G⟦E <* EC⟦N⟧, N <* NC⟦E⟧ ⟧ → Graph⟦E,N⟧ 
{ ...}

I now find the last option very unsatisfactory, as N is used before it is introduced, unlike the first two where N and E are both introduced as type variables before they are used as constraints.

My own preference at this point would be for the first as I find it more readable, though I could live with the second. While the third is more consistent with the association of types with regular parameters, the possible association of a constraint using a type variable before its use seems problematic.

Note that I have ignored issues with Self type here. As long as Self occurs in covariant positions (return types as opposed to parameter types), there is no issue. Self in contravariant positions require restrictions on use that I'd like to avoid for now.

[kjx]

scratchpad: https://docs.google.com/document/d/1-rPo9vww8se5isNfmeZT7x3nouE4_aPkYjKPiZeHeIU/edit?ts=5c89855a#

[apblack]

A couple of points suggested by Kim's comments above:

1. Using type variables before they are introduced is routine in the case of normal type definitions. For example, it's fine to define

type Edge = interface {
    start -> Node
    end -> Node
    weight -> Number 
}

type Node = interface {
    inEdges -> Set⟦Edge⟧
    outEdges -> Set⟦Edge⟧
    label -> String
}

2. So long as Self is in co-variant positions, we don't need matching; subtyping suffices (I think). Once we have contravariant Self, matching is different from subtyping. Try re-coding the Graph example with

type Edge = interface {
    isEdge(start:Node, end:Node) -> Boolean
    weight(start:Node, end:Node) -> Number
}

[apblack]

Right now, the non-terminal TypeParameterList occurs in 7 places in the grammar (see below). It makes sense to me that we should change the meaning of that one non-terminal, rather than adding a separate where clause to each of those 7 productions. (It was my mistake to add where clauses to just 2 of those 7 places, and to forget the other 5). This would mean putting the where clause inside the type parameter brackets, as per Kim's suggestion (2) or immediately following the ⟧ of the TypeParameterList

We could put the where clauses at the end of the declaration if we think that it looks nicer — but we should remember to add them to all 7 of the places where one can put a TypeParameterList

Here is the relevant grammar fragment from the spec:

AssignmentMethodHeader ::= Identifier ":=" TypeParameterList SingleMethodParameter
BinaryMethodHeader ::= <operator> TypeParameterList SingleMethodParameter
ParameterizedMethodHeader ::= <id> TypeParameterList MethodParameterList  ( <id> MethodParameterList )* 
ParameterlessMethodHeader ::= <id> TypeParameterList
TypeDeclaration ::= "type" Identifier TypeParameterList Annotations "=" TypeExpression Where
        | "type" Identifier TypeParameterList Annotations "=" InterfaceLiteral Where
UnaryMethodHeader ::= "prefix" <operator> TypeParameterList

TypeParameterList ::= Empty
        | "⟦" TypeParameter  ( "," TypeParameter )*  "⟧"

Where ::= Empty
        | "where" WhereCondition  ( "," WhereCondition )* 
WhereCondition ::= <id> <typeRelation> Type

[apblack]

We chose Kim's alternative (2) — put the where clauses in the ⟦brackets⟧

[apblack]

Grammar changed, and appropriate text included in the Spec in commit aeb0307c