From Type Theory to Set Theory

Question

I have to provide the definition of a arbitrarly nested data set with recursive types so that I do not fall in the Russel's paradox by its definition. The implementation in OCaml that came into my mind is the following one (*):

type e = E of id | L of l
and l = B of id | I of e * l;;

This means that:

• e is a type that could be either an id or a list l, where:
• any list l is a list of elements in e, terminated by an id

Since it is typed in OCaml, I assume that this definition is compliant. This means that, if I want to reproduce the data structure:

$$\{\{1,2\}_{B=55},3,4,\{6\}_{B=66}\}_{B=0}$$

then I could write something like:

I (L (I (E 1, I (E 2, B 55))), I (
   E 3, I (
   E 4, I (
   L (I (E 6, B 66)), 
B 0))))

Since I want to provide the most intuitive definition of (*) that could be read by any person that does not know type theory but only knows set theory, I'm wondering how to express a recursive data type in such theory. Please note that my target are people not coming from logic field, so they understand set theory but do not understand type theory. Moreover, the set theory used must be the most simple as possible.

I was trying to define something like this:

$$\begin{cases} e \overset{def}{=} (\mathbb{ID}\times\{\textbf{0}\} \cup \ell\times\{\textbf{1}\})\\ \ell \overset{def}{=} \mathbb{ID}\times\{\textbf{0}\} \cup (e \times \ell)\times\{\textbf{1}\}\\ \end{cases}$$

Is there something more simple and intuitive in order to represent nested-well-typed set within set theory?

EDIT

This means that, even supposing that I could always distinguish and id ($\mathbb{ID}$) from a list ($L$) and hence supposing that even this other solution is acceptable:

$$\ell \overset{def}{=} \mathbb{ID} \cup ((\mathbb{ID} \cup \ell)\ \times \ell)$$

I'm still wondering if if there is something more simple than that.

Answer 1

There is a standard way of representing arbitrarily nested sets inside a type theory -- this is done by reprenting sets as pointed graphs with bisimulation giving the equality between "sets". (This was first done, I think, by Miquel)

As for implementing this in an actual programming language, probably the best way is by considering a very particular type of pointed graph -- a tree structure! In Haskell, for instance, you might define:

data NestedSet A = Nesting [Either (NestedSet A) A]

For example, we might represent $\{ \{ 1, 2 \}, 3, 4, \{ 6 \} \}$ as:

Nesting [Left (Nesting [1,2]), Right 3, Right 4, Left (Nesting [6])]

Intuitively, to give a (finite) set, we may simply list its elements, so we do so with the Nesting constructor, and the elements of a nested set may either be simple elements A, or other nested sets NestedSet A.