haskell - 数组和类型类提升(和依赖类型？)

Question

假设类型 b 是 Monoid 的一个实例并且对于 (v1,v2)::(i,i) 的固定索引范围 with i 属于类型类 Ix 我想将相应的 Data.Array 类型也定义为 Monoid。如何才能做到这一点？这里，mempty 应该是包含条目 mempty::b 的数组，数组的 mappend 应该是 mappend -操作组件明智。

(例如，如果 i=(Int,Int) 类型 Data.Array i b 表示具有不同大小(和不同范围的)的所有(二维)矩阵索引)。仅对于固定大小，这样的 Monoid 声明才有意义。实际上，我对向量空间的情况而不是 Monoid 感兴趣，但是 Monoid 已经显示出困难。我只有一个模糊的关于依赖类型的想法，但这似乎是一个原型(prototype)示例，在这种情况下，对应于一个参数范围的唯一子集的单个类型将很有用。)

Answer 1

一种常见的方法是将一个非非常类型化的表示包装成一个更类型化的表示，如下所示:

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 是一个提升的(参见 Giving Haskell a Promotion )幻像(参见 Motivation behind Phantom Types? )值 — 维度大小的列表，m 是这个的长度列表(以及提升和幻影)。因此，Sized 包装器下的任何数组都被假定为多维矩阵，其中 ns 表示其维度。 Monoid 实例看起来像这样:

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)

SingI 的内容来自 singletons图书馆。单例允许将值提升到类型级别，因此我们可以模拟依赖类型，SingI 允许通过 fromSing 函数将提升的值返回到值级别。 listSized 本质上是 listArray，但对于具有静态已知维度的数组，因此它要求所有这些 SingI 都在范围内。这是它的定义:

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 计算给定提升的维度大小列表的边界。它返回一个元组，其第一个组件是最低索引，它始终采用 [0,0..0] 的形式(零的数量与维数一样多，即 m).第二个组成部分是最大的索引，所以如果你例如有一个维度大小的列表，如 [2, 1, 3](表示为 [S (S Z), S Z, S (S (S Z))])，那么最大索引是[1, 0, 2]。

只需要为 Vec n a 提供一个 Ix 实例，它是 the product instances 的直接推广。 :

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

然后我们可以编写一些测试:

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 .