如何将依赖大小的数组推广到n维？

Question

我一直在玩弄这一段时间，但我还没有能够说服GHC做这件事。

基本上它是很容易的创建哈斯克尔/ GHC的当前版本依赖性大小的数组：

newtype Arr1 (w :: Nat) a = Arr1 (Int -> a) 
newtype Arr2 (w :: Nat) (h :: Nat) a = Arr2 (Int -> a) 

ix2 :: forall w h a. (KnownNat w) => Arr2 w h a -> Int -> Int -> a 
ix2 (Arr2 f) x y = f (y * w + x) 
    where w = fromInteger $ natVal (Proxy :: Proxy w) 

sub2 :: forall w h a. (KnownNat w) => Arr2 w h a -> Int -> Arr1 w a 
sub2 (Arr2 f) y = Arr1 $ \x -> f (y * w + x) 
    where w = fromInteger $ natVal (Proxy :: Proxy w) 

mkArr2V :: forall w h a. (V.Unbox a, KnownNat w, KnownNat h) => V.Vector a -> Arr2 w h a 
mkArr2V v = Arr2 $ (v V.!) 

-- and so on ... errorchecking neglected 

但是，目前GHC版本给我们带来更多的表达性。基本上，它应该有可能为此创建一个单一类型：

newtype Mat (s :: [Nat]) a = Mat (Int -> a) 

-- create array backed by vector 
mkMatV :: forall s a. V.Vector a -> Mat s a 
mkMatV v = Mat $ (v V.!) 

此作品在GHCI：

>>> let m = mkMatV (V.fromList [1,2,3,4]) :: Mat [2,2] Double 
>>> :t m 
m :: Mat '[2, 2] Double 

但到了这一点，我就如何完成索引到数组不确定。一个简单的解决方案是对nd和1d索引使用两种不同的函数。请注意，这不是typecheck。

-- slice from nd array 
(!) :: forall s ss a. (KnownNat s) => Mat (s ': ss) a -> Int -> Mat ss a 
(!) (Mat f) o = Mat $ \i -> f (o*s+i) 
    where s = fromInteger $ natVal (Proxy :: Proxy (sum ss)) 

-- index into 1d array 
(#) :: forall s ss a. (KnownNat s) => Mat (s ': '[]) a -> Int -> a 
(#) (Mat f) o = Mat $ \i -> f o 

大概可用这样的：

>>> :t m ! 0 
Mat [2] Double 
>>> m ! 0 # 0 
1 

这并不是说，有必要在给予Z，Y，X次序索引。我的首选解决方案将提供一个索引函数，根据数组的维度更改它的返回类型。据我所知，这可以以某种方式通过使用类型类来实现，但我还没有想到。如果指数可以按“自然”x，y，z顺序给出，则为积分。

tl; dr：我要求一个函数索引如上定义的n维数组。

Answer 1

这确实可以通过类型类来完成。一些预备：

{-# LANGUAGE 
    UndecidableInstances, MultiParamTypeClasses, TypeFamilies, 
    ScopedTypeVariables, FunctionalDependencies, TypeOperators, 
    DataKinds, FlexibleInstances #-} 

import qualified Data.Vector as V 

import GHC.TypeLits 
import Data.Proxy 

newtype NVec (shape :: [Nat]) a = NVec {_data :: V.Vector a} 

在别的之前，我们应该能够告诉一个n维向量的整体平面大小。我们将使用它来计算索引的步幅。我们使用一个类在类型级别列表上进行递归。

class FlatSize (sh :: [Nat]) where 
    flatSize :: Proxy sh -> Int 

instance FlatSize '[] where 
    flatSize _ = 1 

instance (KnownNat s, FlatSize ss) => FlatSize (s ': ss) where 
    flatSize _ = fromIntegral (natVal (Proxy :: Proxy s)) * flatSize (Proxy :: Proxy ss)  

我们也使用一个类型的类来建立索引。我们为一维情况（其中我们简单地索引底层向量）和高维情况（其中我们返回具有减少的维度的新的NVec）提供不同的实例。不过，我们对这两种情况使用相同的类。

infixl 5 !            
class Index (sh :: [Nat]) (a :: *) (b :: *) | sh a -> b where 
    (!) :: NVec sh a -> Int -> b 

instance Index '[s] a a where 
    (NVec v) ! i = v V.! i   

instance (Index (s2 ': ss) a b, FlatSize (s2 ': ss), res ~ NVec (s2 ': ss) a) 
    => Index (s1 ': s2 ': ss) a res where 
    (NVec v) ! i = NVec (V.slice (i * stride) stride v) 
    where stride = flatSize (Proxy :: Proxy (s2 ': ss)) 

索引到一个更高维的矢量只是用所得到的矢量的平坦大小和适当的偏移来切片。

一些测试：

fromList :: forall a sh. FlatSize sh => [a] -> NVec sh a 
fromList as | length as == flatSize (Proxy :: Proxy sh) = NVec (V.fromList as) 
fromList _ = error "fromList: initializer list has wrong size" 

v3 :: NVec [2, 2, 2] Int 
v3 = fromList [ 
    2, 4, 
    5, 6, 

    10, 20, 
    30, 0 ] 

v2 :: NVec [2, 2] Int 
v2 = v3 ! 0 

vElem :: Int 
vElem = v3 ! 0 ! 1 ! 1 -- 6 

---

作为一个额外的，让我提出一个解决方案singletons过，因为它是相当多的便利。它让我们可以重用更多的代码（对于单个函数，使用更少的自定义类型类）并以更直接，实用的风格进行编写。

{-# LANGUAGE 
    UndecidableInstances, MultiParamTypeClasses, TypeFamilies, 
    ScopedTypeVariables, FunctionalDependencies, TypeOperators, 
    DataKinds, FlexibleInstances, StandaloneDeriving, DeriveFoldable, 
    GADTs, FlexibleContexts #-} 

import qualified Data.Vector as V 
import qualified Data.Foldable as F 
import GHC.TypeLits 
import Data.Singletons.Preludeimport 
import Data.Singletons.TypeLits 

newtype NVec (shape :: [Nat]) a = NVec {_data :: V.Vector a} 

flatSize变得简单多了：我们只是降低sh到价值层面，并在其上照常工作：

flatSize :: Sing (sh :: [Nat]) -> Int 
flatSize = fromIntegral . product . fromSing 

我们用一个类型的家庭和索引功能。在之前的解决方案中，我们使用实例来分派维度;在这里，我们做同样的模式匹配：

type family Index (shape :: [Nat]) (a :: *) where 
    Index (s ': '[])  a = a 
    Index (s1 ': s2 ': ss) a = NVec (s2 ': ss) a 

infixl 5 ! 
(!) :: forall a sh. SingI sh => NVec sh a -> Int -> Index sh a 
(!) (NVec v) i = case (sing :: Sing sh) of 
    SCons _ SNil  -> v V.! i 
    SCons _ ss@SCons{} -> NVec (V.slice (i * stride) stride v) where 
    stride = flatSize ss 

我们还可以使用Nat单身安全索引和初始化（即与静态检查范围和大小。）。为了初始化，我们定义一个具有静态大小的列表类型（Vec）。

safeIx :: 
    forall a s sh i. (SingI (s ': sh), (i + 1) <= s) => 
    NVec (s ': sh) a -> Sing i -> Index (s ': sh) a 
safeIx v si = v ! (fromIntegral $ fromSing si)      

data Vec n a where 
    VNil :: Vec 0 a 
    (:>) :: a -> Vec (n - 1) a -> Vec n a 
infixr 5 :> 
deriving instance F.Foldable (Vec n) 

fromVec :: forall a sh. SingI sh => Vec (Foldr (:*$) 1 sh) a -> NVec sh a 
fromVec = fromList . F.toList 

的安全功能的一些例子：

-- Other than 8 elements in the Vec would be a type error 
v3 :: NVec [2, 2, 2] Int 
v3 = fromVec 
    (2 :> 4 :> 
     5 :> 6 :> 

     10 :> 20 :> 
     30 :> 0 :> VNil) 

vElem :: Int 
vElem = v3 
    `safeIx` (sing :: Sing 0) 
    `safeIx` (sing :: Sing 1) 
    `safeIx` (sing :: Sing 1) -- 6