Ist es in haskell möglich, Dimensionen in einen Typ zu „backen“?

Angenommen, ich möchte eine Bibliothek schreiben, die sich mit Vektoren und Matrizen befasst. Ist es möglich, die Dimensionen in die Typen zu backen, sodass Operationen inkompatibler Dimensionen beim Kompilieren einen Fehler erzeugen?

Zum Beispiel möchte ich, dass die Signatur des Punktprodukts so ähnlich ist

dotprod :: Num a, VecDim d => Vector a d -> Vector a d -> a

Dabei denthält der Typ einen einzelnen ganzzahligen Wert (der die Dimension dieser Vektoren darstellt).

Ich nehme an, dass dies getan werden kann, indem (von Hand) ein separater Typ für jede Ganzzahl definiert und in einer Typklasse mit dem Namen gruppiert wird VecDim. Gibt es einen Mechanismus, um solche Typen zu "erzeugen"?

Oder vielleicht eine bessere / einfachere Möglichkeit, dasselbe zu erreichen?

Um die Antwort von @ KarlBielefeldt zu erweitern, finden Sie hier ein vollständiges Beispiel für die Implementierung von Vektoren - Listen mit einer statisch bekannten Anzahl von Elementen - in Haskell. Halte an deinem Hut fest ...

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

import Prelude hiding (foldr, zipWith)
import qualified Prelude
import Data.Type.Equality
import Data.Foldable
import Data.Traversable

Wie Sie der langen Liste der LANGUAGEDirektiven entnehmen können, funktioniert dies nur mit einer neueren Version von GHC.

Wir brauchen eine Möglichkeit, Längen innerhalb des Typensystems darzustellen. Per Definition ist eine natürliche Zahl entweder Null ( Z) oder der Nachfolger einer anderen natürlichen Zahl ( S n). So würde zum Beispiel die Nummer 3 geschrieben werden S (S (S Z)).

data Nat = Z | S Nat

Mit der DataKinds Erweiterung , diese dataErklärung stellt eine Art genannt Natund zwei Typ Bauer genannt Sund Z- in anderen Worten , wir haben Typ-Ebene natürliche Zahlen. Beachten Sie, dass die Typen Sund Zkeine Mitgliedswerte haben - nur Arten von Typen *werden von Werten bewohnt.

Nun führen wir eine GADT ein, die Vektoren mit bekannter Länge darstellt. Beachten Sie die Art-Signatur: VecErfordert eine ArtNat (dh eine Zoder eine SArt), um ihre Länge darzustellen.

data Vec :: Nat -> * -> * where
    VNil :: Vec Z a
    VCons :: a -> Vec n a -> Vec (S n) a
deriving instance (Show a) => Show (Vec n a)
deriving instance Functor (Vec n)
deriving instance Foldable (Vec n)
deriving instance Traversable (Vec n)

Die Definition von Vektoren ähnelt der von verknüpften Listen mit einigen zusätzlichen Informationen zur Länge auf Typebene. Ein Vektor ist entweder VNil, in welchem ​​Fall er eine Länge von Z(ero) hat, oder es ist eine VConsZelle, die ein Element zu einem anderen Vektor hinzufügt. In diesem Fall ist seine Länge eins länger als der andere Vektor ( S n). Beachten Sie, dass es kein Konstruktorargument vom Typ gibt n. Es wird nur zur Kompilierungszeit verwendet, um Längen zu verfolgen. Es wird gelöscht, bevor der Compiler Maschinencode generiert.

Wir haben einen Vektortyp definiert, der statisches Wissen über seine Länge enthält. Fragen wir die Art einiger VecSekunden ab, um ein Gefühl dafür zu bekommen, wie sie funktionieren:

ghci> :t (VCons 'a' (VCons 'b' VNil))
(VCons 'a' (VCons 'b' VNil)) :: Vec ('S ('S 'Z)) Char  -- (S (S Z)) means 2
ghci> :t (VCons 13 (VCons 11 (VCons 3 VNil)))
(VCons 13 (VCons 11 (VCons 3 VNil))) :: Num a => Vec ('S ('S ('S 'Z))) a  -- (S (S (S Z))) means 3

Das Skalarprodukt verhält sich wie bei einer Liste:

-- note that the two Vec arguments are declared to have the same length
vap :: Vec n (a -> b) -> Vec n a -> Vec n b
vap VNil VNil = VNil
vap (VCons f fs) (VCons x xs) = VCons (f x) (vap fs xs)

zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith f xs ys = fmap f xs `vap` ys

dot :: Num a => Vec n a -> Vec n a -> a
dot xs ys = foldr (+) 0 $ zipWith (*) xs ys

vap, der 'flink' einen Vektor von Funktionen auf einen Vektor von Argumenten anwendet, ist Vecanwendbar <*>; Ich habe es nicht in eine ApplicativeInstanz gestellt, weil es chaotisch wird . Beachten Sie auch, dass ich die foldrvom Compiler generierte Instanz von verwende Foldable.

Probieren wir es aus:

ghci> let v1 = VCons 2 (VCons 1 VNil)
ghci> let v2 = VCons 4 (VCons 5 VNil)
ghci> v1 `dot` v2
13
ghci> let v3 = VCons 8 (VCons 6 (VCons 1 VNil))
ghci> v1 `dot` v3
<interactive>:20:10:
    Couldn't match type ‘'S 'Z’ with ‘'Z’
    Expected type: Vec ('S ('S 'Z)) a
      Actual type: Vec ('S ('S ('S 'Z))) a
    In the second argument of ‘dot’, namely ‘v3’
    In the expression: v1 `dot` v3

Groß! Beim Versuch, dotVektoren zu erstellen, deren Länge nicht übereinstimmt , wird ein Kompilierungsfehler angezeigt.

Hier ist ein Versuch einer Funktion, Vektoren miteinander zu verketten:

-- This won't compile because the type checker can't deduce the length of the returned vector
-- VNil +++ ys = ys
-- (VCons x xs) +++ ys = VCons x (concat xs ys)

Die Länge des Ausgangsvektors wäre die Summe der Längen der beiden Eingangsvektoren. Wir müssen dem Typprüfer beibringen, wie man Nats addiert . Hierfür verwenden wir eine Funktion auf Typebene :

type family (n :: Nat) :+: (m :: Nat) :: Nat where
    Z :+: m = m
    (S n) :+: m = S (n :+: m)

Diese type familyDeklaration führt eine Funktion für Typen ein, die aufgerufen werden. Mit :+:anderen Worten, es ist ein Rezept für die Typprüfung, um die Summe zweier natürlicher Zahlen zu berechnen. Es wird rekursiv definiert - immer wenn der linke Operand größer als Zero ist, fügen wir dem Ausgang einen hinzu und reduzieren ihn im rekursiven Aufruf um eins. (Es ist eine gute Übung, eine Typfunktion zu schreiben, die zwei NatSekunden multipliziert .) Nun können wir +++kompilieren:

infixr 5 +++
(+++) :: Vec n a -> Vec m a -> Vec (n :+: m) a
VNil +++ ys = ys
(VCons x xs) +++ ys = VCons x (concat xs ys)

So verwenden Sie es:

ghci> VCons 1 (VCons 2 VNil) +++ VCons 3 (VCons 4 VNil)
VCons 1 (VCons 2 (VCons 3 (VCons 4 VNil)))

So weit so einfach. Was ist, wenn wir das Gegenteil von Verkettung machen und einen Vektor in zwei Teile teilen wollen? Die Längen der Ausgabevektoren hängen vom Laufzeitwert der Argumente ab. Wir möchten so etwas schreiben:

-- this won't work because there aren't any values of type `S` and `Z`
-- split :: (n :: Nat) -> Vec (n :+: m) a -> (Vec n a, Vec m a)

aber leider lässt Haskell uns das nicht zu. Wenn der Wert des nArguments im Rückgabetyp angezeigt werden soll (dies wird im Allgemeinen als abhängige Funktion oder Pi-Typ bezeichnet ), sind abhängige Typen mit "vollem Spektrum" erforderlich, wohingegen DataKindsuns nur hochgestufte Typkonstruktoren zur Verfügung stehen. Anders ausgedrückt, die Typkonstruktoren Sund werden Znicht auf der Wertebene angezeigt. Wir müssen uns mit Singleton-Werten begnügen, um eine bestimmte Darstellung zur Laufzeit zu erhalten Nat. *

data Natty (n :: Nat) where
    Zy :: Natty Z  -- pronounced 'zed-y'
    Sy :: Natty n -> Natty (S n)  -- pronounced 'ess-y'
deriving instance Show (Natty n)

Für einen bestimmten Typ n(mit Art Nat) gibt es genau einen Typbegriff Natty n. Wir können den Singleton-Wert als Laufzeitzeugen für Folgendes verwenden n: Wenn Sie etwas über a lernen, lernen Sie Nattyetwas über dessen Wert nund umgekehrt.

split :: Natty n ->
         Vec (n :+: m) a ->  -- the input Vec has to be at least as long as the input Natty
         (Vec n a, Vec m a)
split Zy xs = (Nil, xs)
split (Sy n) (Cons x xs) = let (ys, zs) = split n xs
                           in (Cons x ys, zs)

Lass es uns mal ausprobieren:

ghci> split (Sy (Sy Zy)) (VCons 1 (VCons 2 (VCons 3 VNil)))
(VCons 1 (VCons 2 VNil), VCons 3 VNil)
ghci> split (Sy (Sy Zy)) (VCons 3 VNil)
<interactive>:116:21:
    Couldn't match type ‘'S ('Z :+: m)’ with ‘'Z’
    Expected type: Vec ('S ('S 'Z) :+: m) a
      Actual type: Vec ('S 'Z) a
    Relevant bindings include
      it :: (Vec ('S ('S 'Z)) a, Vec m a) (bound at <interactive>:116:1)
    In the second argument of ‘split’, namely ‘(VCons 3 VNil)’
    In the expression: split (Sy (Sy Zy)) (VCons 3 VNil)

Im ersten Beispiel haben wir einen Vektor mit drei Elementen an Position 2 erfolgreich aufgeteilt. Dann ist ein Tippfehler aufgetreten, als wir versucht haben, einen Vektor an einer Position nach dem Ende zu teilen. Singletons sind die Standardtechnik, um einen Typ von einem Wert in Haskell abhängig zu machen.

_{* Die singletonsBibliothek enthält einige Template Haskell-Helfer, um Singleton-Werte wie Nattyfür Sie zu generieren .}

Letztes Beispiel. Was ist, wenn Sie die Dimensionalität Ihres Vektors nicht statisch kennen? Was ist zum Beispiel, wenn wir versuchen, einen Vektor aus Laufzeitdaten in Form einer Liste zu erstellen? Der Typ des Vektors hängt von der Länge der Eingabeliste ab. Anders ausgedrückt, wir können keinen foldr VCons VNilVektor erstellen, da sich der Typ des Ausgabevektors mit jeder Iteration der Falte ändert. Wir müssen die Länge des Vektors vor dem Compiler geheim halten.

data AVec a = forall n. AVec (Natty n) (Vec n a)
deriving instance (Show a) => Show (AVec a)

fromList :: [a] -> AVec a
fromList = Prelude.foldr cons nil
    where cons x (AVec n xs) = AVec (Sy n) (VCons x xs)
          nil = AVec Zy VNil

AVecist ein existentieller Typ : Die Typvariable nerscheint nicht im Rückgabetyp des AVecDatenkonstruktors. Wir können es verwenden eine zu simulieren abhängig Paar : fromListSie können nicht sagen , der Länge des Vektors statisch, aber es kann Ihnen etwas zurückgeben können Muster-Match auf lernen die Länge des Vektors - die Natty nim ersten Element des Tupels . Wie Conor McBride es in einer verwandten Antwort formuliert : "Sie betrachten eine Sache und lernen dabei etwas über eine andere".

Dies ist eine übliche Technik für existenziell quantifizierte Typen. Da Sie mit Daten, für die Sie den Typ nicht kennen, eigentlich nichts data Something = forall a. Sth aanfangen können - versuchen Sie, eine Funktion zu schreiben -, werden Existenzdaten häufig mit GADT-Beweisen gebündelt, die es Ihnen ermöglichen, den ursprünglichen Typ durch Durchführung von Pattern-Matching-Tests wiederherzustellen. Andere gebräuchliche Muster für Existentials sind das Packen von Funktionen zum Verarbeiten Ihres Typs ( data AWayToGetTo b = forall a. HeresHow a (a -> b)), was eine gute Möglichkeit ist, erstklassige Module zu erstellen, oder das Einrichten eines Typklassenwörterbuchs ( data AnOrd = forall a. Ord a => AnOrd a), mit dessen Hilfe der Polymorphismus von Subtypen emuliert werden kann.

ghci> fromList [1,2,3]
AVec (Sy (Sy (Sy Zy))) (VCons 1 (VCons 2 (VCons 3 Nil)))

Abhängige Paare sind nützlich, wenn die statischen Eigenschaften von Daten von dynamischen Informationen abhängen, die zur Kompilierungszeit nicht verfügbar sind. Hier ist filterfür Vektoren:

filter :: (a -> Bool) -> Vec n a -> AVec a
filter f = foldr (\x (AVec n xs) -> if f x
                                    then AVec (Sy n) (VCons x xs)
                                    else AVec n xs) (AVec Zy VNil) 

Zu dotzweit AVecmüssen wir GHC beweisen, dass ihre Längen gleich sind. Data.Type.Equalitydefiniert eine GADT, die nur erstellt werden kann, wenn ihre Typargumente identisch sind:

data (a :: k) :~: (b :: k) where
    Refl :: a :~: a  -- short for 'reflexivity'

Wenn Sie die Musterübereinstimmung Reflaktivieren, weiß GHC das a ~ b. Es gibt auch einige Funktionen, die Ihnen bei der Arbeit mit diesem Typ helfen: Wir werden gcastWithzwischen äquivalenten Typen konvertieren und TestEqualityfeststellen, ob zwei Nattys gleich sind.

Um die Gleichheit zweier zu testen Nattys, sind wir nach Bedarf zu nutzen die Tatsache geht , dass , wenn zwei Zahlen gleich sind, dann ihre Nachfolger auch gleich sind ( :~:ist deckungsgleich über S):

congSuc :: (n :~: m) -> (S n :~: S m)
congSuc Refl = Refl

Der Mustervergleich Reflauf der linken Seite zeigt dies GHC an n ~ m. Mit diesem Wissen ist es trivial S n ~ S m, also lässt uns GHC Reflsofort ein neues zurückgeben .

Jetzt können wir TestEqualitydurch einfache Rekursion eine Instanz von schreiben . Wenn beide Zahlen Null sind, sind sie gleich. Wenn beide Zahlen Vorgänger haben, sind sie gleich, wenn die Vorgänger gleich sind. (Wenn sie nicht gleich sind, kehren Sie einfach zurück Nothing.)

instance TestEquality Natty where
    -- testEquality :: Natty n -> Natty m -> Maybe (n :~: m)
    testEquality Zy Zy = Just Refl
    testEquality (Sy n) (Sy m) = fmap congSuc (testEquality n m)  -- check whether the predecessors are equal, then make use of congruence
    testEquality Zy _ = Nothing
    testEquality _ Zy = Nothing

Jetzt können wir die Teile zu doteinem Paar AVecunbekannter Länge zusammenfügen.

dot' :: Num a => AVec a -> AVec a -> Maybe a
dot' (AVec n u) (AVec m v) = fmap (\proof -> gcastWith proof (dot u v)) (testEquality n m)

Zuerst wird eine Musterübereinstimmung im AVecKonstruktor durchgeführt, um eine Laufzeitdarstellung der Längen der Vektoren zu erhalten. Stellen Sie testEqualitynun fest, ob diese Längen gleich sind. Wenn ja, werden wir haben Just Refl; gcastWithwird diesen Gleichheitsnachweis verwenden, um sicherzustellen, dass er dot u vgut typisiert ist, indem er seine implizite n ~ mAnnahme erfüllt .

ghci> let v1 = fromList [1,2,3]
ghci> let v2 = fromList [4,5,6]
ghci> let v3 = fromList [7,8]
ghci> dot' v1 v2
Just 32
ghci> dot' v1 v3
Nothing  -- they weren't the same length

Beachten Sie, dass wir die Listenversion von effektiv neu implementiert haben, da ein Vektor ohne statische Kenntnis seiner Länge im Grunde genommen eine Liste ist dot :: Num a => [a] -> [a] -> Maybe a. Der Unterschied besteht darin, dass diese Version in Bezug auf die Vektoren implementiert ist dot. Hier ist der Punkt: vor dem Typ - Checker Sie können anrufen dot, Sie getestet haben müssen , ob die Eingangslisten haben die gleiche Länge verwenden testEquality. Ich ifneige dazu, -Anweisungen falsch herum zu bekommen , aber nicht in einer von der Schreibmaschine abhängigen Umgebung!

Sie können es nicht vermeiden, existenzielle Wrapper an den Rändern Ihres Systems zu verwenden, wenn Sie mit Laufzeitdaten arbeiten, aber Sie können abhängige Typen überall in Ihrem System verwenden und die existenziellen Wrapper an den Rändern belassen, wenn Sie eine Eingabevalidierung durchführen.

Da dies Nothingnicht sehr informativ ist, können Sie die Art der dot'Rückgabe eines Beweises, dass die Längen nicht gleich sind (in Form eines Beweises, dass ihre Differenz nicht 0 ist), im Fehlerfall weiter verfeinern . Dies ist ziemlich ähnlich der Standard-Haskell-Technik, mit Either String ader möglicherweise eine Fehlermeldung zurückgegeben wird, obwohl ein Beweisbegriff weitaus rechenintensiver ist als eine Zeichenfolge!

Damit endet diese Pfeifentour mit einigen der Techniken, die bei der Programmierung mit Haskell-Typen üblich sind. Das Programmieren mit solchen Typen in Haskell ist wirklich cool, aber gleichzeitig sehr umständlich. Das Aufteilen all Ihrer abhängigen Daten in viele Darstellungen, die dasselbe bedeuten - NatTyp, NatArt, Natty nSingleton - ist sehr umständlich, obwohl Code-Generatoren vorhanden sind, die bei der Erstellung des Boilerplates helfen. Derzeit gibt es auch Einschränkungen, was auf die Typstufe heraufgestuft werden kann. Es ist zwar verlockend! Der Verstand wundert sich über die Möglichkeiten - in der Literatur gibt es in Haskell Beispiele für stark typisierte printfDatenbankschnittstellen, UI-Layout-Engines ...

Wenn Sie mehr darüber lesen möchten, gibt es eine wachsende Zahl von Literatur zu Haskell, die abhängig von der Schreibweise geschrieben wurde, sowohl veröffentlicht als auch auf Websites wie Stack Overflow. Ein guter Ausgangspunkt ist das Hasochismus- Papier - das Papier geht genau dieses Beispiel durch (unter anderem) und erörtert die schmerzhaften Teile ausführlich. Das Singleton- Paper demonstriert die Technik von Singleton-Werten (wie z. B. Natty). Weitere Informationen zum abhängigen Tippen im Allgemeinen finden Sie im Agda- Lernprogramm. auch, Idris ist eine Sprache , in der Entwicklung , die (grob) entwickelt , um „Haskell mit abhängigen Arten“ ist.

Das nennt man abhängiges Tippen . Sobald Sie den Namen kennen, können Sie mehr Informationen darüber finden, als Sie sich jemals wünschen könnten. Es gibt auch eine interessante haskell-artige Sprache namens Idris , die sie von Haus aus verwendet. Sein Autor hat ein paar wirklich gute Präsentationen zu dem Thema gemacht, das Sie auf Youtube finden können.