多次元配列（テンソル）を表す型レベルプログラミング

Question

多次元配列（Tensors）をタイプセーフな方法で表現する型が必要です。私は、たとえば書くことができます：全ての要素がIntegerの

どのように使用して、このタイプを定義している2つの要素を持っているそれぞれの3つの要素があり、それぞれが5要素を、持っている多次元配列を表すことになりzero :: Tensor (5,3,2) Integer を、タイプレベルのプログラミング？

編集：

この使用GADT秒を実現しアレックことで素晴らしい答え、後、

あなたはさらに一歩これを取る、とclass Tensorのとの複数の実装をサポートすることができれば、私は疑問に思います

0123：あなたはたとえば持っている可能性があること

なテンソルとテンソルのシリアライズでの操作C

• 純粋Haskell実装
• のみ計算のグラフを印刷し、ディスク
• 平行又は分散計算
• などの結果をキャッシュするもの
• 実装を計算しない実装を使用
• GPU又はCPU実装...

すべてのタイプ安全で使いやすい。

私の意図は、私がHaskellのような関数型言語がはるかだと思うくらいtensor-flowが、タイプセーフとはるかに拡張性、automatic differentiation（ad library）を使用して、およびexact real arithmetic（exact-real library）

ようにHaskellでライブラリを作ることです何とか発芽したPythonの生態系よりも、これらのもの（私の意見ではすべてのもの）に適しています。

• HaskellはHaskellははるかに効率的パイソンよりバイナリ
• Haskellの怠惰は、（おそらく）計算を最適化する必要性を除去するにコンパイルすることができる
• 、パイソンより計算プログラミングのためのはるかsutible純粋に機能的ですグラフは、と私は可能性を参照してくださいが

が、私はちょうど十分に精通していないよハスケルにコードはるかに簡単そのよう

はるかに強力な抽象化を行い（またはスマート十分な）このタイプレベルのプログラミングのため、私はどのようにHaskellでそのようなものを実装し、コンパイルすることを知りません。

私はあなたの助けが必要です。

Answer 1

これは片道です（here is a complete Gist）。私たちはGHCのタイプレベルNatの代わりにPeanoの数字を使用することに固執しています。

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

これらのタイプを表示するには、我々は（すでにGHCに付属している）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 

最後に、一部： -

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インスタンスをコンパイルするためにあなたがそれを必要とするだけであるため、これを含めたよ何もここで意外な）のインスタンスでありますあなたは答えます：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}}}