mirror of
https://github.com/roc-lang/roc.git
synced 2025-08-03 11:52:19 +00:00
Use strict unification of vars in unspecialized lambda sets right now
This commit is contained in:
Ayaz Hafiz
parent
a1152934f5
commit
ebcd323449
5 changed files with 192 additions and 66 deletions
|
|
@ -547,26 +547,113 @@ How do we make this a type error? A couple options have been considered, but we
|
|||
1. One approach, suggested by Richard, is to sort abilities into strongly-connected components and see if there is any zig-zag chain of member signatures in a SCC where an ability-bound type variable doesn’t escape through the front or back. We can observe two things: (1) such SCCs can only exist within a single module because Roc doesn’t have (source-level) circular dependencies and (2) we only need to examine pairs of functions have at least one type variable only appearing on one side of an arrow. That means the worst case performance of this analysis is quadratic in the number of ability members in a module. The downside of this approach is that it would reject some uses of abilities that can be resolved and code-generated by the compiler.
|
||||
2. Another approach is to check whether generalized variables in a let-bound definition’s body escaped out the front or back of the let-generalized definition’s type (and **not** in a lambda set, for the reasons described above). This admits some programs that would be illegal with the other analysis but can’t be performed until typechecking. As for performance, note that new unbound type variables in a body can only be introduced by using a let-generalized symbol that is polymorphic. Those variables would need to be checked, so the performance of this approach on a per-module basis is linear in the number of let-generalized symbols used in the module (assuming the number of generalized variables returned is a constant factor).
|
||||
|
||||
## A Nice Property
|
||||
## A Property that’s lost, and how we can hold on to it
|
||||
|
||||
One question I asked myself was, does this still ensure lambda sets can vary over multiple able type parameters? I believe the answer is yes. Unfortunately the traces are terribly long so I won’t bore you with that, but as a simple example consider
|
||||
One question I asked myself was, does this still ensure lambda sets can vary over multiple able type parameters? At first, I believed the answer was yes — however, this may not hold and be sound. For example, consider
|
||||
|
||||
```python
|
||||
Go has go : a -> ({} -> {}) | a has Go
|
||||
J has j : j -> (k -> {}) | j has J, k has K
|
||||
K has k : k -> {} | k has K
|
||||
|
||||
f = \flag, a, b ->
|
||||
when flag is
|
||||
A -> go a
|
||||
B -> go b
|
||||
C := {}
|
||||
j = \@C _ -> k
|
||||
|
||||
D := {}
|
||||
j = \@D _ -> k
|
||||
|
||||
E := {}
|
||||
k = \@E _ -> {}
|
||||
|
||||
f = \flag, a, b, c ->
|
||||
it = when flag is
|
||||
A -> j a
|
||||
B -> j b
|
||||
it c
|
||||
```
|
||||
|
||||
`f` has type
|
||||
The first branch has type (`a` has generalized type `a'`)
|
||||
|
||||
```python
|
||||
f : [A, B], a, b -[f]-> ({} -[[] + a:go:2, b:go:2]-> {})
|
||||
```
|
||||
c'' -[[] + a':j:2]-> {}
|
||||
```
|
||||
|
||||
Now no matter how you resolve the type variables for `a` or `b`, or in what order, their specialization lambda sets will be resolved independently. So the single-variable traces I showed previously compose in the presence of multiple variables without additional work.
|
||||
The second branch has type (`b` has generalized type `b'`)
|
||||
|
||||
```
|
||||
c''' -[[] + b':j:2]-> {}
|
||||
```
|
||||
|
||||
So now, how do we unify this? Well, following the construction above, we must unify `a'` and `b'` - but this demands that they are actually the same type variable. Is there another option?
|
||||
|
||||
Well, one idea is that during normal type unification, we simply take the union of unspecialized lambda sets with **disjoint** variables. In the case above, we would get `c' -[[] + a':j:2 + b':j:2]` (supposing `c` has type `c'`). During lambda set compaction, when we unify ambient types, choose one non-concrete type to unify with. Since we’re maintaining the invariant that each generalized type variable appears at least once on one side of an arrow, eventually you will have picked up all type variables in unspecialized lambda sets.
|
||||
|
||||
```
|
||||
=== monomorphize (f A (@C {}) (@D {}) (@E {})) ===
|
||||
(inside f, solving `it`:)
|
||||
|
||||
it ~ E -[[] + C:j:2 + D:j:2]-> {}
|
||||
<specialization time: C>
|
||||
step 1:
|
||||
uls_C = { [[] + C:j:2 + D:j:2] }
|
||||
step 2:
|
||||
uls_C = { [[] + C:j:2 + D:j:2] } (sorted)
|
||||
step_3:
|
||||
1. iteration: [[] + C:j:2 + D:j:2]
|
||||
E -[[] + D:j:2]-> {} (t_f1 after removing C:j:2)
|
||||
~ k' -[[] + k':k:2]-> {}
|
||||
= E -[[] + E:k:2 + D:j:2]-> {} (no non-concrete type to unify with)
|
||||
=> E -[[] + E:k:2 + D:j:2]-> {}
|
||||
<specialization time: D>
|
||||
step 1:
|
||||
uls_D = { [[] + E:k:2 + D:j:2] }
|
||||
step 2:
|
||||
uls_D = { [[] + E:k:2 + D:j:2] } (sorted)
|
||||
step_3:
|
||||
1. iteration: [[] + E:k:2 + D:j:2]
|
||||
E -[[] + E:k:2]-> {} (t_f1 after removing D:j:2)
|
||||
~ k'' -[[] + k'':k:2]-> {}
|
||||
= E -[[] + E:k:2 + E:k:2]-> {} (no non-concrete type to unify with)
|
||||
=> E -[[] + E:k:2 + E:k:2]-> {}
|
||||
<specialization time: E>
|
||||
step 1:
|
||||
uls_E = { [[] + E:k:2], [[] + E:k:2] }
|
||||
step 2:
|
||||
uls_E = { [[] + E:k:2], [[] + E:k:2] } (sorted)
|
||||
step_3:
|
||||
1. iteration: [[] + E:k:2]
|
||||
E -[[]]-> {} (t_f1 after removing E:k:2)
|
||||
~ E -[[lamE]]-> {}
|
||||
= E -[[lamE]]-> {}
|
||||
=> E -[[lamE]]-> {}
|
||||
=> E -[[lamE]]-> {}
|
||||
|
||||
== final type of it ==
|
||||
it : E -[[lamE]]-> {}
|
||||
```
|
||||
|
||||
The disjointedness is important - we want to unify unspecialized lambdas whose type variables are equivalent. For example,
|
||||
|
||||
```
|
||||
f = \flag, a, c ->
|
||||
it = when flag is
|
||||
A -> j a
|
||||
B -> j a
|
||||
it c
|
||||
```
|
||||
|
||||
Should produce `it` having generalized type
|
||||
|
||||
```
|
||||
c' -[[] + a':j:2]-> {}
|
||||
```
|
||||
|
||||
and not
|
||||
|
||||
```
|
||||
c' -[[] + a':j:2 + a':j:2]-> {}
|
||||
```
|
||||
|
||||
For now, we will not try to preserve this property, and instead unify all type variables with the same member/region in a lambda set. We can improve the status of this over time.
|
||||
|
||||
# Conclusion
|
||||
|
||||
|
|
|
|||
|
|
@ -1492,33 +1492,33 @@ fn solve(
|
|||
// https://github.com/rtfeldman/roc/issues/3207 is resolved, this may be redundant
|
||||
// anyway.
|
||||
&Resolve(OpportunisticResolve {
|
||||
specialization_variable: _,
|
||||
specialization_expectation: _,
|
||||
member: _,
|
||||
specialization_id: _,
|
||||
specialization_variable,
|
||||
specialization_expectation,
|
||||
member,
|
||||
specialization_id,
|
||||
}) => {
|
||||
// if let Some(Resolved::Specialization(specialization)) =
|
||||
// resolve_ability_specialization(
|
||||
// subs,
|
||||
// abilities_store,
|
||||
// member,
|
||||
// specialization_variable,
|
||||
// )
|
||||
// {
|
||||
// abilities_store.insert_resolved(specialization_id, specialization);
|
||||
if let Some(Resolved::Specialization(specialization)) =
|
||||
resolve_ability_specialization(
|
||||
subs,
|
||||
abilities_store,
|
||||
member,
|
||||
specialization_variable,
|
||||
)
|
||||
{
|
||||
abilities_store.insert_resolved(specialization_id, specialization);
|
||||
|
||||
// // We must now refine the current type state to account for this specialization.
|
||||
// let lookup_constr = arena.alloc(Constraint::Lookup(
|
||||
// specialization,
|
||||
// specialization_expectation,
|
||||
// Region::zero(),
|
||||
// ));
|
||||
// stack.push(Work::Constraint {
|
||||
// env,
|
||||
// rank,
|
||||
// constraint: lookup_constr,
|
||||
// });
|
||||
// }
|
||||
// We must now refine the current type state to account for this specialization.
|
||||
let lookup_constr = arena.alloc(Constraint::Lookup(
|
||||
specialization,
|
||||
specialization_expectation,
|
||||
Region::zero(),
|
||||
));
|
||||
stack.push(Work::Constraint {
|
||||
env,
|
||||
rank,
|
||||
constraint: lookup_constr,
|
||||
});
|
||||
}
|
||||
|
||||
state
|
||||
}
|
||||
|
|
@ -2081,7 +2081,6 @@ fn compact_lambda_set<P: Phase>(
|
|||
Some { t_f2: Variable },
|
||||
// The specialized lambda set should actually just be dropped, not resolved and unified.
|
||||
Drop,
|
||||
// NotYetSpecialized,
|
||||
}
|
||||
|
||||
let spec = match subs.get_content_without_compacting(c) {
|
||||
|
|
@ -2119,9 +2118,10 @@ fn compact_lambda_set<P: Phase>(
|
|||
}
|
||||
}
|
||||
Err(DeriveError::UnboundVar) => {
|
||||
// not specialized yet
|
||||
todo!()
|
||||
// Spec::NotYetSpecialized
|
||||
// not specialized yet, but that also means that it can't possibly be derivable
|
||||
// at this point?
|
||||
// TODO: is this right? Revisit if it causes us problems in the future.
|
||||
Spec::Drop
|
||||
}
|
||||
Err(DeriveError::Underivable) => {
|
||||
// we should have reported an error for this; drop the lambda set.
|
||||
|
|
@ -2193,9 +2193,6 @@ fn compact_lambda_set<P: Phase>(
|
|||
};
|
||||
|
||||
match spec {
|
||||
// Spec::NotYetSpecialized => {
|
||||
// // Do nothing; no compaction ready yet.
|
||||
// }
|
||||
Spec::Some { t_f2 } => {
|
||||
// Ensure the specialization lambda set is already compacted.
|
||||
// if subs.get_root_key(specialized_lambda_set) != subs.get_root_key(this_lambda_set) {
|
||||
|
|
|
|||
|
|
@ -7281,8 +7281,7 @@ mod solve_expr {
|
|||
&[
|
||||
"Fo#f(10) : Fo, b -[[f(10)]]-> ({} -[[13(13) b]]-> ({} -[[] + b:g(8):2]-> {})) | b has G",
|
||||
"Go#g(11) : Go -[[g(11)]]-> ({} -[[14(14)]]-> {})",
|
||||
// TODO this is wrong: why is there a unspecialized lambda set left over?
|
||||
"Fo#f(10) : Fo, Go -[[f(10)]]-> ({} -[[13(13) Go]]-> ({} -[[14(14)]]-> {})) | b has G",
|
||||
"Fo#f(10) : Fo, Go -[[f(10)]]-> ({} -[[13(13) Go]]-> ({} -[[14(14)]]-> {}))",
|
||||
],
|
||||
);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue