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