Ответ 1
Во-первых, типы, о которых вы упоминаете, на самом деле не являются GADT, они простые ADT, так как тип возврата каждого конструктора всегда T a. Правильный GADT будет чем-то вроде
data T a where
K1 :: T Bool -- not T a
В любом случае, упомянутый вами метод - это хорошо известный метод кодирования алгебраических типов данных в (полиморфные) функции. Он подпадает под многие имена, такие как кодовое кодирование, кодирование Бёма-Берардуччи, кодирование конца, как катаморфизм и т.д. Иногда лемма Ионеды используется для обоснования такого подхода, но нет необходимости понимать теоретико-множественные механизмы для понимания метода.
В принципе, идея такова. Все ADT могут быть сгенерированы с помощью
- типы продуктов
(,) a b - типы сумм
Either a b - Типы стрелок
a -> b - тип устройства
() - void type
Void(редко используется в Haskell, но теоретически хорошо) - (если тип bing имеет параметры)
- возможно, базовые типы (
Integer,...) - тип level-recursion
Рекурсия уровня уровня используется, когда какой-либо конструктор значений принимает тип, который определяется как аргумент. Классический пример - натуральные пиано:
data Nat where
O :: Nat
S :: Nat -> Nat
-- ^^^ recursive!
Списки также распространены:
data List a where
Nil :: List a
Cons :: a -> List a -> List a
-- ^^^^^^ recursive!
Типы типа Maybe a, пары и т.д. не являются рекурсивными.
Обратите внимание, что каждый ADT, рекурсивный или нет, может быть сведен к одному конструктору с аргументом sigle, суммируя (Either) по всем конструкторам и умножая все аргументы. Например, Nat изоморфно
data Nat1 where
O1 :: () -> Nat
S1 :: Nat -> Nat
которая изоморфна
data Nat2 where K2 :: (Either () Nat) -> Nat
Списки становятся
data List1 a where K1 :: (Either () (a, List a)) -> List a
В приведенных выше шагах используется алгебра типов, в результате чего сумма и произведения типов подчиняются тем же правилам, что и алгебра средней школы, а a -> b ведет себя как экспоненциальная b^a.
Следовательно, мы можем написать любой ADT в виде
-- pseudo code
data T where
K :: F T -> T
type F k = .....
Например
type F_Nat k = Either () k -- for T = Nat
type F_List_a k = Either () (a, k) -- for T = List a
(Обратите внимание, что функция последнего типа F зависит от a, но это не важно прямо сейчас.)
Нерекурсивные типы не будут использовать k:
type F_Maybe_a k = Either () a -- for T = Maybe a
Обратите внимание, что конструктор k выше делает тип T изоморфным F T (пусть игнорирует введенное им поднятие/дополнительное дно). По существу, мы имеем, что
Nat ~= F Nat = Either () Nat
List a ~= F (List a) = Either () (a, List a)
Maybe a ~= F (Maybe a) = Either () a
Мы можем даже формализовать это далее, абстрагируясь от F
newtype Fix f = Fix { unFix :: f (Fix f) }
По определению Fix F теперь будет изоморфно F (Fix F). Мы могли бы позволить
type Nat = Fix F_Nat
(В Haskell нам нужна обложка newtype вокруг F_Nat, которую я опускаю для ясности.)
Наконец, общая кодировка или катаморфизм:
cata :: (F k -> k) -> Fix F -> k
Это предполагает, что F является функтором.
Для Nat получаем
cata :: (Either () k -> k) -> Nat -> k
-- isomorphic to
cata :: (() -> k, k -> k) -> Nat -> k
-- isomorphic to
cata :: (k, k -> k) -> Nat -> k
-- isomorphic to
cata :: k -> (k -> k) -> Nat -> k
Обратите внимание на шаги средней школы albegra, где k^(1+k) = k^1 * k^k, следовательно Either () k -> k ~= (() -> k, k -> k).
Заметим, что мы получаем два аргумента k и k->k, которые соответствуют O и S. Это не совпадение - мы суммировали все конструкторы. Это означает, что cata ожидает, что будет передано значение типа k, которое "играет роль O", а затем значение типа k -> k, которое играет роль S.
Более неформально cata сообщает нам, что если мы хотим отобразить естественное в k, нам нужно только указать, что такое "ноль" внутри k и как взять "преемника" в k, а затем каждый Nat может отображаться соответственно.
Для списков мы получаем:
cata :: (Either () (a, k) -> k) -> List a -> k
-- isomorphic to
cata :: (() -> k, (a, k) -> k) -> List a -> k
-- isomorphic to
cata :: (k, a -> k -> k) -> List a -> k
-- isomorphic to
cata :: k -> (a -> k -> k) -> List a -> k
который равен foldr.
Опять же, это cata говорит нам, что если мы укажем, как взять "пустой список" в k и "cons" a и k внутри k, мы можем сопоставить любые список в k.
Maybe a то же самое:
cata :: (Either () a -> k) -> Maybe a -> k
-- isomorphic to
cata :: (() -> k, a -> k) -> Maybe a -> k
-- isomorphic to
cata :: (k, a -> k) -> Maybe a -> k
-- isomorphic to
cata :: k -> (a -> k) -> Maybe a -> k
Если мы можем сопоставить Nothing в k и выполнить Just отображение a в k, мы можем отобразить любой Maybe a в k.
Если мы попытаемся применить тот же подход к Bool и (a,b), мы получим функции, которые были опубликованы в вопросах.
Более продвинутые теоретические темы для поиска:
- (начальные) F-алгебры в теории категорий
- элиминаторы/рекурсоры/принципы индукции в теории типов (они также могут применяться к GADT)