Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dyno: initial implementation of checking (explicit) interface constraints #26396

Open
wants to merge 72 commits into
base: main
Choose a base branch
from

Conversation

DanilaFe
Copy link
Contributor

@DanilaFe DanilaFe commented Dec 12, 2024

This PR lays the foundation for interface support in Dyno; specifically, it makes it possible to verify that a type implements an interface via an implements statement or via a definition like record foo : someInterface. The goal here is to implement the functionality required by stabilized standard library features. Specifically, it's desirable to support the outcomes of the special method naming discussion by supporting hashable, serializable, etc., the implement interface primitive, as well as the Sort module discussion in the form of the sortComparator interface.

The Predicate interpretation of interfaces

We can think of interfaces as predicates on types; an interface definition as follows:

interface I {
  proc Self.foo();
}

Defines a predicate I(t) which is satisfied when a method t.foo() is present. This generalizes well to multi-argument interfaces, even though they are not officially stable: an interface

interface BinaryI(T1, T2) {
  operator :(lhs: T1, rhs: T2);
}

Defines a binary predicate I(T1, T2) that holds when one of the two types can be cast to another.

InterfaceType encodes the predicate

When we are searching for a witness to prove a predicate, we want to state what it is we are trying to "prove". As a result, it's convenient to have an encoding for a claim like I(t1, ..., tn), even if we haven't found a proof for it yet, or never will. I elected to make this object -- which just contains the interface ID and a mapping of its formals to requested types -- itself a type. I think this makes sense because interface predicates can occur in expressions and statements:

proc foo(x: I) {}
proc bar(x, y) where implements BinaryI(x, y) {}
implements BinaryI(int, bool) {}

As a result, it's easier to just treat the interface constraint as another sort of type that can be constructed. This PR takes that route, defining a new type constructor for interfaces (default-functions.cpp, commits aba8332, e157006, cfa3b26). From there, it simply relies on the standard resolution process.

Implementation points

There are several ways to implement an interface:

record myRec : I {}
myRec implements I;
implements I(myRec);

Generally speaking, all of these map to a predicate application I(myRec). Thus, it became convenient to treat them in an (almost) unified manner, instead of resorting to constant AST-based pattern matching. To this end, I introduced ImplementationPoint, which contains the interface ID, the ID of the AST node that causes the implementation, and a list of actuals / arguments to the predicate. Unfortunately I had to treat the myRec : I case specially because resolving the type of myRec involves resolving the aggregate declaration rather than searching for an expression's type.

To check whether an interface predicate (in the form of an InterfaceType) is satisfied, one needs to find all implementation points available, find the one that applies to the given interface and types, and check whether at that point, the requirements for the predicate (e.g., the presence of Self.foo()) are met.

In implementing the implementation point search, I observed that in production, visibility of implementation points is propagated only via unrestricted use statements. Thus, import M.{R} would not bring in the implements facts for R, even if they are in the type's declaration. In general, it's not possible to "name" a standalone implements statement, which means it's impossible to mention it in a restriction on something like import; as a result, I chose to always bring in implements I(T) statements into a scope through mentions of modules in visibility statements. Leaning on this approach, it was easiest to also always bring in implementation points from type declarations like R : I. This is perhaps inefficient (we see more implementation points than might be usable), but it's sound (if a type isn't brought in, its implementation point is irrelevant) and perhaps even necessary if a type isn't directly visible, but is, e.g., contained via another imported type:

module M1 {
  interface I {}
  record R : I {}
  record S { var x: R; }
}
module M2 {
  import M1.{S};

  proc doSomething(x: I) {}

  doSomething((new S()).x); // perhaps this ought to work?
}

Finding matching implementation points

To support the standard library today, we need support for generic implementation points, such as implements hashable(_tuple). In general, there may not be only a single matching implementation point for any application of an interface predicate.

At first, I wanted to treat finding a matching implementation point as a function call, and piggy-back on the disambiguation process to select the most specific generic implementation point if need be. I still think this is desirable, but there were a number of challenges and observations in the way:

  • We would need to construct a generated proc that corresponds to the implementation point. This is fine by itself, but the code that maps IDs to their (generated) ASTs is relatively brittle (see builderResultForDefaultFunction) and relies on name-based comparisons. It might be possible to get it to work with implementation points, but it did not seem worth it for a first prototype.
  • Given a hypothetical generated function, we would still need to adjust logic in instantiateSignature to handle the case of an interface implementation function. instantiateSignature is already very complex and hard to maintain, and additional tweaks will only make it more so.
  • The disambiguation code is more intense than we need it to be. Notionally, an implementation point only has type formals, so conversions, coercions, and other measures of specificity are less important.
  • In production, we do not use function resolution to find the matching implementation point.

As a consequence of the above bullets, this PR matches the behavior of production, by simply iterating the list of visible implementation points, selecting the first concrete point if one exists, and otherwise selecting the first generic point.

Checking Interface Constraints

Once an implementation point is found, the last step is to check if the interface's requirements (methods, associated types) are met. When it comes to "subtyping" or compatibility, functions are contravariant in their inputs, and covariant in their outputs. Thus, a function that satisfies an interface must have formals that are supertypes of the interface function's signature, and a return type that is a subtype of the interface function's return type. Thus, when searching for a function proc foo(arg1: A, ... argN: Z), set up a call for foo(A, ..., Z) and resolve it. This finds a function that accepts the required types, and possibly more (i.e., the formals are supertypes). From there, it's necessary to check if the return type of the function can be passed to the type expected by the interface (in other words, if it's a "subtype").

It was suggested in the team chat that we ought to treat formal names as part of the iterator's interface. As a result, this implementation feeds all arguments by name foo(arg1 = A, ..., argN = Z), and then ensures that this does not cause re-ordering of formals -- that way, both by-name and nameless calls ought to work.

The trickiest aspect is that some of our standard interfaces (particularly serializers and the keyComparator interface) require generic functions, sometimes with type queries. Here's one offender (not defined in production because prod. can't handle it):

interface serializable {
  proc Self.serialize(writer: fileWriter(locking=false, ?ST), ref serializer: ST);
}

Here, the type query constraints are important, and the ability to accept any serializable type is important. Thus, when checking interface constraints, what we want is the ability to "match up" type queries. This PR does this by introducing opaque --- but concrete --- placeholder types for type queries in the interface's function. The above signature becomes:

proc Self.serialize(writer: fileWriter(locking=false, Placeholder(ST)), ref serializer: Placeholder(ST));

Because they are unique, these types cannot be passed to concrete formals (i.e., ref serializer: binarySerialier will not accept a Placeholder(ST), because the latter is only compatible with itself). This ensures that the candidate function is generic in that spot, or references a previously queried type parameter. To make this work, the PR adds a new flag (usePlaceholders) in Resolver that configures it to create placeholder types in place of AnyType.

Placeholders are also used for interface formals (e.g., Self) when getting the signature of a formal's required function. This is because an interface is intended to encapsulate all the required properties of a type. If Self is immediately instantiated with a type, then in cases like proc Self.foo(), this type can be used as the implicit receiver for calls, which introduces "hidden" dependencies on methods that aren't clear from the interface declaration. Using an opaque placeholder type like Placeholder(Self) ensures that no "external" methods slip in, and that the signatures in the interface are self-contained.

Thus, the typed signatures of the interface's required functions have placeholders for Self; however, when searching for candidates that satisfy these signatures, we need to use the actual type of Self (e.g, int in I(int)). Thus, this PR adds a "substitute" method on Type and related types to replace placeholders with their actual values. Note that this does not replace the placeholders from generic type queries.

TODO before this PR is non-draft

  • error immediately for concrete implementation points
  • comments to new headers
  • nicer stringify function for InterfaceType
  • move interface types into a new header
  • implementation point formals should be called actuals
  • use const Type* for substitution instead of QualifiedType

Future work

  • resolving functions with constraint formals, like foo(x : I)
    • this includes the default bodies of interface signatures
  • design: how should we prioritize between several generic implementation points?
  • design: should we note calls for interface resolution as associated actions anywhere?
  • associated / dependent constraints, which are not used in production

Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
This is a shortcut for resolving the call `I(t1, t2, ...)`.

Signed-off-by: Danila Fedorin <[email protected]>
Since type queries don't currently work while resolving the expressions,
there's no reason to pretend they do in the code.

Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
0 = implements interface, 2 = no interface found

Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
Signed-off-by: Danila Fedorin <[email protected]>
@DanilaFe DanilaFe marked this pull request as ready for review December 13, 2024 22:20
@dlongnecke-cray dlongnecke-cray self-requested a review December 13, 2024 22:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant