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

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

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

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

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

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

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

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

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

Ответ 1

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

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

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. Подобные идеи применимы и к вашим другим типам Церкви.

Ответ 2

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

data Nat = Succ Nat | Zero

мы можем рассмотреть, как мы сопоставляем шаблон по этим данным

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

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

EDIT: подумайте о 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
}

теперь наш оператор case из ранее может стать

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

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

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

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

но, по-видимому, оптимизатор GHCs иногда задыхается: (.