[HN Gopher] Lazier Binary Decision Diagrams for set-theoretic types
       ___________________________________________________________________
        
       Lazier Binary Decision Diagrams for set-theoretic types
        
       Author : tvda
       Score  : 45 points
       Date   : 2025-12-02 12:37 UTC (10 hours ago)
        
 (HTM) web link (elixir-lang.org)
 (TXT) w3m dump (elixir-lang.org)
        
       | taeric wrote:
       | 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.
        
         | josevalim wrote:
         | 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.
        
           | taeric wrote:
           | 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!
        
       | MarkusQ wrote:
       | 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()`?)
        
         | josevalim wrote:
         | Correct, I pushed a fix, should be live soon! Thank you!
        
       ___________________________________________________________________
       (page generated 2025-12-02 23:01 UTC)