Colocated in choreographies #32
Conversation
The `Colocated<T, L>` type is contravariant, meaning that for any `A` that's a subtype of `A | B`, we have `Colocated<T, A | B>` being a subtype of `Colocated<T, A>`! This is so that any message of type `Colocated<T, A | B>` can be passed to `unwrap`, which can accept a parameter of type `Colocated<T, A>`. For instance, we might want `Colocated<string, "alice" | "bob">` to be accepted by the `unwrap()` function for "bob" in `locally`, which can accept an argument of type `Colocated<T, "bob">`. This contravariance is fine except when we want to extend the `Colocated<T, L>` type for `Args` in the `Choreography` type definition in `core.ts`, so then the `Choreography` can accept `Colocated<T, L>` types as arguments. The problem is that `Args` tries to extend `Colocated<T, L>` to its subtypes, and the only subtype when all locations are specified in `L` is the `Colocated<T, L>` type with the same locations specified in `L`! In particular, this means that an argument of type `Colocated<T, A | B>` cannot be passed to a parameter with type `Colocated<T, A | B | C>`, which is what is extended by `Args` in the choreography when the choreography is first defined. This contravariance of the `Colocated<T, L>` type is enforced by the `phantom?: (x: L) => void` member in the `Colocated` class where it's defined in `core.ts`, which takes advantage of the fact that function types are contravariant in Typescript (so for subtype `A` of `A | B`, the function type `(x: A | B) => void` is a subtype of `(x: A) => void`). Compare this with the definition of the `Located<T, L>` class in `core.ts`, where we have `{phantom?: L1}` instead, which just compares the types of `phantom` between two `Located` objects in the natural covariant fashion, such that `A` is a subtype of `A | B`. Since the `phantom` member is optional, its value doesn't need to be given, but its type is still compared between two objects of the type it's defined for (hence the name "phantom"). With this limitation, it seems like we need a way for a `Choreography` to accept `Colocated` in a covariant type fashion, while `unwrap` still accepts it in a contravariant fashion. I am still trying to think of a workaround for this.
Implemented covariance and contravariance for the choreography `Colocated` type
…ance for `Colocated` messages work now!
Codecov Report
@@ Coverage Diff @@
## main #32 +/- ##
==========================================
- Coverage 88.48% 88.36% -0.12%
==========================================
Files 19 19
Lines 660 662 +2
Branches 89 89
==========================================
+ Hits 584 585 +1
- Misses 75 76 +1
Partials 1 1
... and 1 file with indirect coverage changes 📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
There was a problem hiding this comment.
@ImpregnableProgrammer This is great! As we discussed offline, I want type-level test cases (on error cases) to make sure this approach works as intended. More specifically, I want tests that ensures
- when using as choreography arguments are covariant
- If you provide a colocated value with missing locations, it would be a type error
- when unwrapping, they are contravariant
- If you try to unwrap at invalid locations, it would be a type error
The easiest way to test the type is to use if (false) and // @ts-expect-error as done in the backend test suite.
choreography-ts/packages/core/src/backend-local.test.ts
Lines 38 to 41 in 9c4407b
I think you can have something similar in examples and the typecheck task would check the line (which never gets executed at runtime) does not typecheck.
| return []; | ||
| }; | ||
|
|
||
| const _test: Choreography< |
There was a problem hiding this comment.
It is better if you have actual jest tests as in the bookseller2 example.
|
|
||
| // Exported `Colocated` class and the corresponding covariant or contravariant type variations | ||
| export class Colocated<T, L extends Location> extends ColocatedBase<T> { | ||
| phantom?: ((x: L) => void) & L; |
There was a problem hiding this comment.
Question: do we need this line at all? It seems that everything typechecks without this line.
| ] | ||
| | [] | ||
| > = async ({ locally, peel, multicast }, [msgAlice, msgCarol]) => { | ||
| const aliceMsg = peel(msgAlice); |
There was a problem hiding this comment.
wait a second, why is this valid? If this choreography is being executed on Locations = "alice" | "bob" | "carol" | "dave", it should be illegal to peel Colocated<string, "bob" | "alice" | "carol"> because it would be undefined at dave, no?
This pull request makes changes that resolve issue #31 to now allow passing
Colocatedmessages to and returning them from choreographies. This works around the limitation ofColocatedmessage types being contravariant, which caused an issue while passing them as arguments to choreographies.