You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Clarified the discussion on eager literal intersections and their implications. Added details on potential pitfalls and examples of trade-offs in type systems.
Copy file name to clipboardExpand all lines: _posts/2026-02-26-eager-literal-intersections.markdown
+14-16Lines changed: 14 additions & 16 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -154,30 +154,28 @@ If `a1 and a2` is empty, then the whole C1 node can be eliminated.
154
154
155
155
Then we proceed recursively intersect `a2` with every literal node in `a2 and U1`
156
156
and `a2 and D1`. And, if their literal nodes are empty, those subtrees are eliminated
157
-
too. This allows us to dramatically cut down the size of tree! In our benchmarks,
157
+
too. This may allows us to cut down the size of tree considerably! In our benchmarks,
158
158
these optimizations allowed us to reduce type checking of a module from 10s to
159
159
25ms.
160
160
161
161
The remaining terms of the union are `U2 and B1` and `(not a2 and D2) and B1`.
162
162
If desired, we could apply the same eager literal intersection optimization to
163
163
`U2 and B1` (as long as the constrained part in either `U2` or `B1 ` are `:top`).
164
164
165
-
This optimization has worked quite well for us, but it is important to keep in
166
-
mind since BDDs are ordered and the literal intersection may create a new literal
167
-
value, this optimization must be applied semantically so we can recompute the
168
-
position of intersected literals in the tree. We cannot apply it when we are
169
-
already traversing the tree using the general lazy BDD formulas from the previous
170
-
article.
165
+
This optimization has worked quite well for us but there are some pitfalls one
166
+
must be aware of. The first of them is to consider how expensive it is to compute
167
+
that the literal intersection is empty. Since this is an optimization, the check
168
+
itself does not have to be complete and you can optimize only certain idioms.
171
169
172
-
Finally, note this optimization may eagerly reintroduce some of the complexity seen
173
-
in DNFs if applied recursively. For instance, if you have `(foo or bar) and (baz or bat)`,
174
-
the recursive application of eager literal intersections will yield
175
-
`(foo and baz) or (foo and bat) or (bar and baz) or (bar and bat)`. If most of those
176
-
intersections are eliminated, then applying eager literal intersections is still beneficial,
177
-
but that may not always be the case.
170
+
Another option is to have the "eager literal intersection" always compute a new
171
+
literal, which is then reinserted into the BDD. This is the approach done by
172
+
the Elixir compiler but one has to be additionally careful because, if a new
173
+
literal node is computed, then it has to be resorted within the BDD, which may be
174
+
too expensive. If most of the intersections are eliminated, then computing the eager
175
+
literal intersections is still beneficial, but that may not always be the case.
178
176
179
-
To discuss exactly when these trade-offs may be problematic, let's talk about open vs
180
-
closed types.
177
+
Let's explore one example where these trade-offs may be problematic by discussing
178
+
open vs closed types.
181
179
182
180
## Open vs closed types
183
181
@@ -225,4 +223,4 @@ from 10 seconds to 25ms!
225
223
However, our initial implementation also caused a performance regression,
226
224
as we did not distinguish between open and closed maps. This regression was
227
225
addressed by [applying the optimization only to closed maps](https://github.com/elixir-lang/elixir/commit/e5dc69398ef172b4a590e7e4e20f9d52b4b7ab59), as discussed
0 commit comments