類型級別的編程來表示多維數組（張量）

Question

我想有一個類型來以類型安全的方式表示多維數組（張量）。所以我可以例如寫：zero :: Tensor (5,3,2) Integer ，將代表具有5元件的多維陣列，其中的每一個具有3個元件的每一個有2個元素，其中的所有元素都是Integer小號

你如何定義這種類型的使用類型級編程？

編輯：

由蘇有朋，這實現了這個使用GADT S上精彩的回答後，

我不知道你能否藉此更進一步，並支持class Tensor和的多個實現

0123：

這樣你可以有例如在張量和張量的系列化運作個

• GPU或CPU實現使用C
• 純Haskell實現
• 實現，只打印計算的曲線圖，並且不計算任何
• 執行用於緩存
• 平行或分佈式計算磁盤上的結果
• 等...

所有類型安全和易於使用。

我的目的是讓在Haskell庫很像tensor-flow但類型安全的，更加可擴展，使用automatic differentiation（ad library）和exact real arithmetic（exact-real library）

我認爲像Haskell函數式語言是更適合這些事情（對於我所見的所有事情）比以某種方式發芽的蟒蛇生態系統。

• Haskell是純粹的功能，更sutible比蟒蛇計算編程
• Haskell是比Python更有效，並且可以編譯成二進制
• Haskell的懶惰（可以說）移除，以優化的計算需要圖中，使代碼更簡單這樣
• 更強大的抽象哈斯克爾

雖然我看到潛在的，我只是不精通不夠（或足夠聰明）來進行這種類型編程，所以我不知道如何在Haskell中實現這樣的事情並讓它編譯。

這就是我需要你的幫助的地方。

Answer 1

這裏是一種方式（here is a complete Gist）。我們堅持使用Peano數字代替GHC的類型級別Nat，因爲感應對他們更好。

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

要顯示這些類型的，我們將使用pretty包（其中已經自帶了GHC）。

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 

當年這裏是Foldable我們的數據類型（沒什麼好驚訝這裏 - 我包括這只是因爲你需要它的Pretty實例編譯）實例：

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 

最後，部分回答您的問題：我們可以定義Applicative (Vector n)和Applicative (Tensor ds)類似於如何定義Applicative ZipList（除了pure不返回並且空列表 - 它返回正確長度的列表）。

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) 

然後，在ghci中，它是非常容易的，讓您的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}}}