Haskell中的大小索引可变数组

Question

在Haskell中,可以在大小索引列表上编写函数,以确保我们永远不会超出范围.可能的实现是:

data Nat = Zero | Succ Nat deriving (Eq, Ord, Show)

infixr 5 :-

data Vec (n :: Nat) a where
    Nil  :: Vec 'Zero a
    (:-) :: a -> Vec n a -> Vec ('Succ n) a       

data Fin (n :: Nat) where
    FZ :: Fin ('Succ n)
    FS :: Fin n -> Fin ('Succ n)                       

vLookup :: Vec n a -> Fin n -> a
vLookup Nil _ = undefined           
vLookup (x :- _) FZ = x
vLookup (_ :- xs) (FS i) = vLookup xs i                      

当然,这对于不可变大小的索引列表(aka Vec)来说很好.

但可变的呢？是否可以在Haskell中定义(或是否存在库)可变大小索引数组？如果没有这样的库,它是如何实现的？

编辑1:我搜索了Hackage并没有找到任何匹配我的描述的库(大小索引的可变数组).

编辑2:我想提一下,我曾经想过使用IORef's来获得所需的可变性:

 type Array n a = IORef (Vec n a)

但我想知道是否有更好(更高效,更优雅)的选择......

Answer 1

Hackage上确实存在这样的类型.

我会避免类似的事情type Array n a = IORef (Vec n a).可变阵列都与效率有关.如果你不需要快速运行/内存占用少,那么使用它们就没有多大意义 - 即使是"可变算法"通常也更容易在Haskell中使用函数式表达,也许是使用状态monad但没有真正的破坏性可变状态.
但是,如果效率很重要,那么您还需要高效的缓存高效存储.未装箱的矢量是理想的.OTOH,Vec在运行时数据级别上与普通列表没有什么不同,在高速缓存一致性方面当然不是那么好.即使你将它们定义为实际将可变性交织到列表脊柱中,它也不会比Vec在纯函数式中使用不可变s 更好.

因此,如果我必须编写类似这样简单的东西,我宁愿在长度索引的newtype中包装一个(不安全的,长度方式的)未装箱的可变arrox.

import qualified Data.Vector.Unboxed.Mutable as VUM

newtype MVec (s :: *) (n :: Nat) (a :: *)
        = MVec { getMVector :: VUM.MVector s a }

然后,您可以定义一个接口,使所有公共操作类型检查长度安全,同时仍保留性能配置文件MVector.