Typ-Level-Programmierung zur Darstellung mehrdimensionaler Arrays (Tensoren)

Question

Ich möchte einen Typ haben, der mehrdimensionale Arrays (Tensoren) typsicher darstellt. so konnte ich zum Beispiel schreiben: zero :: Tensor (5,3,2) Integer , die ein mehrdimensionales Array darstellen würde, die 5-Element hat, von denen jeder hat drei Elemente, von denen jedes zwei Elemente aufweisen, wobei alle Elemente sind Integer s

Wie würden Sie definieren diese Art verwenden Typ-Level-Programmierung?

bearbeiten:

Nach der wunderbaren Antwort von Alec, der diese mit GADT s umgesetzt,

Ich frage mich, ob Sie noch einen Schritt weiter, nehmen und mehrere Implementierungen eines class Tensor und der Unterstützung die Operationen auf Tensoren und Serialisierung von Tensoren

, so dass Sie zum Beispiel haben könnte:

• GPU oder CPU Implementierungen C
• reine Haskell Implementierungen
• Implementierung verwenden, die nur die grafische Darstellung der Berechnung druckt und berechnen nichts
• Implementierung, die Ergebnisse auf der Festplatte Berechnung
• etc
• parallel oder verteilten Caches ...

Alle Typen sicher und einfach zu bedienen.

Meine Absicht ist es, eine Bibliothek in Haskell viel wie tensor-flow aber typsicher und vieles mehr erweiterbar zu machen, mit automatic differentiation (ad library) und exact real arithmetic (exact-real library)

Ich denke, eine funktionale Sprache wie Haskell viel mehr ist passend für diese Dinge (für alle Dinge meiner Meinung nach) als das Python-Ökosystem, das irgendwie keimte.

• Haskell ist rein funktional, viel mehr sutible für Computational Programmierung als Python
• Haskell viel effizienter als Python und kann auf binäre
• Haskells Faulheit (wohl) kompiliert werden, entfällt die Notwendigkeit, die Berechnung zu optimieren graph, macht und Code viel einfacher auf diese Weise
• viel mächtiger Abstraktionen in Haskell

Obwohl ich das Potenzial sehen, ich bin einfach nicht gut versiert genug (oder schlau genug) für diese Typ-Level-Programmierung, also weiß ich nicht, wie man so etwas in Haskell implementiert und es kompilieren lässt.

Dort brauche ich deine Hilfe.

Answer 1

Hier ist eine Möglichkeit (here is a complete Gist).Wir bleiben bei der Verwendung von Peano-Nummern anstelle von GHC-Typ-Ebene Nat, nur weil Induktion besser auf ihnen funktioniert.

{-# LANGUAGE GADTs, PolyKinds, DataKinds, TypeOperators, FlexibleInstances, FlexibleContexts #-} 

import Data.Foldable 
import Text.PrettyPrint.HughesPJClass 

data Nat = Z | S Nat 

-- Some type synonyms that simplify uses of 'Nat' 
type N0 = Z 
type N1 = S N0 
type N2 = S N1 
type N3 = S N2 
type N4 = S N3 
type N5 = S N4 
type N6 = S N5 
type N7 = S N6 
type N8 = S N7 
type N9 = S N8 

-- Similar to lists, but indexed over their length 
data Vector (dim :: Nat) a where 
    Nil :: Vector Z a 
    (:-) :: a -> Vector n a -> Vector (S n) a 

infixr 5 :- 

data Tensor (dim :: [Nat]) a where 
    Scalar :: a -> Tensor '[] a 
    Tensor :: Vector d (Tensor ds a) -> Tensor (d : ds) a 

diese Arten anzuzeigen, wir das pretty Paket verwenden werden (die bereits mit GHC kommt).

instance (Foldable (Vector n), Pretty a) => Pretty (Vector n a) where 
    pPrint = braces . sep . punctuate (text ",") . map pPrint . toList 

instance Pretty a => Pretty (Tensor '[] a) where 
    pPrint (Scalar x) = pPrint x 

instance (Pretty (Tensor ds a), Pretty a, Foldable (Vector d)) => Pretty (Tensor (d : ds) a) where 
    pPrint (Tensor xs) = pPrint xs 

Dann sind hier Fälle von Foldable für unsere Datentypen (nicht verwunderlich hier - ich bin auch nur, weil Sie es brauchen für die Pretty Instanzen zu kompilieren):

instance Foldable (Vector Z) where 
    foldMap f Nil = mempty 

instance Foldable (Vector n) => Foldable (Vector (S n)) where 
    foldMap f (x :- xs) = f x `mappend` foldMap f xs 


instance Foldable (Tensor '[]) where 
    foldMap f (Scalar x) = f x 

instance (Foldable (Vector d), Foldable (Tensor ds)) => Foldable (Tensor (d : ds)) where 
    foldMap f (Tensor xs) = foldMap (foldMap f) xs 

Schließlich ist der Teil Das beantwortet Ihre Frage: Wir können Applicative (Vector n) und Applicative (Tensor ds) ähnlich wie Applicative ZipList definiert definieren (außer pure nicht zurück und leere Liste - es gibt eine Liste der richtigen Länge).

instance Applicative (Vector Z) where 
    pure _ = Nil 
    Nil <*> Nil = Nil 

instance Applicative (Vector n) => Applicative (Vector (S n)) where 
    pure x = x :- pure x 
    (x :- xs) <*> (y :- ys) = x y :- (xs <*> ys) 


instance Applicative (Tensor '[]) where 
    pure = Scalar 
    Scalar x <*> Scalar y = Scalar (x y) 

instance (Applicative (Vector d), Applicative (Tensor ds)) => Applicative (Tensor (d : ds)) where 
    pure x = Tensor (pure (pure x)) 
    Tensor xs <*> Tensor ys = Tensor ((<*>) <$> xs <*> ys) 

Dann in GHCi, ist es ziemlich trivial zu Ihrer zero Funktion zu machen:

ghci> :set -XDataKinds 
ghci> zero = pure 0 
ghci> pPrint (zero :: Tensor [N5,N3,N2] Integer) 
{{{0, 0}, {0, 0}, {0, 0}}, 
{{0, 0}, {0, 0}, {0, 0}}, 
{{0, 0}, {0, 0}, {0, 0}}, 
{{0, 0}, {0, 0}, {0, 0}}, 
{{0, 0}, {0, 0}, {0, 0}}}