Lazier Binary Decision Diagrams for set-theoretic types
elixir-lang.org45 points by tvda 12 hours ago
45 points by tvda 12 hours ago
I am a little confused on the idea that the "C [node] appears twice" in the diagram. I would expect that both of those are the same node such that the standard BDD implementation would already have reduced those. Though, my understanding for BDD is more that a label will only appear once per path to TOP/BOTTOM. Not that they only appear once per diagram.
Fun to consider how to use these for type checking. I hope to spend a lot more time reading more on this. Love that one of the linked papers has exercises in the appendix.
You are right, poor phrasing on my side. Instead of focusing on C appearing twice, I should rather focus on how complex the expansion is, meaning that everytime we have to expand the BDD (which we need to do during subtyping or emptiness for example), we end-up doing a lot of repeated operations. I will push an update, thank you for commenting.
Kudos on the article! My understanding on BDDs is sadly not as strong as I would prefer it to be, so I'm guessing I am not quite caught up on how they are being used here.
I think I was expecting to see the algorithm for merging multiple BDDs that I saw in Knuth's work. Though, in that regard, I would expect a ZDD approach would be a lot easier to start with. That or you would have to make the BDD to merge be a big chain of every variable before the stuff to be merged where true goes to BOTTOM, and false goes to the next variable before new first to merge.
Again, kudos on this. I do look forward to trying to understand it more!
Shouldn't it be:
``` type lazy_bdd() = :top or :bottom or {type(), constrained :: lazy_bdd(), uncertain :: lazy_bdd(), dual :: lazy_bdd()} ```
(where the members are `lazy_bdd()` instead of `bdd()`?)