[Haskell-cafe] Explanation of Data.Set, please

[MigMit]

What is called "Set" in Prelude is not "set" in a set-theoretic meaning. It is a finite set. Not sure what you mean by "ZFC-friendly", since it is not a "concept of set theory" at all.

It is represented that way for efficiency; balanced trees generally guarantee O(log n) performance, while a list would give you O(n).

> On 2 Aug 2021, at 00:12, Galaxy Being <borgauf at gmail.com> wrote:
> 
> I'm looking at this code and wondering, first, about the strategy behind the data type Set itself
> 
> data Set a    = Bin {-# UNPACK #-} !Size !a !(Set a) !(Set a) | Tip
> 
> It says it's a "balanced tree." I found this talking about maybe why that is. Will read. But in the meantime, any explanation in plain English as to why we're doing it as a tree and not some other structure would be helpful. And why are we bringing Size along, and in general, why all the strictness !'s? All this might have something to do with why a balanced tree is better than quick-and-dirty list representation like I see in beginner tutorials? Next, is this ZFC? I've seen treatments that supposedly are ZFC-friendly. Finally, I've taken a preliminary look at Agda, and right from the start there's Set, and no doubt an entirely alternative, category universe approach to the concept of set theory. Any contrast and compare between Haskell and Agda's set notions would be appreciated. Haskell seems to dance in and out of Category Theory, while Agda seems pretty much just CT....
> 
> -- 
> ⨽
> Lawrence Bottorff
> Grand Marais, MN, USA
> borgauf at gmail.com
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.