配列と型クラスリフティング（および依存型？）

Question

レッツはタイプbがMonoidの固定インデックスのインスタンスであると言う私は、対応するデータを定義する型クラスIxに属するiで(v1,v2) :: (i,i)の範囲。配列型もMonoidになります。これはどうすればできますか？ここで、memptyは、アレイがmappendである必要がありますので、エントリmempty::bおよびmappendの配列である必要があります。

（例えばi=(Int,Int)タイプData.Array i bは、2次元の（すべてで表す場合）、異なるサイズ（インデックスの異なる範囲とmatricies）。のみ固定サイズのため、そのようなMonoid -declarationは理にかなっている。実際に、私が興味を持ってMonoidsの代わりにベクトル空間のケースがありますが、Monoidはすでに難しさを示しています。私は依存型について漠然とした考え方しか持っていませんが、これはプロトタイプのようです。 1つのパラメータが有用であろう）

Answer 1

一般的な方法は、このようなより多くの型付き一つにない - 非常に型指定された表現をラップすることです：。

寸法の大きさと mのリストは、このリストの長さである（同様に促進及びファントム） -

data Nat = Z | S Nat 
newtype Vec (n :: Nat) a = Vec [a] 
newtype Sized m (ns :: [Nat]) a = Sized { getArray :: Array (Vec m Int) a } 

ここnsが促進（​​参照）ファントム（Motivation behind Phantom Types?参照）の値です。したがって、Sizedラッパーの下にある配列は、次元を表すnsの多次元行列とみなされます。 SingIものはsingletonsライブラリからのものであることを

instance (SingI m, SingI ns, Monoid a) => Monoid (Sized m ns a) where 
    mempty      = listSized $ repeat mempty 
    Sized as `mappend` Sized bs = listSized $ zipWith mappend (elems as) (elems bs) 

：Monoidインスタンスは、このようになります。シングルトンは値を型レベルに持ち上げることができるので、従属型をちょっとエミュレートすることができ、SingIはfromSing関数を介して値レベルで持ち上げられた値を取り戻すことができます。 listSizedは本質的にはlistArrayですが、静的に既知の次元を持つ配列の場合には、したがって、それらのすべてが範囲内にあることが必要です。

toInt :: Nat -> Int 
toInt = go 0 where 
    go !a Z = a 
    go a (S n) = go (1 + a) n 

vecBounds :: forall m (ns :: [Nat]). (SingI m) => Sing ns -> (Vec m Int, Vec m Int) 
vecBounds singNs = (Vec $ replicate m 0, Vec ns') where 
    m = toInt $ fromSing (sing :: Sing m) 
    ns' = map (pred . toInt) $ fromSing singNs 

listSized :: forall m (ns :: [Nat]) a. (SingI m, SingI ns) => [a] -> Sized m ns a 
listSized = Sized . listArray (vecBounds (sing :: Sing ns)) 

vecBoundsは寸法の大きさの与えられた昇格リストの境界を計算します。ここではその定義です。これは、第1の成分が、常に、[0,0..0]という形式の低関心の指標であるタプルを返します（次元数が0の場合は、m）。 2番目の要素が最大のインデックスです。 [2, 1, 3]（[S (S Z), S Z, S (S (S Z))]と表示されます）のようなサイズのリストがある場合、最大インデックスは[1, 0, 2]です。

instance Ix a => Ix (Vec n a) where 
    range (Vec ns, Vec ms)   = map Vec . sequence $ zipWith (curry range) ns ms 
    index (Vec ns, Vec ms) (Vec ps) = foldr (\(i, r) a -> i + r * a) 0 $ 
    zipWith3 (\n m p -> (index (n, m) p, rangeSize (n, m))) ns ms ps 
    inRange (Vec ns, Vec ms) (Vec ps) = and $ zipWith3 (curry inRange) ns ms ps 

そして、我々はいくつかのテストを書くことができます：

それだけthe product instancesの直接の一般化であるVec n aためIxインスタンスを提供するために、残って

type M = S (S (S Z)) 
type Ns = [S (S Z), S Z, S (S (S Z))] 

arr1 :: Sized M Ns (Sum Int) 
arr1 = listSized $ map Sum [5,3,6,7,1,4] 

arr2 :: Sized M Ns (Sum Int) 
arr2 = listSized $ map Sum [8,2,9,7,3,6] 

main = mapM_ (print . getArray) $ [arr1, arr2, arr1 `mappend` arr2 `mappend` mempty] 

これは

array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 5}),(Vec [0,0,1],Sum {getSum = 6}),(Vec [0,0,2],Sum {getSum = 1}),(Vec [1,0,0],Sum {getSum = 3}),(Vec [1,0,1],Sum {getSum = 7}),(Vec [1,0,2],Sum {getSum = 4})] 
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 8}),(Vec [0,0,1],Sum {getSum = 9}),(Vec [0,0,2],Sum {getSum = 3}),(Vec [1,0,0],Sum {getSum = 2}),(Vec [1,0,1],Sum {getSum = 7}),(Vec [1,0,2],Sum {getSum = 6})] 
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 13}),(Vec [0,0,1],Sum {getSum = 15}),(Vec [0,0,2],Sum {getSum = 4}),(Vec [1,0,0],Sum {getSum = 5}),(Vec [1,0,1],Sum {getSum = 14}),(Vec [1,0,2],Sum {getSum = 10})] 

を印刷します

必要に応じて要素を点単位で合計した。

type Ns = [S (S Z), S Z, S (S (S Z))] 
type Ns' = [S (S (S Z)), S Z, S (S Z)] 

arr1 :: Sized M Ns (Sum Int) 
arr1 = listSized $ map Sum [5,3,6,7,1,4] 

arr2 :: Sized M Ns' (Sum Int) 
arr2 = listSized $ map Sum [8,2,9,7,3,6] 

main = print . getArray $ arr1 `mappend` arr2 

-- Couldn't match type 'S 'Z with 'Z … 
-- Expected type: Sized M Ns (Sum Int) 
-- Actual type: Sized M Ns' (Sum Int) 
-- In the second argument of `mappend', namely `arr2' 
-- In the first argument of `mappend', namely `arr1 `mappend` arr2' 

Full code：あなたが誤って異なる次元での配列を合計しようと、あなたは型エラーを取得します。 user3237465さん@

Answer 2

はArray sの静的なサイズ情報を付加に関するご質問への完全かつ直接的な答えです。しかし、あなたは従属型にはまったく新しいものだと言って以来、私はトピックのより良い紹介として役立つかもしれないと思うマトリックス追加の簡単な例を挙げたいと思っていました。 the Hasochism paperには、以下のうちの多くが見つかりました。

いつものように、GHCは自動的にタイプレベルに上がる自然数を持っています。次data宣言タイプNatと2値コンストラクタZとSを定義するだけでなく、我々はまた、種類Natと2 タイプコンストラクタZとSを取得します。

data Nat = Z | S Nat 

type One = S Z 
type Two = S (S Z) 
type Three = S (S (S Z)) 

私は、運用上、その長さの静的な知識とリンクリストである慣習ベクトル GADTを定義するつもりです。

infixr 5 :> 
data Vec n a where 
    VNil :: Vec Z a 
    (:>) :: a -> Vec n a -> Vec (S n) a 
deriving instance Show a => Show (Vec n a) 

instance Functor (Vec n) where 
    fmap f VNil = VNil 
    fmap f (x :> xs) = f x :> fmap f xs 

ここにいくつかのベクター例があります。

v1 :: Vec Two String 
v1 = "foo" :> "bar" :> VNil 
v2 :: Vec Two String 
v2 = "baz" :> "quux" :> VNil 
v3 :: Vec One String 
v3 = "nabble" :> VNil 

タイプレベル番号の実行時分析を行う必要があります。例えば、与えられた要素n回を繰り返す関数vreplicate :: n -> a -> Vec n aを書こうとします。 vreplicateは実行時にを知っていなければなりません何枚の値をコピーするか！しかし、Haskellは実行時の値とコンパイル時の型を分離しているので、上記の型シグネチャは無効です。タイプNatに属するタイプは、実行時に渡すことはできません。 シングルトン値を入力します。

data Natty n where 
    Zy :: Natty Z 
    Sy :: Natty n -> Natty (S n) 

は、与えられた（明確に定義された）種類Natのnは、正確に1つの（明確に定義された）値が存在する場合（これはsingletonsライブラリがあなたのために。生成多かれ少なかれコードです）タイプNatty n。 Nattyのパターンマッチングでは、nが表示されます。数字のforall n. Natty n ->は、実行時にnが使用されることを示します。したがって、vreplicate関数のタイプはNatty n -> a -> Vec n aで、はランタイムスタンドとしてnです。

前述したように、Nattyの値を知っていれば、nを知っているはずですが、実際には、このようなフープでジャンプすることはありません。我々は、さらに以下のハック型クラスを使用して、情報がタイプからの値に、他の道を流れて作ることができます。

class NATTY n where 
    natty :: Natty n 
instance NATTY Z where 
    natty = Zy 
instance NATTY n => NATTY (S n) where 
    natty = Sy natty 

NATTY n辞書はnのシングルトンNattyの暗黙のコピーです。

OK。VecのApplicativeインスタンスは、2つのベクトルをまとめ、その内容をポイントワイズに組み合わせます。

vzip :: Vec n a -> Vec n b -> Vec n (a, b) 
vzip VNil VNil = VNil 
vzip (x :> xs) (y :> ys) = (x, y) :> vzip xs ys 

vreplicate :: Natty n -> a -> Vec n a 
vreplicate Zy _ = VNil 
vreplicate (Sy n) x = x :> vreplicate n x 

instance NATTY n => Applicative (Vec n) where 
    pure = vreplicate natty 
    fs <*> xs = fmap (uncurry ($)) (vzip fs xs) 

だから、我々はaのベクトルに対してMonoidにMonoida用のを持ち上げることができます。これはApplicativeをMonoidにする標準的な方法です。

instance Monoid a => Monoid (Vec n a) where 
    mempty = pure mempty 
    mappend = liftA2 mappend 

報酬：mappend長さが一致するベクトルのみが可能です。これをリストzipと比較すると、2つのリストのうち長い方が圧縮されたものが切り捨てられます。

ghci> v1 `mappend` v2 
"foobaz" :> ("barquux" :> VNil) 

-- ┌  ┐  ┌  ┐  ┌   ┐ 
-- | "foo" | + | "baz" | = | "foobar" | 
-- | "bar" |  | "quux" |  | "bazquux" | 
-- └  ┘  └  ┘  └   ┘ 

ghci> v1 `mappend` v3 
<interactive>:35:14: error: 
    • Couldn't match type ‘'Z’ with ‘'S 'Z’ 
     Expected type: Vec Two String 
     Actual type: Vec One String 
    • In the second argument of ‘mappend’, namely ‘v3’ 
     In the expression: v1 `mappend` v3 
     In an equation for ‘it’: it = v1 `mappend` v3 

-- ┌  ┐  ┌   ┐ 
-- | "foo" | + | "nabble" | = ? 
-- | "bar" |  └   ┘ 
-- └  ┘ 

---

今度は2D行列で作業しましょう。そのトリックは、再利用可能な小さなビットからそれらを構築することです。行列はベクトルのベクトルで、2つのベクトルの型レベルの構成です。ある

newtype (f :.: g) a = Compose { getCompose :: f (g a) } deriving Show 

type Mat n m = Vec n :.: Vec m 

、Mat n m aはVec n (Vec m a)と同型です。

関手とapplicativityは、組成物を介して保持され、

instance (Functor f, Functor g) => Functor (f :.: g) where 
    fmap f = Compose . fmap (fmap f) . getCompose 
instance (Applicative f, Applicative g) => Applicative (f :.: g) where 
    pure = Compose . pure . pure 
    Compose fgf <*> Compose fgx = Compose (liftA2 (<*>) fgf fgx) 

、我々はもう一度構成Applicative SのApplicativeにMonoidを持ち上げるために、標準的なトリックを使用することができます。

instance (Monoid a, Applicative f, Applicative g) => Monoid ((f :.: g) a) where 
    mempty = pure mempty 
    mappend = liftA2 mappend 

ここで無料で行列を追加します。

m1 :: Mat Two Two String 
m1 = Compose (v1 :> v2 :> VNil) 
m2 :: Mat Two Two String 
m2 = Compose (v2 :> v1 :> VNil) 

ghci> m1 `mappend` m2 
Compose {getCompose = ("foobaz" :> ("barquux" :> VNil)) :> (("bazfoo" :> ("quuxbar" :> VNil)) :> VNil)} 

-- ┌    ┐  ┌    ┐  ┌     ┐ 
-- | "foo" "bar" | + | "baz" "quux" | = | "foobaz" "barquux" | 
-- | "baz" "quux" |  | "foo" "bar" |  | "bazfoo" "quuxbar" | 
-- └    ┘  └    ┘  └     ┘ 

memptyとしてのアイデンティティ行列で、行列の乗算を行う（正方行列に対して、newtype Square n = Square (Mat n n)）別の有効な行列Monoidあります。私はここには示しません。あなた自身でそれを理解することができます。

---

最後のはN次元の行列であるテンソルの追加を行いましょう。テンソルは、ディメンションのリストによってインデックスされた型のファミリです。つまり、Tensorは、ファンクションで、次元のリストから型コンストラクタ* -> *になります。リストに新しいディメンションを追加すると、Vecのレイヤーが追加されます。

type family Tensor (dims :: [Nat]) :: * -> * where 
    Tensor '[d] = Vec d 
    Tensor (d ': ds) = Vec d :.: Tensor ds 

ので、Tensor '[One, Two, Three] a、1×2×3テンソルは、Vec One (Vec Two (Vec Three a))に-isomorphic newtypeです。

もう一度、Vecと:.:の形でTensorを定義すると、私たちが必要とするインスタンスが無料で取得されます。

t1 :: Tensor '[Two, Two, Two] String 
t1 = Compose (m1 :> m2 :> VNil) 
t2 :: Tensor '[Two, Two, Two] String 
t2 = Compose (m2 :> m1 :> VNil) 

ghci> t1 `mappend` t2 
Compose {getCompose = Compose {getCompose = ("foobaz" :> ("barquux" :> VNil)) :> (("bazfoo" :> ("quuxbar" :> VNil)) :> VNil)} :> (Compose {getCompose = ("bazfoo" :> ("quuxbar" :> VNil)) :> (("foobaz" :> ("barquux" :> VNil)) :> VNil)} :> VNil)} 

-- i'm not going to try drawing that