Отношения между TypeRep и "Type" GADT

Question

В Scrap your Boilerplate reloaded авторы описывают новую презентацию Scrap Your Boilerplate, которая должна быть эквивалентна оригиналу.

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

data Type :: * -> * where
  Int :: Type Int
  List :: Type a -> Type [a]
  ...

В оригинальном SYB используется типобезопасное приведение, реализованное с использованием Typeable учебный класс.

Мои вопросы:

• Какова связь между этими двумя подходами?
• Почему представление GADT было выбрано для презентации SYB Reloaded?

Answer 1

[Я являюсь одним из авторов статьи "SYB Reloaded".]

TL; DR Мы действительно использовали это, потому что оно показалось нам более красивым. На основе класса Typeable подход более практичен. Spine вид может быть объединен с Typeable класс и не зависит от Type GADT.

В документе говорится об этом в своих выводах:

Наша реализация обрабатывает два центральных компонента универсального программирования не так, как в оригинальной статье SYB: мы используем перегруженные функции с явными аргументами типа вместо перегруженных функций, основанных на безопасном приведениях типа 1 или расширяемой схеме на основе классов [20]; и мы используем явное представление позвоночника, а не комбинаторный подход. Оба изменения не зависят друг от друга и были сделаны с ясностью: мы считаем, что структура подхода SYB более заметна в наших условиях, и что отношения с PolyP и Generic Haskell становятся более ясными. Мы обнаружили, что, хотя представление позвоночника ограничено в классе обобщенных функций, которые могут быть написаны, оно применимо к очень большому классу типов данных, включая GADT.

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

Итак, выбор использования GADT для представления типов мы сделали в основном для ясности. Как утверждает Дон в своем ответе, в этом представлении есть некоторые очевидные преимущества, а именно то, что оно содержит статическую информацию о том, для какого типа представлено представление типа, и что оно позволяет нам осуществлять приведение без какой-либо дополнительной магии, и в частности без использования из unsafeCoerce, Индексированные по типу функции также могут быть реализованы напрямую, используя сопоставление с образцом для типа и не прибегая к различным комбинаторам, таким как mkQ или же extQ,

Дело в том, что я (и я думаю, что соавторы) просто не очень любили Typeable учебный класс. (На самом деле, я до сих пор нет, хотя теперь, наконец, это становится немного более дисциплинированным, поскольку GHC добавляет авто-вывод для Typeable, делает его немного полиморфным и, в конечном счете, исключает возможность определять ваши собственные экземпляры.) Кроме того, Typeable не было так широко распространено и широко известно, как сейчас, возможно, поэтому казалось привлекательным "объяснить" это с помощью кодировки GADT. И, кроме того, это было время, когда мы также думали о добавлении открытых типов данных в Haskell, тем самым снимая ограничение на закрытие GADT.

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

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

Сам документ показывает (в Разделе 8) вариант, вдохновленный документом "Зачисти свою учебную табличку с классом", в котором используется Spine смотреть с ограничением класса вместо. Но мы также можем сделать более прямое развитие, которое я покажу в следующем. Для этого мы будем использовать Typeable от Data.Typeable, но определим наше собственное Data класс, который для простоты просто содержит toSpine метод:

class Typeable a => Data a where
  toSpine :: a -> Spine a

Spine тип данных теперь использует Data ограничение:

data Spine :: * -> * where
  Constr  :: a -> Spine a
  (:<>:)  :: (Data a) => Spine (a -> b) -> a -> Spine b

Функция fromSpine так же тривиально, как и с другим представлением:

fromSpine :: Spine a -> a
fromSpine (Constr x) = x
fromSpine (c :<>: x) = fromSpine c x

Экземпляры для Data тривиальны для плоских типов, таких как Int:

instance Data Int where
  toSpine = Constr

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

data Tree a = Empty | Node (Tree a) a (Tree a)

instance Data a => Data (Tree a) where
  toSpine Empty        = Constr Empty
  toSpine (Node l x r) = Constr Node :<>: l :<>: x :<>: r

Затем документ продолжается и определяет различные общие функции, такие как mapQ, Эти определения почти не меняются. Мы получаем только ограничения класса для Data a => где статья имеет аргументы функции Type a ->:

mapQ :: Query r -> Query [r]
mapQ q = mapQ' q . toSpine

mapQ' :: Query r -> (forall a. Spine a -> [r])
mapQ' q (Constr c) = []
mapQ' q (f :<>: x) = mapQ' q f ++ [q x]

Функции более высокого уровня, такие как everything также просто потеряйте их явные аргументы типа (а затем на самом деле выглядят точно так же, как в оригинальном SYB):

everything :: (r -> r -> r) -> Query r -> Query r
everything op q x = foldl op (q x) (mapQ (everything op q) x)

Как я уже говорил выше, если мы теперь хотим определить общую функцию суммы, суммирующую все Int случаи, мы не можем больше соответствовать шаблону, но должны вернуться к mkQ, но mkQ определяется чисто с точки зрения Typeable и полностью независим от Spine:

mkQ :: (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
(r `mkQ` br) a = maybe r br (cast a)

И затем (снова точно так же, как в оригинальном SYB):

sum :: Query Int
sum = everything (+) sumQ

sumQ :: Query Int
sumQ = mkQ 0 id

Для некоторых вещей позже в статье (например, добавление информации конструктора) требуется немного больше работы, но все это можно сделать. Итак, используя Spine на самом деле не зависит от использования Type совсем.

Answer 2

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

Важным изменением является то, что в этом TypeRep нетипизированный. То есть нет связи между типом среды выполнения, TypeRepи статический тип, который он кодирует. С подходом GADT мы можем закодировать отображение между типом a И его Typeданное ГАДТ Type a,

Таким образом, мы выдвигаем доказательства того, что тип rep статически связан с его типом origin, и можем написать статически типизированное динамическое приложение (например), используя Type a в качестве доказательства того, что у нас есть время выполнения a,

В более раннем случае TypeRep у нас нет таких доказательств, и все сводится к равенству строк во время выполнения, а также к принуждению и надежде на лучшее через fromDynamic,

Сравните подписи:

toDyn :: Typeable a => a -> TypeRep -> Dynamic

против стиля GADT:

toDyn :: Type a => a -> Type a -> Dynamic

Я не могу подделать доказательства типа, и я могу использовать их позже при восстановлении, например, для поиска экземпляров класса типов для a когда все, что у меня есть, это Type a,