How can finite sets be represented as a type?
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.