Prototype 'out' type variables that mimic associated types

[Garciat]

First, I introduced @Out which annotates a type parameter in a type class. It denotes that a witness for this type class outputs a type through the respective type argument.

My goal was to enable an encoding of GHC Generics, without the need for type families:

interface Generic<A, @Out Rep> {
  Rep from(A value);
  A to(Rep rep);
}

And, for starters, with a very basic type-level representation:

interface TyRep {
  record K1<A>(A value) {}

  sealed interface Sum<A, B> {
    record L1<A, B>(A left) implements Sum<A, B> {}

    record R1<A, B>(B right) implements Sum<A, B> {}
  }

  record Prod<A, B>(A first, B second) {}
}

Witnesses would then look like:

sealed interface Tree<A> {
  record Leaf<A>(A value) implements Tree<A> {}

  record Node<A>(Tree<A> left, Tree<A> right) implements Tree<A> {}

  @TypeClass.Witness
  static <A> Generic<Tree<A>, Sum<K1<A>, Prod<K1<Tree<A>>, K1<Tree<A>>>>> generic() { ... }
}

The API is really simple. But then we have a couple of implementation challenges to tackle:

1. Revamping witness resolution so that types flow out of type variables whose target parameter is annotated with @Out.
2. Tying the knot for recursive data types such as Tree above, so that:

• resolution terminates, and
• the resolved witness constructor plan can be reified.

Let's tackle (2) first.

First, I introduced a wrapper type that introduces laziness for witness constraints:

interface Lazy<A> {
  A get();
}

It needs to be applied, for example, when handling the K1 type representation constructor, which may or may not introduce recursion. For example:

@TypeClass
public interface ToJsonGeneric<Rep> {
  JsonValue toJson(Rep rep);

  @TypeClass.Witness
  static <A> ToJsonGeneric<K1<A>> k1(Lazy<ToJson<A>> toJsonA) {
    return rep -> toJsonA.get().toJson(rep.value());
  }
}

Then, I updated the recursive resolution algorithm:

• Introduced a Lazy constructor for the ParsedType ADT. This marks the request for lazy resolution by the client.
• Started keeping track of previously seen resolution targets. (Similar to a DFS algorithm.)
• When the resolution target is has Lazy on the head, then:
  • If this the type under the Lazy constructor has been seen before, then emit a LazyLookup node,
    • In this case, witness reification is expected to keep its own cache to tie the know and use this a signal to look up in the cache.
  • otherwise recurse into resolution as usual, but wrap the result in a LazyWrap node.
    • This is so that witness reification can correctly return an instance of Lazy<A>, even though we have a concrete object.

Now, onto tackling (1).

At a high level:

• Type variables which are arguments to @Out-annotated type parameters are annotated in the ParsedType structure somehow.
• After finding a single witness constructor candidate (through unification and overlapping instances reduction):
  • The candidate's constraints (its argument dependencies) are substituted with the result from unification. (This is not new).
    • These resolved constraint types may contain unbound type variables.
    • Some of which are under an Out constructor. (Note: unification ignores Out nodes.)
  • From each constrain type, we can derive: (provides: List<Var>, expects: List<Var>).
    • Type variables under Out constructors go in provides and the rest go under expects.
  • This denotes a directed graph. (Possibly acyclic due to Java's type system; not sure.)
  • Constraints can be topologically sorted, from fewest expectations to most. (Like a TreeMap<Integer, List<Constraint>>.)
  • At each expectation stratum:
    • Resolve each constraint type.
    • Unify each newly-resolved constraint type with the original constraint type.
    • Merge all substitutions maps and apply them to all of the constraint types (or just the following stratum).
  • By the end of this, there should be no unbound type variables.
    • If there are any, resolution fails.
  • Resolution succeeds with a witness constructor match where its return type and constraint types have been fully substituted .

[codecov]

Codecov Report

❌ Patch coverage is 65.42751% with 93 lines in your changes missing coverage. Please review.
✅ Project coverage is 60.34%. Comparing base (096b66a) to head (92d8869).
⚠️ Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
.../java/com/garciat/typeclasses/impl/Resolution.java	61.83%	41 Missing and 9 partials ⚠️
.../main/java/com/garciat/typeclasses/impl/Types.java	52.00%	6 Missing and 6 partials ⚠️
...main/java/com/garciat/typeclasses/TypeClasses.java	50.00%	7 Missing and 1 partial ⚠️
...n/java/com/garciat/typeclasses/impl/Witnesses.java	46.15%	5 Missing and 2 partials ⚠️
...ciat/typeclasses/runtime/RuntimeWitnessSystem.java	68.42%	3 Missing and 3 partials ⚠️
.../java/com/garciat/typeclasses/impl/ParsedType.java	70.00%	2 Missing and 1 partial ⚠️
...java/com/garciat/typeclasses/impl/Unification.java	66.66%	0 Missing and 2 partials ⚠️
...java/com/garciat/typeclasses/impl/utils/Lists.java	66.66%	1 Missing and 1 partial ⚠️
...iat/typeclasses/processor/StaticWitnessSystem.java	89.47%	0 Missing and 2 partials ⚠️
...java/com/garciat/typeclasses/processor/Static.java	50.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main      #25      +/-   ##
============================================
- Coverage     61.50%   60.34%   -1.17%     
- Complexity      276      334      +58     
============================================
  Files            58       61       +3     
  Lines           769      976     +207     
  Branches         52       87      +35     
============================================
+ Hits            473      589     +116     
- Misses          252      318      +66     
- Partials         44       69      +25     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.