Programmation au niveau du type pour représenter les tableaux multidimensionnels (Tenseurs)

Question

Je voudrais avoir un type pour représenter les tableaux multidimensionnels (Tenseurs) de manière sécurisée. donc je pourrais écrire par exemple: zero :: Tensor (5,3,2) Integer qui représenterait un tableau multidimensionnel qui a élément 5, dont chacun dispose de 3 éléments dont chacun ont 2 éléments, où tous les éléments sont Integer s

Comment définiriez-vous ce type en utilisant programmation au niveau du type?

Modifier:

Après la merveilleuse réponse par Alec, qui mettait en œuvre ce en utilisant GADT s,

Je me demande si vous pouviez prendre un peu plus loin et prendre en charge plusieurs implémentations d'un class Tensor et les opérations sur tenseurs et sérialisation des tenseurs

telle que vous pourriez avoir par exemple:

• GPU ou CPU implémentations utilisant C
• pures Haskell implémentations
• application qui imprime uniquement le graphe de calcul et ne calcule rien
• mise en œuvre qui met en cache les résultats sur le disque
• de calcul parallèle ou distribué
• etc ...

Tous les types Sûr et facile à utiliser.

Mon intention est de faire une bibliothèque Haskell un peu comme tensor-flow mais le type de sécurité et beaucoup plus extensible, en utilisant automatic differentiation (ad library) et exact real arithmetic (exact-real library)

Je pense un langage fonctionnel comme Haskell est beaucoup plus approprié pour ces choses (pour toutes les choses à mon avis) que l'écosystème python qui a germé en quelque sorte.

• Haskell est purement fonctionnelle, beaucoup plus sutible pour la programmation informatique que python
• Haskell est beaucoup plus efficace que python et peut être compilé en binaire
• paresse de Haskell (sans doute) supprime la nécessité d'optimiser le calcul graphique et rend le code plus simple de cette façon
• abstractions beaucoup plus puissants dans Haskell

bien que je vois le potentiel, je ne suis pas assez bien versé (ou assez intelligent) pour cette programmation de niveau type, donc je ne sais pas comment implémenter une telle chose dans Haskell et la compiler.

C'est là que j'ai besoin de votre aide.

Answer 1

Voici une façon (here is a complete Gist).Nous nous en tenons à utiliser des numéros de Peano au lieu du niveau de type GHC Nat juste parce que l'induction fonctionne mieux sur eux.

{-# 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 

Pour afficher ces types, nous allons utiliser le paquet pretty (qui est livré avec GHC déjà).

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 

Ensuite, voici les cas de Foldable pour nos types de données (rien d'étonnant ici - je compris ce que parce que vous en avez besoin pour les Pretty cas de compilation):

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 

Enfin, la partie cela répond à votre question: nous pouvons définir Applicative (Vector n) et Applicative (Tensor ds) comme Applicative ZipList est défini (sauf pure ne renvoie pas et liste vide - il renvoie une liste de la bonne longueur).

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) 

Puis, en GHCi, il est assez trivial pour rendre votre fonction zero:

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