Can a data type be defined which stores a lambda function that has the same data type as parameter?

Question

I'm trying to create a data type which contains a lambda function which takes the same data type as argument.

Here is an example:

datatype id = n_1 | n_2

type_synonym entry = "(id * (entry list ⇒ nat))"
type_synonym myList = "entry list"

fun ivalue :: "myList ⇒ nat"
  where
    "ivalue [] = 0" |
    "ivalue (x # xs) = snd x (x xs)"

fun search :: "myList ⇒ id ⇒ myList"
  where
    "search [] t = []" |
    "search (x # xs) t = (if fst x = t then (x # xs) else search xs t)"

definition my_list :: "myList"
  where
    "my_list = [(n_1, %p.(42::nat)),
                (n_2, %p.(ivalue (search p n_1)) + 6)]"

The idea of the code is to have list of tuples with an ID and an expression. The expression is realized by a lambda function which can get a list of the same format itself. The search and ivalue functions allow to refer to other entries in the expression. The expected result of an algorithm which evaluates all expressions in my_list would be [(n_1, 42), (n_2, 48)].

The definition of entry is obviously wrong, but hopefully makes it clear what I try to achieve. Is there a way to create such a data type?

Answer 1

This is not possible because it would be mathematically inconsistent. Simply put, such a datatype would be too large to fit into a set. (If it did, one could easily construct an injection from the power set of this type into itself)

You can find a more detailed explanation e.g. here.

If the functions you want to store have a restricted domain (e.g. finite or countable), it might be possible to get this to work. I would have naively thought that a finite map would work:

datatype entry = Entry id "(entry list, nat) fmap"

But apparently it doesn't. Whether that's due to a deep logical issue or simply because fmap wasn't set up properly to support this, I'm not sure. I suspect it is the latter though, since the following similar thing does work:

datatype entry = Entry id "(entry list × nat) fset"

Would a finite map be sufficient for you?