Haskell Language
Geben Sie Algebra ein

Natürliche Zahlen in der Typalgebra

Wir können eine Verbindung zwischen den Haskell-Typen und den natürlichen Zahlen herstellen. Über diese Verbindung kann jedem Typ die Einwohnerzahl zugeordnet werden.

Endliche Vereinigungstypen

Bei endlichen Typen genügt es zu sehen, dass wir jeder Zahl basierend auf der Anzahl der Konstruktoren einen natürlichen Typ zuweisen können. Zum Beispiel:

type Color = Red | Yellow | Green

wäre 3 . Und der Bool Typ wäre 2 .

type Bool = True | False

Einzigartigkeit bis zum Isomorphismus

Wir haben gesehen, dass mehrere Typen einer einzigen Zahl entsprechen würden, aber in diesem Fall wären sie isomorph. Dies bedeutet, dass es ein Paar von Morphismen f und g , deren Zusammensetzung die Identität sein würde, die die beiden Typen verbindet.

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

f . g == id == g . f

In diesem Fall würden wir sagen, dass die Typen isomorph sind . Wir werden zwei Typen in unserer Algebra als gleich betrachten, solange sie isomorph sind.

Zum Beispiel sind zwei verschiedene Darstellungen der Zahl zwei trivalis isomorph:

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

Weil wir bitValue . booleanBit == id == booleanBit . bitValue sehen bitValue . booleanBit == id == booleanBit . bitValue

Eins und Null

Die Darstellung der Zahl 1 ist offensichtlich ein Typ mit nur einem Konstruktor. In Haskell ist dieser Typ kanonisch der Typ () , der Einheit genannt wird. Jeder andere Typ mit nur einem Konstruktor ist isomorph zu () .

Und unsere Darstellung von 0 wird ein Typ ohne Konstruktoren sein. Dies ist der Void- Typ in Haskell, wie in Data.Void definiert. Dies würde einem unbewohnten Typ ohne Datenkonstruktoren entsprechen:

data Void

Addition und Vermehrung

Die Addition und Multiplikation haben Entsprechungen in dieser Typalgebra. Sie entsprechen den gekennzeichneten Vereinigungen und Produkttypen .

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

Wir können sehen, wie die Einwohnerzahl jedes Typs den Operationen der Algebra entspricht.

Gleichermaßen können Wir Either und (,) als Typkonstruktoren für die Addition und die Multiplikation verwenden. Sie sind isomorph zu unseren zuvor definierten Typen:

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

Auf die erwarteten Additions- und Multiplikationsergebnisse folgt die Typalgebra bis hin zum Isomorphismus. Zum Beispiel können wir einen Isomorphismus zwischen 1 + 2, 2 + 1 und 3 sehen; als 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

Additions- und Multiplikationsregeln

Die allgemeinen Regeln der Kommutativität, Assoziativität und Verteilbarkeit gelten, weil zwischen den folgenden Typen triviale Isomorphismen existieren:

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

Rekursive Typen

Listen

Listen können definiert werden als:

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

Wenn wir dies in unsere Typalgebra übersetzen, erhalten wir

Liste (a) = 1 + a * Liste (a)

Aber wir können jetzt List (a) in diesem Ausdruck mehrmals ersetzen, um Folgendes zu erhalten:

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

Dies ist sinnvoll, wenn wir eine Liste als einen Typ sehen, der nur einen Wert enthalten kann, wie in [] ; oder jeder Wert vom Typ a wie in [x] ; oder zwei Werte vom Typ a wie in [x,y] ; und so weiter. Die theoretische Definition von List, die wir von dort bekommen sollten, wäre:

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

Bäume

Mit binären Bäumen können wir beispielsweise dasselbe tun. Wenn wir sie definieren als:

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

Wir bekommen den Ausdruck:

Baum (a) = 1 + a * Baum (a) * Baum (a)

Und wenn wir immer wieder dieselben Substitutionen vornehmen, erhalten wir die folgende Reihenfolge:

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

Die hier erhaltenen Koeffizienten entsprechen der katalanischen Zahlenfolge, und die n-te katalanische Zahl ist genau die Anzahl der möglichen binären Bäume mit n Knoten.

Derivate

Die Ableitung eines Typs ist der Typ seines Typs von Ein-Loch-Kontexten. Dies ist der Typ, den wir erhalten würden, wenn wir eine Typvariable in jedem möglichen Punkt verschwinden lassen und die Ergebnisse summieren.

Als Beispiel können wir den dreifachen Typ (a,a,a) und ableiten, indem wir erhalten

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

Dies steht im Einklang mit unserer üblichen Ableitungsdefinition:

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

Mehr zu diesem Thema erfahren Sie in diesem Artikel .

Funktionen

Funktionen können in unserer Algebra als Exponential betrachtet werden. Wie wir sehen können, wenn wir einen Typ a mit n Instanzen und einen Typ b mit m Instanzen nehmen, hat der Typ a -> b m die Macht von n Instanzen.

Als Beispiel ist Bool -> Bool isomorph zu (Bool,Bool) mit 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)