Haskell Language
Типная алгебра

Естественные числа в алгебре типов

Мы можем провести связь между типами Хаскелла и натуральными числами. Это соединение можно присвоить каждому типу количеству жителей.

Конечные типы соединений

Для конечных типов достаточно видеть, что мы можем присвоить натуральный тип каждому числу, основанному на числе конструкторов. Например:

type Color = Red | Yellow | Green

будет 3 . И тип Bool будет 2 .

type Bool = True | False

Единственность с точностью до изоморфизма

Мы видели, что несколько типов будут соответствовать одному числу, но в этом случае они будут изоморфны. Это означает, что существует пара морфизмов f и g , состав которых будет тождественным, соединяющим два типа.

f :: a -> b
g :: b -> a

f . g == id == g . f

В этом случае мы будем говорить, что типы изоморфны . Мы будем рассматривать два типа, равные в нашей алгебре, если они изоморфны.

Например, два разных представления числа два тривиально изоморфны:

type Bit  = I    | O
type Bool = True | False

bitValue :: Bit -> Bool
bitValue I = True
bitValue O = False

booleanBit :: Bool -> Bit
booleanBit True  = I
booleanBit False = O

Потому что мы можем видеть bitValue . booleanBit == id == booleanBit . bitValue

Один и ноль

Представление числа 1 , очевидно, является типом только с одним конструктором. В Haskell этот тип является каноническим типом () , называемым Unit. Каждый другой тип с одним конструктором изоморфен () .

И наше представление 0 будет типом без конструкторов. Это тип Void в Haskell, как определено в Data.Void . Это будет эквивалентно неживому типу с конструкторами данных:

data Void

Добавление и умножение

Сложение и умножение имеют эквиваленты в алгебре этого типа. Они соответствуют маркированным союзам и типам продукции .

data Sum a b = A a | B b
data Prod a b = Prod a b

Мы можем видеть, как число жителей каждого типа соответствует операциям алгебры.

Эквивалентно, мы можем использовать Either и (,) как конструкторы типов для сложения и умножения. Они изоморфны нашим ранее определенным типам:

type Sum' a b = Either a b
type Prod' a b = (a,b)

Ожидаемым результатам сложения и умножения следуют алгебра типов до изоморфизма. Например, мы можем видеть изоморфизм между 1 + 2, 2 + 1 и 3; как 1 + 2 = 3 = 2 + 1.

data Color = Red | Green | Blue

f :: Sum () Bool -> Color
f (Left ())     = Red
f (Right True)  = Green
f (Right False) = Blue

g :: Color -> Sum () Bool
g Red   = Left ()
g Green = Right True
g Blue  = Right False

f' :: Sum Bool () -> Color
f' (Right ())   = Red
f' (Left True)  = Green
f' (Left False) = Blue

g' :: Color -> Sum Bool ()
g' Red   = Right ()
g' Green = Left True
g' Blue  = Left False

Правила сложения и умножения

Общие правила коммутативности, ассоциативности и дистрибутивности справедливы, поскольку существуют тривиальные изоморфизмы между следующими типами:

-- Commutativity
Sum a b           <=> Sum b a
Prod a b          <=> Prod b a
-- Associativity
Sum (Sum a b) c   <=> Sum a (Sum b c)
Prod (Prod a b) c <=> Prod a (Prod b c)
-- Distributivity
Prod a (Sum b c)  <=> Sum (Prod a b) (Prod a c)

Рекурсивные типы

Списки

Списки могут быть определены как:

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

Если мы переведем это в нашу алгебру типов, получим

Список (a) = 1 + a * Список (a)

Но теперь мы можем снова заменить List (a) в этом выражении несколько раз, чтобы получить:

Список (a) = 1 + a + a * a + a * a * a + a * a * a * a + ...

Это имеет смысл, если мы видим список как тип, который может содержать только одно значение, как в [] ; или любое значение типа a , как в [x] ; или два значения типа a , как в [x,y] ; и так далее. Теоретическое определение списка, которое мы должны получить оттуда, будет:

-- Not working Haskell code!
data List a = Nil
            | One a
            | Two a a
            | Three a a a 
            ...

деревья

Например, мы можем сделать то же самое с бинарными деревьями. Если мы определим их как:

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

Получаем выражение:

Дерево (a) = 1 + a * Дерево (a) * Дерево (a)

И если мы будем делать те же подстановки снова и снова, мы получим следующую последовательность:

Дерево (a) = 1 + a + 2 (a * a) + 5 (a * a * a) + 14 (a * a * a * a) + ...

Коэффициенты, которые мы получаем здесь, соответствуют последовательности каталонских чисел, а n-е каталонское число - это точно число возможных бинарных деревьев с n узлами.

производные

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

В качестве примера мы можем взять тройной тип (a,a,a) и получить его, получив

data OneHoleContextsOfTriple = (a,a,()) | (a,(),a) | ((),a,a)

Это согласуется с нашим обычным определением вывода:

d / da (a * a * a) = 3 * a * a

Подробнее об этой теме можно прочитать в этой статье .

функции

Функции можно рассматривать как экспоненты в нашей алгебре. Как мы видим, если взять тип a с n экземплярами и тип b с m экземплярами, тип a -> b будет иметь m для мощности n экземпляров.

В качестве примера, Bool -> Bool изоморфен (Bool,Bool) , как 2 * 2 = 2².

iso1 :: (Bool -> Bool) -> (Bool,Bool)
iso1 f = (f True,f False)

iso2 :: (Bool,Bool) -> (Bool -> Bool)
iso2 (x,y) = (\p -> if p then x else y)