不同大小的向量，其中类型“在其他地方工作”

Question

假设我有一个函数，可以处理编译时已知大小的向量（这些由包提供vector-sized）：

{-# LANGUAGE DataKinds, GADTs #-}
module Test where
import Data.Vector.Sized

-- Processes vectors known at compile time to have size 4.
processVector :: Vector 4 Int -> String
processVector = undefined

很好，但是如果我不想处理整数向量，而是向量向量怎么办？

-- Same thing but has subvectors of size 3.
processVector2 :: Vector 4 (Vector 3 Int) -> String
processVector2 = undefined

很好，但是每个子向量都有固定的大小。我想要一个函数，其中子向量可以具有不同的大小，但在编译时仍然已知。

我们可以通过存在量化来做到这一点：

data InnerVector = forall n. InnerVector (Vector n Int)
processVector3 :: Vector 4 InnerVector -> String
processVector3 = undefined

很好，但是如果我想返回的不是字符串而是相同维度的向量怎么办？

processVector4 :: Vector 4 InnerVector -> Vector 4 InnerVector
processVector4 = undefined

这不起作用，因为第二个向量可能具有与输入子向量不同大小的子向量！我希望它们在编译时是相同的。（因此索引 0 处的子向量具有相同的大小，索引 1 处的子向量具有相同的大小，依此类推。）

这有可能实现吗？如果没有，您是否知道（或者您可以创建）一种可以实现这一点的数据结构吗？

我避免使用元组是因为：

• 我的向量的大小将超过 100。
• 向量使一般处理变得容易（使用基于 0 的索引），因此即使我向向量添加更多项目，我的处理函数仍然可以继续工作。
• 我确实只想要内部向量中的一种类型的值（Int在示例中）。

Answer 1

通过使用存在量化，您可以有效地隐藏内部向量的大小。但是，如果您想编写带有类型的代码来表明您正在保留这些大小，那么您不希望它们被隐藏。相反，你希望你的类型能够大声而清晰地表达它们。

因此，让我们定义一些广播这些内部尺寸的类型。本质上，您需要“向量的向量”类型是一种异构列表，它将这些列表的元素限制为向量。当然，有一些库可以帮助您组合这样的类型，但在这里我们将推出自己的库。只是因为这样做更有趣。

让我们从启用一些语言扩展开始，然后为内部向量及其大小编写一些类型：

{-# LANGUAGE DataKinds, GADTs, InstanceSigs, KindSignatures, TypeOperators #-}

data Nat = Zero | Succ Nat

data Vector :: Nat -> * -> * where
  VNil  :: Vector Zero a
  VCons :: a -> Vector n a -> Vector (Succ n) a

instance Functor (Vector n) where
  fmap f VNil         = VNil
  fmap f (VCons x xs) = VCons (f x) (fmap f xs)

接下来是我们的“锯齿状”矩阵类型（即可变大小向量的向量）。如前所述，这只是一种特定类型的异构列表：

data JaggedMatrix :: [Nat] -> * -> * where
  MNil  :: JaggedMatrix '[] a
  MCons :: Vector n a -> JaggedMatrix ns a -> JaggedMatrix (n : ns) a

就在那里，就是这样。锯齿状矩阵的类型由包含内部向量大小的列表索引。外部尺寸未在类型中说明，但可以简单地从内部尺寸列表的长度导出。

让我们将其付诸实践并编写一个维度保留函数。这是一个明显的例子：

instance Functor (JaggedMatrix ns) where
  fmap :: (a -> b) -> JaggedMatrix ns a -> JaggedMatrix ns b
  fmap f MNil           = MNil
  fmap f (MCons xs xss) = MCons (fmap f xs) (fmap f xss)