Типовая алгебра и нотная стрелка Knuth

Чтение через этот вопрос и этот пост в блоге заставил меня больше думать о типа и, в частности, как злоупотреблять им.

1) Мы можем придумать тип Either A B как дополнение: A+B

2) Мы можем представить упорядоченную пару (A,B) как умножение: A*B

3) Мы можем рассматривать функцию A -> B как возведение в степень: B^A

Здесь очевидная закономерность: умножение - это повторное добавление, а экспоненциация - повторное умножение. Это привело к Knuth для определения стрелки вверх ↑ как возведение в степень, ↑↑ как повторное возведение в степень, ↑↑↑ как повторяется ↑↑ и т.д. Таким образом, 10 ↑↑↑↑ 10 - ОГРОМНОЕ число.

Мой вопрос: как может функция ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑ быть представлена в алгебраических данных типы? Кажется, что ↑ должна быть функцией с бесконечным числом аргументов, но это не имеет большого смысла. Было бы A↑B просто [A] -> B и, таким образом, A↑↑↑↑B be [[[[A]]]]->B?

Ответы

Ответ 1

На самом очевидном уровне вы можете идентифицировать ↑↑ b с помощью

((...(a -> a) -> ...) -> a)  -- iterated b times

а ↑↑↑ b - это просто

(a↑↑(a↑↑(...(a↑↑(a↑↑a))...))) -- iterated b times

поэтому все может быть выражено в терминах некоторого длинного типа функции (следовательно, как некоторый очень длинный тип кортежа...). Но я не думаю, что есть удобное выражение для произвольного символа со стрелкой в терминах (массивности) знакомых типов Хаскелла (помимо тех, которые были написаны выше с помощью ... или ↑), так как я не могу думать любых общих математических объектов, которые имеют более крупные, чем экспоненциальные комбинаторные зависимости от размера базовых наборов (не переходя к слишком рекурсивным типам данных)... может быть, есть некоторые такие объекты в теории комбинаторных множеств? (Ваш вопрос кажется мне больше о размерах наборов, чем что-либо конкретное для типов.)

(ссылка на Википедию уже соединяет эти объекты с функцией Ackermann.)