# How can finite sets be represented as a type?

Manually self-migrated from stack overflow.

A set of objects of a type T is often represented using its indicator function (set T = T -> bool). However, for practical purposes this representation isn't necessarily very useful. For instance, if T is the natural numbers, there's no way to print0 out all of the numbers in a given set, since it would require checking all of the natural numbers, which is an infinite task.1

However, say I'm only interested in finite sets, and I want to be able to print out all the members of a set. (Obviously I also want to easily test membership, construct unions and intersections, etc.) Is there a good way to do this using inductive types?

Edit:
To clarify, I need the set type to encapsulate all of the set invariants (no duplicates, unordered, etc) so that all members of that type automatically satisfy those properties. The indicator function representation does this, but is impractical to use as a data structure for the above reasons. Using sorted lists (set T = list T) is possible, but not all lists are valid (sorted without duplicates) representation of a set—I need the type system to enforce that all members of set T are actually sets.

0: Let's assume we're using some monad to encapsulate printing, etc.
1: In exchange, we do of course get the ability to represent infinite sets.

• Is there something wrong with a usual list/tree? Oct 27, 2014 at 17:49
• How general are your sets? Do they come from some range? Are they always even numeric?
– Juho
Oct 27, 2014 at 18:13
• @KarolisJuodelė Lists are ordered and can contain duplicates, so different representations of a set wouldn't be definitionally equal. I'm not sure how you'd use a tree---perhaps you could post that as an answer?
– lily
Oct 27, 2014 at 18:21
• I think there are implicit restrictions to this question (esp. in the title); you better make them explicit. There are well-known representations, e.g. sorted lists without duplicates, but you seem to want to define a type using only a limited set of basic types as building blocks. Oct 27, 2014 at 18:22
• @Juho I was hoping for a solution for any type T, possibly infinite, but numericity (is that a word?) is of course a reasonable constraint.
– lily
Oct 27, 2014 at 18:23

If you want a type system for finite sets that enforces the validity and unicity of all representations, then your type system must be able to model equality of elements. (Informal proof: insert x (insert y empty) has differently-shaped representations depending on whether x and y are equal.) This is impossible with algebraic datatypes alone, unless you're willing to restrict the domain of the sets to sufficiently simple sets (for example, you can use a bit vector to represent a finite subset of a finite set; you can use finite lists of positive integers to get a unique representation of finite sets of positive integers: store $\{x_1, \ldots, x_n\}$ as $[x_1, x_2-x_1, \ldots, x_n-x_{n-1}]$ where the $x_i$ are numbered in increasing order).
If you're willing to relinquish either the requirement for unicity or for validity, you can make do with algebraic datatypes. Representing finite sets as finite lists yields a set representation where every datum is valid, but each set admits multiple representation ($n!$ representations for an $n$-element set if the elements have unique representations). Something like a sorted list or search tree can give a unique representation (assuming that the elements have a unique representation). For search trees, to have representation unicity, you need a balancing function that guarantees unicity (which may impact performance).