Можно ли определить тип данных, который хранит лямбда-функцию, которая имеет тот же тип данных, что и параметр? - PullRequest
Новая
       17

Можно ли определить тип данных, который хранит лямбда-функцию, которая имеет тот же тип данных, что и параметр?

2 голосов
/ 17 мая 2019

Я пытаюсь создать тип данных, который содержит лямбда-функцию, которая принимает тот же тип данных, что и аргумент.

Вот пример: 

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)]"

Идея кода состоит в том, чтобы иметь список кортежей с идентификатором и выражением. Выражение реализуется лямбда-функцией, которая может получить список того же самого формата. Функции search и ivalue позволяют ссылаться на другие записи в выражении. Ожидаемый результат алгоритма, который оценивает все выражения в my_list, будет [(n_1, 42), (n_2, 48)].

Определение entry явно неверно, но, надеюсь, проясняет, чего я пытаюсь достичь. Есть ли способ создать такой тип данных?

1 Ответ

2 голосов
/ 17 мая 2019

Это невозможно, потому что это было бы математически непоследовательным.Проще говоря, такой тип данных был бы слишком большим, чтобы поместиться в набор.(Если это так, можно легко построить инъекцию из блока питания этого типа в себя)

Более подробное объяснение можно найти, например, здесь .

Еслифункции, которые вы хотите сохранить, имеют ограниченный домен (например, конечный или счетный), возможно, можно заставить это работать.Я бы наивно думал, что будет работать конечная карта: 

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

Но, очевидно, это не так.Я не уверен, что это из-за глубокой логической проблемы или просто потому, что fmap не был настроен должным образом для поддержки этого.Я подозреваю, что это последнее, так как работает следующая похожая вещь: 

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

Вам достаточно конечной карты?

...