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?

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.

  • $\begingroup$ Is there something wrong with a usual list/tree? $\endgroup$ Oct 27, 2014 at 17:49
  • 1
    $\begingroup$ How general are your sets? Do they come from some range? Are they always even numeric? $\endgroup$
    – Juho
    Oct 27, 2014 at 18:13
  • $\begingroup$ @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? $\endgroup$
    – lily
    Oct 27, 2014 at 18:21
  • 1
    $\begingroup$ 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. $\endgroup$
    – Raphael
    Oct 27, 2014 at 18:22
  • $\begingroup$ @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. $\endgroup$
    – lily
    Oct 27, 2014 at 18:23

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.