Preliminary fix for recursive records with polymorphic contracts

[vkleen]

Implement a preliminary, but (hopefully) semantically sound fix for #1161. With this change, when building the recursive environment for a record, each pending contract on a field is applied twice, once normally and the second time "dualized". For a type A the dual contract for A is whatever would be applied as the domain contract of A -> Dyn.

This comes with a significant performance penalty on large records. A benchmark on a tf-ncl AWS configuration showed a 2.5x degradation. Because of this, we only apply contracts twice when they come from a type containing a type variable. This reduces the performance impact to 1.25x on the same benchmark.

The implementation introduces a new dualize field in Labels that indicates to a polymorphic contract that the dual contract is needed. The field is read by a new %dualize% primop and set in the code that builds recursive record environments.

Depends on #1192. Fixes #1161.

[yannham]

For the bystanders, note that this is not the final form of contract dualization: we expect (once proved correct) to implement a rewrite rule to just apply one contract that will be the equivalent of the composition of a contract and its dual contract. The only difference would happen at the type variables, which would have a special behavior (simple, in fact: they will just become partial identities, either on all terms, or on the subset of sealed terms). We expect the latter to have very low impact.

[yannham]

I fear this will disappear just as we do the fusion of the contract and the dual contract. But it's not too important, we can get rid of it then.

[vkleen]

Yes, it really should disappear then. I tried for a while to make do with just the data in type_environment, but I think I really need a global flag to compute the dual contracts dynamically.

[yannham]

So you flip the polarity if the label is dualized, although the polarity was already flipped as well in the code generating the recursive environment. This means the polarity is back to the original one? Is there any difference between a normal label and a dualized one, then? I might be a bit lost.

[vkleen]

polarity here is not the current polarity in the label. It's the statically assigned polarity of the forall binding during contract generation. Setting dualize to true in the label basically makes the code that subcontract generated pretend that it was called with an initial polarity of Negative.

[yannham]

Ah, if I understand correctly, you flip two different polarities when dualizing: the current polarity of the label (makes sense, as the whole contract moves to the codomain), and the one corresponding to what was the polarity of the forall when it was introduced. I'm not sure to understand why we need the second flip. Isn't T.dualize() in the notes defined as the codomain contract of T -> Dyn ? Shouldn't the foralls that are already introduced stay the same?

[vkleen]

When subcontract generates the domain contract for T -> Dyn, it calls T.subcontract(vars.clone(), pol.flip(), sy). So the polarities of all the forall's in T are flipped. That behaviour is replicated with the check here.

[yannham]

But you already flip the label polarity when dualizing, right? There is a call to flip(). This should corresponds to the pol.flip(). So, any forall introduced inside T should inherit the flipped polarity and shouldn't need an additional flip, it seems.

Additionally, here, the dualization seems to also targets type variables that are already introduced in T (free in T, the ones corresponding to vars inside subcontract, which shouldn't be affected by the codomain contract flip). The fact that it works is still a bit confusing, but there might be a "double dualization error that cancels out" as well. Or I might be misunderstanding something, but I'm having a hard time mapping the formalization of T.dualize() to this dualization operation.

[vkleen]

Let's walk through an example, say T = forall a. a. This is translated, by T.subcontract(pol = `Positive), into the contract

$forall 0 `Positive ($forall_var 0)

The contract T.dualize() should then be the domain contract in T -> Dyn, so we need to look at what T -> Dyn is translated into. That is

$func (T.subcontract(pol = `Negative)) $dyn
== $func ($forall 0 `Negative ($forall_var 0)) $dyn

So T.dualize() must be the contract $forall 0 `Negative ($forall_var 0). Note that no label polarities have entered the picture yet, but still the polarity (statically) passed to $forall is flipped.

Now, when the resulting contracts are applied, another layer of polarity tracking is initiated in the label. Let's imagine we're applying the contract T -> Dyn to a function f taking a T. Then the following reductions take place, where I'm pretending %go_codom% and %go_dom% primops don't do anything:

   ($func ($forall 0 `Negative ($forall_var 0)) $dyn) label f
== fun x => $dyn label (f ($forall 0 `Negative ($forall_var 0) (chng_pol label) x))
== fun x => f ($forall 0 `Negative ($forall_var 0) (chgn_pol label) x)

When building the recursive environment in a record, when thinking of a recursive field as a function T -> Dyn, a recursive reference x should then be patched to

$forall 0 `Negative ($forall_var 0) (chgn_pol label) x'

where x' is x with the original T contract applied to it.

[yannham]

Yes, I think I get it when the forall is introduced inside T. What I'm having a hard time seeing is how this works when the forall is introduced outside of the record. So, something like the record map type (say a specialized version): forall a. (a -> a) -> {_: a} -> {_: a}. Here, the contract T is mostly a. Shouldn't the corresponding forall contract then stay the same, instead of having its polarity flipped?

[yannham]

In some sense, it feels like it treats forall a. a and a exactly the same, which is bugging me

[vkleen]

The corresponding forall contract will stay unflipped, but the reason is a bit convoluted. Let's say we're dealing with a type like forall a. {_: a} -> {_: a} and let's see which contracts actually make it into the recursive environment. At first, the contract generation code will produce

$forall 0 `Positive ($func ($dyn_record ($forall_var 0)) ($dyn_record ($forall_var 0)))

Evaluation will then proceed and $dyn_record will insert just $forall_var 0 into the pending contracts of the record that it is applied to. So when building a recursive environment, there are no $forall's left in the contract term whose polarity would be flipped. Instead, the original polarity of the forall is recorded in the typing environment of the label and stays untouched.

In a sense, setting the dualize flag in the label to true flips only the forall's that have not yet been introduced. That's also what is checked by the new test in tests/integration/pass/contracts.ncl.

[yannham]

Ooooh, it's the $forall contract, not the $forall_var, in this snippet.... Here goes my wrong axiom 😅 . Now this absolutely makes sense. Thanks for taking the time to explain.

It's a really non trivial magic trick we're pulling here, we'll have to document it very clearly and in details, if we want this to be remotely understandable 6 months from now. The examples you posted here are valuable and should be stored somewhere, before we put the note in good shape.

[dpulls]

🎉 All dependencies have been resolved !