矢量创建安全答案

【问题标题】：Vector creation safety矢量创建安全
【发布时间】：2018-04-12 21:06:08
【问题描述】：

这个问题实际上是一个非常密切相关的问题的小格子；我认为现在拆分它没有多大意义。

创建Vector 的基本方法之一是使用unsafeFreeze。顾名思义，unsafeFreeze 确实不安全。特别是，没有什么可以阻止传递给unsafeFreeze 的MVector 在冻结后被修改。这会导致两个不同的问题：

它可以使“不可变”向量的值发生变化。这只是 Haskell 通常回避的那种离奇的动作。
修改冻结的向量可能（至少可能）混淆垃圾收集器。没有文档保证垃圾收集器将扫描冻结的数组以确保其内容被撤出。更一般地说，绝对禁止在冻结时对向量进行变异，这样做的结果完全没有说明。

vector 包[1] 为创建不可变向量提供了两个高效、看似安全的原语：create 和 createT：

create :: (forall s. ST s (MVector s a)) -> Vector a
createT :: Traversable t => (forall s. ST s (t (MVector s a))) -> t (Vector a)

忽略向量融合业务，基本实现是这样的

create m = runST $ m >>= unsafeFreeze
createT m = runST $ m >>= traverse unsafeFreeze

create 显然是安全的。它运行给定的ST s 动作，它必须创建一个新的MVector s（runST 的类型确保它不能使用现有的，并且还确保fixST 不能玩任何有趣的技巧），冻结它，并返回冻结的向量。

当Traversable 实例合法时，createT 显然是安全的。例如，对于列表，createT m 运行一个操作，生成一个 MVectors 列表，然后将它们全部冻结。 s 中的参数化似乎就足够了，至于create，可以确保不会发生任何不好的事情。请注意，操作可能会创建一个包含多个相同MVector 副本的列表。这些将被冻结两次，但这不应该有任何伤害。合法的Traversable 实例all look pretty much like decorated lists，因此它们的行为应该相似。现在我终于遇到了我的第一个问题：

createT 与非法的Traversable 实例一起使用是否安全？

非法丢弃、复制或重新排列某些元素或更改装饰（违反身份法）不会造成任何明显的困难。参数化可以防止任何有趣的违反自然法则的行为，所以它已经过时了。我还没有找到一种方法来通过违反组成法或整体性来制造麻烦，但这并不能保证没有。

概括createT 的一个明显方法是允许用户传递他们自己的遍历函数：

createTOf
  :: (forall f x y. Applicative f => (x -> f y) -> t x -> f (u y))
  -> (forall s. ST s (t (MVector s a))) -> u (Vector a)
createTOf trav m = runST $ m >>= trav unsafeFreeze

请注意，我允许遍历将容器类型从 t 更改为 u。例如，这允许用户生成Vector (MVector s a)，但返回[Vector a]。当t ~ u 时，这显然与带有非法Traversable 实例的createT 一样安全。更改“容器”类型的额外灵活性是否会降低安全性？ 编辑：我刚刚意识到我可以回答这个问题：不，没有区别。有关说明，请参阅下面的 [2]。

当我们使用createT 时，我们可能实际上并不想要一个向量容器；也许我们想遍历那个容器来得到别的东西。我们可以写类似

traverse f <$> createT m

createTOf 的额外类型灵活性意味着我们手上不一定有Traversable，也不一定能做到这一点。但是使用Traversable的组合法则，我们可以将这个遍历整合到创建函数中：

createTOfThen
  :: Applicative g
  => (forall f x y. Applicative f => (x -> f y) -> t x -> f (u y))
  -> (Vector a -> g b)
  -> (forall s. ST s (t (MVector s a)))
  -> g (u b)
createTOfThen trav f m =
  runST $ m >>= getCompose . trav (Compose . fmap f . unsafeFreeze)

如果trav 不是合法遍历，createTOfThen 是否安全？

我确实说过我会谈论格子，对吧？下一个问题是我们可以在多大程度上（如果有的话）削弱遍历的多态性而不会造成麻烦。即使在s 中只要求遍历是多态的，一切都会进行类型检查，但这显然是不安全的，因为它可以将冻结与修改交错，但它喜欢。揭示最终结果包含 Vector 值似乎可能是无害的，但我们肯定不能让遍历知道 both 它正在 ST s 中运行 /em> 它正在处理 MVector s a 值。但是我们可以让它知道其中一个事实吗？修复Applicative 肯定会有用：

createTOf'
  :: (forall s x y. (x -> ST s y) -> t x -> ST s (u y))
  -> (forall s. ST s (t (MVector s a))) -> u (Vector a)

createTOfThen'
  :: Applicative g
  => (forall s x y. (x -> Compose (ST s) g y) -> t x -> Compose (ST s) g (u y))
  -> (Vector a -> g b)
  -> (forall s. ST s (t (MVector s a)))
  -> g (u b)

这将提供更有效的创建诸如向量向量之类的东西，因为向量可以在ST 中比在任意Applicative 函子中更有效地遍历。它还可以减少对内联的依赖，因为我们可以避免处理 Applicative 字典。

另一方面，我怀疑我们可以让遍历知道它正在处理MVectors ...只要我们不让它知道它们与哪个状态线程相关联。这足以将它们拆箱，并且（可能很遗憾）还可以获取它们的尺寸。

编辑！如果允许遍历知道它正在产生Vectors（这似乎是最不可能有问题的事情），那么createTOfThen可以按照以下方式实现createTOf:

createTOfThen trav post m = getConst $
  createTOf (\f ->
    fmap Const . getCompose . (trav (Compose . fmap post . f))) m

在第三个方向上考虑格子，让我们继续进行 rank-2 遍历。 rank2classes 包提供了自己的 Traversable 类，我将其称为 R2.Traversable：

class (R2.Functor g, R2.Foldable g) => R2.Traversable g where
  R2.traverse :: Applicative m
              => (forall a. p a -> m (q a))
              -> g p -> m (g q)

我们可以用它完全玩同样的游戏来生成Vectors的异构容器：

createTHet
  :: R2.Traversable t
  => (forall s. ST s (t (MVector s)))
  -> t Vector
createTHet m = runST $ m >>= R2.traverse unsafeFreeze

createTHetOf
  :: (forall h f g.
       (Applicative h => (forall x. f x -> h (g x)) -> t f -> h (u g)))
  -> (forall s. ST s (t (MVector s)))
  -> u Vector
createTHetOf trav m = runST $ m >>= trav unsafeFreeze

createTHetOfThen
  :: Applicative q
  => (forall h f g.
       (Applicative h => (forall x. f x -> h (g x)) -> t f -> h (u g)))
  -> (forall x. Vector x -> q (r x))
  -> (forall s. ST s (t (MVector s)))
  -> q (u r)
createTHetOfThen trav post m =
    runST $ m >>= getCompose . trav (Compose . fmap post . unsafeFreeze)

以及允许遍历知道它在ST s 中工作的类似版本。我会想象 rank-2 版本的安全属性与相应的 rank-1 版本相同，但我不知道如何证明这一点。 p>

只是为了好玩，我认为我的格子的顶部是下面的怪物。如果这些想法中的任何一个不安全，那么这个想法可能是：

createTHetOfThen'
  :: (forall s1 s2.
       ((forall x. MVector s2 x -> Compose (ST s1) q (r x)) -> t (MVector s2) -> Compose (ST s1) q (u r)))
  -> (forall x. Vector x -> q (r x))
  -> (forall s. ST s (t (MVector s)))
  -> q (u r)
createTHetOfThen' trav post m =
    runST $ m >>= getCompose . trav (Compose . fmap post . unsafeFreeze)

[1] 我已链接到 Stackage，因为 Hackage 今天停止运行。如果我记得并且有时间，我会稍后修复链接。

[2] 证明来自Data.Functor.Sum。给定一个不改变类型的createTOfSame，我们可以这样写

createTOf
  :: (forall f a b. Applicative f => (a -> f b) -> t a -> f (u b))
  -> (forall s. ST s (t (MVector s a)))
  -> u (Vector a)
createTOf trav m =
  case createTOfSame (\f (InL xs) -> InR <$> trav f xs)
                     (InL <$> m) of
    InR u -> u

这实际上是全部的，尽管“遍历”是部分的：我们总是对肯定会找到的内容进行大小写匹配。

【问题讨论】：

标签： arrays haskell vector higher-rank-types traversable

【解决方案1】：

将这个想法推向极限实际上帮助我更好地理解它，我现在相当确信所有这些功能都是安全的。考虑

createTOf
  :: (forall s1 s2.
       (MVector s1 a -> ST s2 (Vector a))
       -> t (MVector s1 a) -> ST s2 (u (Vector a)))
  -> (forall s. ST s (t (MVector s a)))
  -> u (Vector a)
createTOf trav m = runST $ m >>= trav unsafeFreeze

这当然是一大口类型签名！让我们密切关注我们关心的安全属性：MVector 在冻结后不会发生突变。我们要做的第一件事是运行m 来生成t (MVector s a) 类型的东西。

t 现在很神秘。是容器吗？是某种产生向量的动作吗？我们真的不能说太多关于它是什么，但我们可以说一些关于trav unsafeFreeze不能用它做什么的事情。让我们从分解trav的类型签名开始：

trav :: forall s1 s2.
        (MVector s1 a -> ST s2 (Vector a))
     -> t (MVector s1 a) -> ST s2 (u (Vector a)))

trav 将t (MVector s1 a) 变成ST s2 (u (Vector a))。如果t 中有向量，那么这些向量存在于状态线程s1 中。然而，结果是状态线程s2 中的一个操作。所以trav 不能修改使用通常操作给出的MVectors。它只能应用它所需要的功能（将是unsafeFreeze），并使用任何可能在t 上运行的机器。 t 可以搭载什么样的机器？好吧，这是一个愚蠢的例子：

data T :: Type -> Type where
  T :: [ST s (MVector s a)] -> t (MVector s a)

trav 可以将这些ST 操作与冻结交错吗？不！那些ST 动作匹配MVectors，但它们不匹配trav 操作的状态线程。所以trav 不能对它们做任何事情。

【讨论】：