Haskell Language
Wpisz algebra

Liczby naturalne w algebrze typów

Możemy narysować związek między typami Haskella a liczbami naturalnymi. To połączenie można przypisać każdemu typowi liczby mieszkańców.

Skończone typy unii

W przypadku typów skończonych wystarczy przekonać się, że do każdej liczby możemy przypisać typ naturalny w oparciu o liczbę konstruktorów. Na przykład:

type Color = Red | Yellow | Green

byłoby 3 . A typ Bool to 2 .

type Bool = True | False

Wyjątkowość aż do izomorfizmu

Widzieliśmy, że wiele typów odpowiada jednej liczbie, ale w tym przypadku byłyby one izomorficzne. To znaczy, że istniałaby para morfizmów f i g , których składem byłaby tożsamość, łącząca oba typy.

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

f . g == id == g . f

W tym przypadku powiedzielibyśmy, że typy są izomorficzne . Rozważymy dwa typy równe w naszej algebrze, o ile są one izomorficzne.

Na przykład dwie różne reprezentacje liczby dwa są trywialnie izomorficzne:

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

Ponieważ widzimy bitValue . booleanBit == id == booleanBit . bitValue

Jeden i zero

Przedstawienie liczby 1 jest oczywiście typem z tylko jednym konstruktorem. W Haskell ten typ jest kanonicznie typem () , zwanym Jednostką. Każdy inny typ z tylko jednym konstruktorem jest izomorficzny dla () .

A nasza reprezentacja 0 będzie typem bez konstruktorów. Jest to typ Pustki w Haskell, zgodnie z definicją w Data.Void . Byłby to odpowiednik typu niezamieszkanego bez konstruktorów danych:

data Void

Dodawanie i mnożenie

Dodawanie i mnożenie mają odpowiedniki w algebrze tego typu. Odpowiadają oznaczonym związkom i typom produktów .

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

Widzimy, jak liczba mieszkańców każdego typu odpowiada działaniom algebry.

Równolegle możemy użyć Either i i (,) jako konstruktorów typów dla dodawania i mnożenia. Są izomorficzne w stosunku do naszych wcześniej zdefiniowanych typów:

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

Po oczekiwanych wynikach dodawania i mnożenia następuje algebra typu aż do izomorfizmu. Na przykład możemy zaobserwować izomorfizm między 1 + 2, 2 + 1 i 3; jako 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

Zasady dodawania i mnożenia

Obowiązują wspólne reguły przemienności, asocjatywności i dystrybucji, ponieważ istnieją trywialne izomorfizmy między następującymi typami:

-- 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)

Typy rekurencyjne

Listy

Listy można zdefiniować jako:

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

Jeśli przetłumaczymy to na naszą algebrę typu, otrzymamy

Lista (a) = 1 + a * Lista (a)

Ale możemy teraz zastąpić List (a) ponownie w tym wyrażeniu wiele razy, aby uzyskać:

Lista (a) = 1 + a + a * a + a * a * a + a * a * a * a + ...

Ma to sens, jeśli widzimy listę jako typ, który może zawierać tylko jedną wartość, jak w [] ; lub każda wartość typu a , jak w [x] ; lub dwie wartości typu a , jak w [x,y] ; i tak dalej. Teoretyczna definicja Listy, którą powinniśmy uzyskać, to:

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

Drzewa

Na przykład możemy zrobić to samo z drzewami binarnymi. Jeśli zdefiniujemy je jako:

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

Otrzymujemy wyrażenie:

Drzewo (a) = 1 + a * Drzewo (a) * Drzewo (a)

A jeśli będziemy powtarzać te same podstawienia, uzyskamy następującą sekwencję:

Drzewo (a) = 1 + a + 2 (a * a) + 5 (a * a * a) + 14 (a * a * a * a) + ...

Uzyskane tutaj współczynniki odpowiadają sekwencji liczb katalońskich, a n-ta liczba katalońska jest dokładnie liczbą możliwych drzew dwójkowych z n węzłami.

Pochodne

Pochodna typu jest rodzajem kontekstu jednootworowego. Jest to typ, który uzyskalibyśmy, gdyby zmienna typu znikała w każdym możliwym punkcie i sumowała wyniki.

Jako przykład możemy wziąć typ potrójny (a,a,a) i uzyskać go, uzyskując

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

Jest to spójne z naszą zwykłą definicją pochodnej, ponieważ:

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

Więcej na ten temat można przeczytać w tym artykule .

Funkcje

Funkcje mogą być postrzegane jako wykładnicze w naszej algebrze. Jak widać, jeśli weźmie się typ a z n przykładów i typu b z przypadkach m, typu z a -> b będzie miał m do potęgi n przypadkach.

Na przykład Bool -> Bool jest izomorficzny na (Bool,Bool) , ponieważ 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)