Таблицы разметки по типу - программирование

Общая идиома в Haskell, разностные списки, представляет собой список xs как значение (xs ++). Тогда (.) становится "(++)", а id становится "[]" (на самом деле это работает для любого моноида или категории). Поскольку мы можем составлять функции в постоянное время, это дает нам хороший способ эффективно создавать списки путем добавления.

К сожалению, тип [a] -> [a] больше, чем тип функций формы (xs ++) - большинство функций в списках делают что-то отличное от предшествующего аргумента.

Один подход вокруг этого (как используется в dlist) заключается в создании специального типа dlist с интеллектуальным конструктором. Другой подход (используемый в ShowS) заключается в том, чтобы нигде не принуждать ограничение и надеяться на лучшее. Но есть ли хороший способ сохранить все желаемые свойства списков различий при использовании типа, который точно соответствует размеру?

Ответ 1

Да!

Мы можем просмотреть [a] как бесплатный экземпляр монады Free ((,) a) ().

Таким образом, мы можем применить схему, описанную Эдвардом Кемтом в Free Monads for Less.

Тип, который мы получим, это

newtype F a = F { runF :: forall r. (() -> r) -> ((a, r) -> r) -> r }

или просто

newtype F a = F { runF :: forall r. r -> (a -> r -> r) -> r }

Итак runF - это не что иное, как функция foldr для нашего списка!

Это называется кодировка Boehm-Berarducci и изоморфна исходному типу данных (список) - так что это как можно меньше возможно, получите.

Уилл Несс говорит:

Таким образом, этот тип все еще слишком "широкий", он позволяет больше, чем просто префикс, - не ограничивает аргумент g функции.

Если я правильно понял его аргумент, он указывает, что вы можете применить функцию foldr (или runF) к чему-то, отличному от [] и (:).

Но я никогда не утверждал, что вы можете использовать foldr -encoding только для конкатенации. Действительно, как следует из этого названия, вы можете использовать его для вычисления любой складки - и того, что продемонстрировал Уэст Несс.

Это может стать более понятным, если вы забыли на мгновение, что существует один тип списка, [a]. Могут быть много типов списков - например, Я могу определить один на

data List a = Nil | Cons a (List a)

Он отличается от, но изоморфен [a].

Примером foldr -encoding является просто еще одно кодирование списков, например List a или [a]. Он также изоморфен [a], о чем свидетельствуют функции \l -> F (\a f -> foldr a f l) и \x -> runF [] (:) и тот факт, что их композиции (в любом порядке) являются тождественными. Но вы не обязаны конвертировать в [a] - вы можете напрямую конвертировать в List, используя \x -> runF x Nil Cons.

Важным моментом является то, что F a не содержит элемент, который не является функциями foldr для некоторого списка, и не содержит элемент, который является функциями foldr для более чем одного списка (очевидно).

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

Это неверно для кодировки списка различий - например, функция reverse не является операцией добавления для любого списка.