Почему мы используем сгибы для кодирования типов данных как функций?

Question

Или, если быть точным, почему мы используем foldr для кодирования списков и итерации для кодирования чисел?

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

---

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

Это все работает, как и ожидалось, для нерекурсивных типов

--encoding data Bool = true | False
type Bool r = r -> r -> r

true :: Bool r
true = \ct cf -> ct

false :: Bool r
false = \ct cf -> cf

--encoding data Either a b = Left a | Right b
type Either a b r = (a -> r) -> (b -> r) -> r

left :: a -> Either a b r
left x = \cl cr -> cl x

right :: b -> Either a b r
right y = \cl cr -> cr y

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

--encoding data Nat = Z | S Nat
type RecNat r = r -> (RecNat -> r) -> r
zero = \cz cs -> cz
succ n = \cz cs -> cs n

-- encoding data List a = Nil | Cons a (List a)
type RecListType a r = r -> (a -> RecListType -> r) -> r
nil = \cnil ccons -> cnil
cons x xs = \cnil ccons -> ccons x xs

но мы не можем написать эти рекурсивные определения типов в Haskell! Обычное решение состоит в том, чтобы принудительно применить обратный вызов в случае cons / succ ко всем уровням рекурсии, а не только к первому (т. Е. Написать сложение / итератор). В этой версии мы используем тип возврата r где рекурсивный тип будет:

--encoding data Nat = Z | S Nat
type Nat r = r -> (r -> r) -> r
zero = \cz cf -> cz
succ n = \cz cf -> cf (n cz cf)

-- encoding data List a = Nil | Cons a (List a)
type recListType a r = r -> (a -> r -> r) -> r
nil = \z f -> z
cons x xs = \z f -> f x (xs z f)

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

Итак, на мои реальные вопросы:

1. Как мы можем быть уверены, что кодирование с использованием сгибов является таким же мощным, как и гипотетическое "кодирование по шаблону"? Есть ли способ взять произвольное определение функции с помощью сопоставления с образцом и механически преобразовать его в одно, используя вместо этого только сгибы? (Если это так, это также поможет сделать сложные определения, такие как tail или foldl, с точки зрения foldr как менее магического)

2. Почему система типов Haskell не допускает рекурсивные типы, необходимые в кодировке "сопоставление с образцом"?, Есть ли причина для того, чтобы разрешать только рекурсивные типы в типах данных, определенных с помощью data? Является ли сопоставление с образцом единственным способом непосредственного использования рекурсивных алгебраических типов данных? Связано ли это с алгоритмом вывода типа?

Answer 1

На странице Википедии о кодировке Скотта есть несколько полезных идей. Вкратце, вы имеете в виду кодировку Черча, а ваша "гипотетическая кодировка соответствия шаблону" - кодировка Скотта. Оба являются разумными способами ведения дел, но церковное кодирование требует использования более легкого механизма (в частности, он не требует рекурсивных типов).

Доказательство того, что они эквивалентны, использует следующую идею:

churchfold :: (a -> b -> b) -> b -> [a] -> b
churchfold _ z [] = z
churchfold f z (x:xs) = f x (churchfold f z xs)

scottfold :: (a -> [a] -> b) -> b -> [a] -> b
scottfold _ z [] = z
scottfold f _ (x:xs) = f x xs

scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b
scottFromChurch f z xs = fst (churchfold g (z, []) xs)
 where
  g x ~(_, xs) = (f x xs, x : xs)

Идея в том, что с churchfold (:) [] если в списках есть тождество, мы можем использовать церковную складку, которая выдает аргумент списка, который она дает, а также результат, который она должна выдать. Тогда в цепи x1 `f` (x2 `f` (... `f` xn) ... ) самый внешний f получает пару (y, x2 : ... : xn : []) (для некоторых y нас это не волнует), поэтому возвращается f x1 (x2 : ... : xn : []), Конечно, он также должен вернуться x1 : ... : xn : [] так что больше приложений f также может работать.

(Это на самом деле немного похоже на доказательство математического принципа сильной (или полной) индукции из "слабого" или обычного принципа индукции).

Кстати, ваш Bool r тип слишком велик для настоящих церковных логических выражений - например, (+) :: Bool Integer, но (+) на самом деле не церковная логика. Если вы включите RankNTypes тогда вы можете использовать более точный тип: type Bool = forall r. r -> r -> r, Теперь он вынужден быть полиморфным, поэтому действительно содержит только два (игнорируя seq и внизу) жители - \t _ -> t а также \_ f -> f, Подобные идеи применимы и к другим вашим церковным типам.

Answer 2

Учитывая некоторый индуктивный тип данных

data Nat = Succ Nat | Zero

мы можем рассмотреть, как мы сопоставим образец на этих данных

case n of
  Succ n' -> f n'
  Zero    -> g

должно быть очевидно, что каждая функция типа Nat -> a можно определить, дав соответствующий f а также g и что единственные способы сделать Nat (оголение дна) использует один из двух конструкторов.

---

РЕДАКТИРОВАТЬ: думать о f на мгновение. Если мы определяем функцию foo :: Nat -> a давая соответствующие f а также g такой, что f рекурсивно вызывает foo чем мы можем переопределить f как f' n' (foo n') такой, что f' не является рекурсивным Если тип a = (a',Nat) чем мы можем вместо этого написать f' (foo n), Итак, без потери общности

foo n = h $ case n
                 Succ n' -> f (foo n)
                 Zero    -> g

это формулировка, которая имеет смысл в остальной части моего поста:

---

Таким образом, мы можем думать о выражении case как о применении "словаря деструкторов"

data NatDict a = NatDict {
   onSucc :: a -> a,
   onZero :: a
}

Теперь наш случай из ранее может стать

h $ case n of
      Succ n' -> onSucc (NatDict f g) n'
      Zero    -> onZero (NatDict f g)

учитывая это, мы можем вывести

newtype NatBB = NatBB {cataNat :: forall a. NatDict a -> a}

тогда мы можем определить две функции

fromBB :: NatBB -> Nat
fromBB n = cataNat n (NatDict Succ Zero)

а также

toBB :: Nat -> NatBB
toBB Zero = Nat $ \dict -> onZero dict
toBB (Succ n) = Nat $ \dict -> onSucc dict (cataNat (toBB n) dict)

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

newtype NatAsFold = NatByFold (forall a. (a -> a) -> a -> a)

(что так же, как NatBB) изоморфен Nat

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

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

newtype RecListType a r = RecListType (r -> (a -> RecListType -> r) -> r)

но, видимо, оптимизатор GHC захлёбывается иногда:(.