Почему индуктивные типы данных запрещают типы типа `data Bad a = C (Bad a → a)`, где рекурсия типа встречается перед ->?

Ответ 1

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

data Bad : Set where
  bad : (Bad → Bad) → Bad

unbad : Bad → (Bad → Bad)
unbad (bad f) = f

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

 e := x | \x. e | e e'

Мы можем определить перевод [[e]] из нетипизированных членов лямбда-исчисления в члены Agda типа Bad (хотя и не в Agda):

[[x]]     = x
[[\x. e]] = bad (\x -> [[e]])
[[e e']]  = unbad [[e]] [[e']]

Теперь вы можете использовать свой любимый не-завершающий нетипизированный лямбда-член для создания термина без терминов типа Bad. Например, мы могли бы перевести (\x. x x) (\x. x x) в выражение без конца следующего типа Bad ниже:

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x))

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

Ответ 2

Пример того, как такой тип данных позволяет нам населять любой тип, дается в Turner, D.A. (2004-07-28), Полное функциональное программирование, раздел. 3.1, стр. 758 в Правиле 2: Рекурсия типа должна быть ковариантной. "

Давайте сделаем более подробный пример использования Haskell. Мы начнем с "плохого" рекурсивного типа данных

data Bad a = C (Bad a -> a)

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

Y combinator в нетипизированном лямбда-исчислении определяется как

Y = λf.(λx.f (x x)) (λx.f (x x))

Ключ к этому заключается в том, что мы применяем x к себе в x x. На типизированных языках это невозможно, потому что не существует допустимого типа x. Но наш тип данных Bad позволяет этому модулю добавлять/удалять конструктор:

selfApp :: Bad a -> a
selfApp ([email protected](C x')) = x' x

Взяв x :: Bad a, мы можем развернуть его конструктор и применить функцию внутри к x. Как только мы знаем, как это сделать, легко построить Y combinator:

yc :: (a -> a) -> a
yc f =  let fxx = C (\x -> f (selfApp x))  -- this is the λx.f (x x) part of Y
        in selfApp fxx

Обратите внимание, что ни selfApp, ни yc не являются рекурсивными, рекурсивный вызов функции невозможен. Рекурсия появляется только в нашем рекурсивном типе данных.

Мы можем проверить, что построенный комбинатор действительно делает то, что должен. Мы можем сделать бесконечный цикл:

loop :: a
loop = yc id

или вычислить let say GCD:

gcd' :: Int -> Int -> Int
gcd' = yc gcd0
  where
    gcd0  :: (Int -> Int -> Int) -> (Int -> Int -> Int)
    gcd0 rec a b  | c == 0     = b
                  | otherwise  = rec b c
      where c = a `mod` b