How can finite sets be represented as a type?

Question

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 print⁰ out all of the numbers in a given set, since it would require checking all of the natural numbers, which is an infinite task.¹

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

Answer 1

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

A sophisticated type system can of course represent anything you want. Basically, you need:

• dependent types, so that the type definition can contain equality assertions;
• induction, to build a data structure containing any number of elements.

For example, the calculus of inductive constructions admits representations of finite sets. You can look for examples in the Coq library and contributions.

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

In the type systems found in typical programming languages, it is typical to implement sets with an underlying representation that may or may not be valid. The type system thus does not enforce that all representations are valid. It does, however, help to maintain this property: a finite set can be implemented as an abstract type. The type is implemented as a module which is sealed, ensuring that all elements of the finite set type have been built from constructors provided by the module. The correctness of the finite set modle code ensures the validity of set representations, and the type system helps by maintaining this invariant.