Шаблон с такими функциями, как `bool`,` both` и т.д.

Недавно я узнал о GADTs и их обозначения:

например.

data Maybe a where
  Nothing :: Maybe a
  Just    :: a -> Maybe a

data Either a b where
  Left  :: a -> Either a b
  Right :: b -> Either a b

data Bool where
  False :: Bool
  True  :: Bool

Теперь я заметил сходство с функциями, такими как bool, и either, который в основном похож на определение GADT:

взятие каждой строки в качестве аргумента
заменив фактический тип следующей буквой алфавита
и, наконец, возвращает функцию Type -> (the letter of step 2)

например.

maybe  :: b -> (a -> b) -> Maybe a -> b
either :: (a -> c) -> (b -> c) -> Either a b -> c
bool   :: a -> a -> Bool -> a

Это также включает foldr, но я заметил, что, например, У Tuple нет такой функции, хотя вы можете легко определить ее:

tuple :: (a -> b -> c) -> (a,b) -> c
tuple f (x,y) = f x y

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

Ответ 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)