Type unification for rows, new records, and variants #1646
Conversation
Codecov Report
@@ Coverage Diff @@
## unstable #1646 +/- ##
============================================
+ Coverage 74.96% 75.15% +0.19%
============================================
Files 358 358
Lines 11612 11654 +42
Branches 541 569 +28
============================================
+ Hits 8705 8759 +54
+ Misses 2907 2895 -12
Continue to review full report at Codecov.
|
There was a problem hiding this comment.
I feel this is a little harder to follow than it should be. I had to look back at some previous PR to remember the relation between RecRow and Row. I still believe that introducing a different kind than TlaType1 would make this relation clearer in the code. I'm fine with keeping things like this for now, but I would like to try an approach with kinds on TNT and then, if it's clearer, we can copy it to apalache or something like that.
| val maxUsedVar = Math.max(genericType.usedNames.foldLeft(0)(Math.max), targetType.usedNames.foldLeft(0)(Math.max)) | ||
| new TypeUnifier(new TypeVarPool(maxUsedVar + 1)).unify(Substitution.empty, genericType, targetType) match { |
There was a problem hiding this comment.
Huh, was there a case where type-var name IDs were causing problems?
There was a problem hiding this comment.
Yes. We had it a month or two ago.
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeUnifier.scala
Outdated
Show resolved
Hide resolved
tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeUnifier.scala
Outdated
Show resolved
Hide resolved
| // the base case | ||
| (lvar, rvar) match { | ||
| case (None, None) => | ||
| if (rfields.nonEmpty) None else Some(RowT1()) |
There was a problem hiding this comment.
As an aside, I really don't like how object RowT1 methods are all apply, because it makes it hard to track what is actually being constructed, since RowT1(), RowT1(_), RowT1(_,_) are all different methods that return a RowT1.
| if ( | ||
| compute(lvar.getOrElse(RowT1()), RowT1(rfields, Some(tailVar))).isEmpty | ||
| || compute(rvar.getOrElse(RowT1()), RowT1(lfields, Some(tailVar))).isEmpty | ||
| ) { | ||
| None | ||
| } else { | ||
| // apply the computed substitution to obtain the whole row | ||
| asRow(Some(Substitution(solution).sub(RowT1(lfields, lvar))._1)) |
There was a problem hiding this comment.
The fact that compute mutates solution internally makes this really hard to understand. I'd at least appreciate a comment on that.
There was a problem hiding this comment.
Well, if you don't need the substitution, it does unify things. But since we need the resulting substitution, compute mutates the substitution pretty much everywhere.
Co-authored-by: Kukovec <jure.kukovec@gmail.com>
Closes #1622. This PR implements type unification for rows as part of the meta-issue #401. Unification for new records and variants is very simple: It delegates to row unification. The idea is described in ADR014. However, our unification is much simpler. We do not need kinds, scoped labels, etc.
This version does not require different options of a variant type to have compatible fields, as discussed in Section 5.4. Postponing this decision until implementing the rewriting rules in the model checker. Perhaps, we do not need this requirement.
make fmt-fix(or had formatting run automatically on all files edited)