# From Type Theory to Set Theory

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.

• Do you actually use lower case L as variable names in programs? While also using uppercase L to refer something else? Commented Mar 2, 2017 at 20:53
• EDIT: now $\ell$ stands for the $l$ in lowercase in the program. Commented Mar 2, 2017 at 21:53
• $l$ and $e$ stand for a Algebraic Data Type definition, while the ones in upper case are the types costructor. Commented Mar 2, 2017 at 21:55

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.

• So, given that my $\ell$ is just your NestedSet and $\mathbb{ID}$ is your A, at the end of the road, is more like $\ell \overset{def}{=} ((\mathbb{ID} \cup \ell)\ \times \ell)$, isn't it? Commented Mar 14, 2017 at 16:39
• I'm not sure what the intuition behind your $\mathbb{ID}$ is, but A is just whatever the elements of the set are (i.e. although nested, these sets are still homogeneous, for heterogeneous nested sets you would have to define it a bit differently). In OCaml it would be something like type a nestedset = Nested of ((a nestedset, a) either) list if I'm not butchering the syntax (not very experienced with the language). Commented Mar 14, 2017 at 17:45
• If $\cup$ denotes a binary disjoint union, $\times$ a binary product, and $1$ a unit type, then we can describe the a list type (now with a more ocaml-like notation) as $a \; list = a \times (a \; list) \cup 1$ (A list of as is either the cons cell of an an element of type a and another a list, or the empty list), so then we could say $\mathrm{a \; nestedset} = ((\mathrm{a \; nestedset}) \cup a) \; list$ I'm sure there's a way to write this type as a single definition in OCaml (without using lists), but they're a part of the core language, so why not use them? Commented Mar 14, 2017 at 17:50
• So, if I understand, you want to distinguish (for example) the first occurrence of $\{ 1, 2\}$ in $\{ \{ 1, 2 \}, 3, \{ 1, 2 \} \}$ from the second one, which is your purpose for including an identifier for each branching? Commented Mar 14, 2017 at 18:11
• In that case, I don't know if any more data needs to be specified than what is already in NestedList a. Without imposing an equivalence relation on the type, we don't in fact have the usual set-theoretic identities, e.a. $\{ \{ 1, 2\},3,\{1,2\} \} \neq \{ \{1,2\},3\}$, so the structure of the datatype itself already distinguishes different occurrences of sublists. But if you want a way to refer to different occurrences (in order to modify them, perhaps), I don't think your approach is ideal either -- you want unique identifiers for each occurrence, and your type doesn't enforce that. Commented Mar 14, 2017 at 18:31