Explanation of Data.Set, please

I'm looking at this https://hackage.haskell.org/package/containers-0.6.5.1/docs/src/Data.Set.Int... 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 http://groups.csail.mit.edu/mac/users/adams/BB/index.html 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@gmail.com

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
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@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.

You are asking too much from Data.Set. This module is capturing the notion of a *finite* collection of elements. It deals with a data structure view of set, where you want to use have good performance for the following operations. - lookup - insertion (no duplicate elements) - removal - cardinality - union / intersection The needs of the previous function guided the bang patterns/UNPACK on the definition of the data structure and the use of a balanced tree. -- -- Rubén. pgp: 4EE9 28F7 932E F4AD On 01-08-21 18:12, Galaxy Being wrote:
I'm looking at this https://hackage.haskell.org/package/containers-0.6.5.1/docs/src/Data.Set.Int... 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 http://groups.csail.mit.edu/mac/users/adams/BB/index.html 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....
_______________________________________________ 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.
participants (3)
-
Galaxy Being
-
MigMit
-
Ruben Astudillo