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.