矢量创作安全

Question

这个问题实际上是一个非常密切相关问题的小格子; 我认为将它分解为止并不是很有意义.

创建a的基本方法之一Vector就是使用unsafeFreeze.顾名思义,unsafeFreeze真的是不安全的.特别是,没有什么能阻止MVector传递的内容unsafeFreeze在被冻结后被修改.这导致了两个不同的问题:

1. 它可以使"不可变"向量的值发生变化.这只是Haskell一般避开的那种怪异动作.

2. 修改冻结的矢量可以(至少可能)混淆垃圾收集器.没有文件证明垃圾收集器将扫描冻结的阵列以确保其内容被撤离.更一般地说,绝对禁止变异载体变异,这样做的结果完全没有说明.

所述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不能发挥任何有趣的技巧),冻结它,并返回冻结的矢量.

createTTraversable实例合法时非常安全.例如,使用列表createT m运行生成MVectors 列表的操作,然后将它们全部冻结.s那时的参数似乎就足够了create,以确保没有任何不好的事情发生.请注意,该操作可能会创建一个包含多个副本的列表MVector.这些将被冻结两次,但不应该有任何伤害.合法的Traversable实例看起来都像装饰列表,因此它们应该表现得相似.现在我终于得出了第一个问题:

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)但是返回a [Vector a].什么时候t ~ u,这显然createT和非法Traversable实例一样安全.改变"容器"类型的额外灵活性是否会降低安全性？编辑:我刚才意识到我可以回答这个问题:不,它没有任何区别.有关说明,请参见下面的[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)

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

---

我确实说过我会谈论一个格子,对吧？接下来的问题是我们可以在多大程度上(如果有的话)削弱遍历的多态性而不会造成麻烦.即使遍历只需要是多态的s,所有东西都会进行类型检查,但这显然是不安全的,因为它可以将冻结与修改交错,但它喜欢.揭示的最终结果持有Vector价值很可能是足够无害的,但我们一定不能让遍历知道这两个,它是在工作ST s 和它所受理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字典.

另一方面,我怀疑我们可以让遍历知道它正在处理MVector...只要我们不让它知道它们与哪个状态线程相关联.这足以打开它们,并且(也许不幸的是)获得它们的大小.

编辑!如果允许遍历知道它正在产生Vectors(这似乎是最不可能的问题),那么createTOfThen可以用以下方式实现createTOf:

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

---

从第三个方向看格子,让我们继续进行排名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)

我们可以用这个完全相同的游戏来生成s的异构容器Vector:

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.我想象的是,等级2版本的安全性能是相同的那些对应等级的-1版本,但我没有一个线索会如何证明这样.

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

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

这实际上是完全的,虽然"遍历"是部分的:我们总是会在我们肯定会发现的情况下匹配.

Answer 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

这确实是一个相当拗口的类型签名！让我们密切关注我们关心的安全属性：noMVector被冻结后不会发生变异。我们做的第一件事就是运行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其中有向量，则这些向量位于状态 thread 中s1。然而，结果是状态 thread 中的一个操作s2。因此trav无法修改MVector使用常规操作给出的 s 。它只能应用它所需要的功能（将是unsafeFreeze），并使用 上可能使用的任何机制t。什么样的机械可以乘坐t？好吧，这是一个愚蠢的例子：

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

trav这些操作可以ST与冻结交织在一起吗？不！这些ST操作与MVectors 匹配，但与线程运行的状态不匹配。因此无法对它们执行任何操作。travtrav