FRESH

Hacker News

Lazier Binary Decision Diagrams for set-theoretic types

51 points by tvda

by taeric

1 subcomments

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.

by MarkusQ

1 subcomments

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()`?)