@@ -84,8 +84,8 @@ explores these downsides and how we addressed them.
8484## The trouble with laziness
8585
8686As we described above, lazy BDDs allow us to represent set-theoretic
87- operations at any depth. And while this is extremely useful for unions
88- and differences, they offer a downside when it comes to intersections.
87+ operations at any depth. And while this is useful in many cases,
88+ they offer a downside when it comes to intersections.
8989For example, take this type:
9090
9191``` elixir
@@ -179,7 +179,7 @@ but that may not always be the case.
179179To discuss exactly when these trade-offs may be problematic, let's talk about open vs
180180closed types.
181181
182- ### Open vs closed types
182+ ## Open vs closed types
183183
184184Elixir's type system can represent both open and closed maps. When you write:
185185
@@ -214,139 +214,6 @@ if they were closed maps, the end result would be empty. For this reason,
214214we recommend applying the eager literal intersection only when the
215215intersection will often lead to empty types.
216216
217- ## Optimizing differences
218-
219- The difference between `B1 \ B2 ` can always be expressed as the intersection
220- between `B1 ` and `not B2 `, which is precisely how we write differences in Elixir .
221-
222- Now take the following type:
223-
224- ```elixir
225- {:ok , integer ()} and not {:error , integer ()}
226- ```
227-
228- Currently , both `ok`- type and `error`- type are stored as nodes in the BDD .
229- However , it is clear in the example above the types are disjoint and the
230- result is `{:ok , integer ()}`.
231-
232- If we know the literals `a1` and `a2` are disjoint (their intersection is
233- empty), then it is likely we can avoid adding nodes to the tree.
234-
235- Furthermore , imagine this type:
236-
237- ```elixir
238- {:ok , integer ()} and not (not {:error , integer ()})
239- ```
240-
241- The difference will convert the negation into a positive, resulting in
242- `{:ok , integer ()} and {:error , integer ()}`, which is empty. Therefore ,
243- if `B2 ` contains negations (which means its `D2 ` component is not bottom),
244- then we can also apply the eager literal intersection optimization from
245- the previous section.
246-
247- We will explore both scenarios next, starting with the one where D2
248- is bottom.
249-
250- ## # When `D2` is bottom
251-
252- We start `B1 and not B2 `:
253-
254- ```elixir
255- B1 and not B2
256- ```
257-
258- Next let' s break `B1` into `(a1 and C1) or B1_no_C1`, where `B1_no_C1` is `U1 or (not a1 and D1)`:
259-
260- ```elixir
261- ((a1 and C1) or B1_no_C1) and not B2
262- ```
263-
264- Now we distribute the difference:
265-
266- ```elixir
267- ((a1 and C1) and not B2) or (B1_no_C1 and not B2)
268- ```
269-
270- Let' s solve the left- hand side. We know `B2 = (a2 and C2 ) or U2 ` (remember `D2 ` is bottom), so let' s add that:
271-
272- ```elixir
273- (a1 and C1 and not ((a2 and C2) or U2))
274- or (B1_no_C1 and not B2)
275- ```
276-
277- Now distribute the `not` and remove the parenthesis:
278-
279- ```elixir
280- (a1 and C1 and not (a2 and C2) and not U2)
281- or (B1_no_C1 and not B2)
282- ```
283-
284- Now, **if `a1` and `a2` are disjoint**, then `a1 and not (a2 and C2)` is the same as `a1`.
285- This happens because if `a1` and `a2` are disjoint, `a2 and C2` is a subset of `a2`,
286- which is then also disjoint with `a1`. So the first part simplifies to `a1 and C1 and not U2`:
287-
288- ```elixir
289- (a1 and C1 and not U2) or (B1_no_C1 and not B2)
290- ```
291-
292- Now by expanding `B1_no_C1` into `U1 or (not a1 and D1)` and distributed
293- the union, we get:
294-
295- ```elixir
296- (a1 and C1 and not U2) or (U1 and not B2) or (not a1 and D1 and not B2)
297- ```
298-
299- which is in the BDD format! So we can rewrite the difference of disjoint literals as:
300-
301- ```elixir
302- {a1, C1 and not U2, U1 and not B2, D1 and not B2}
303- ```
304-
305- which completely avoids adding `a2` to the BDD and can then continue recursively.
306-
307- ### When `D2` is not bottom
308-
309- When D2 is not bottom, it means B2 has a negated component.
310- Since B2 itself is negated when part of a difference, the D2
311- component of B2 becomes an intersection, and we can apply the
312- same eager literal technique we applied to intersections.
313-
314- Once again, we start `B1 and not B2`:
315-
316- ```elixir
317- B1 and not B2
318- ```
319-
320- Now let' s break `B2 ` into `(B2_no_D2 or (not a2 and D2 ))`, where `B2_no_D2 ` is `(a2 and C2 ) or U2 `:
321-
322- ```elixir
323- (B1 ) and not (B2_no_D2 or (not a2 and D2 ))
324- ```
325-
326- Now we distribute the negation all the way through:
327-
328- ```elixir
329- (B1 ) and (not B2_no_D2 and (a2 or not D2 ))
330- ```
331-
332- And distribute `B1 `' s intersection with `(a2 or not D2)`:
333-
334- ```elixir
335- ((B1 and a2) or (B1 and not D2)) and not B2_no_D2
336- ```
337-
338- `B1 and a2` is an eager literal intersection from the previous section,
339- which we can reuse!
340-
341- Furthermore, notice at the end we compute the difference between
342- `((B1 and a2) or (B1 and not D2))` and `B2_no_D2`. Given `B2_no_D2`
343- by definition has `D2 = bottom`, we can apply the optimized
344- difference for when D2 is bottom.
345-
346- At the moment, we are not applying this optimization in Elixir,
347- as the difference with negations on the right-hand side are uncommon.
348- We may revisit this in the future.
349-
350217## Results
351218
352219We initially [implemented eager literal intersections as part of
0 commit comments