14

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

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

  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。例如，这允许用户产生 aVector (MVector s a)但取回 a [Vector a]。当 时，这显然与非法实例t ~ u一样安全。更改“容器”类型的额外灵活性是否会降低安全性？编辑：我刚刚意识到我可以回答这个问题：不，没有区别。有关说明，请参见下面的 [2]。createTTraversable

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

traverse f <$> createT m

额外的类型灵活性createTOf意味着我们不一定有 aTraversable在我们手上，也不一定能做到这一点。但是使用 的组合律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 aApplicative

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

将晶格放在第三方向，让我们继续进行 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)

我们可以用它玩完全相同的游戏来生成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。我想rank -2 版本的安全属性与相应的 rank-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

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

4

1 回答 1

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其中有向量，则这些向量存在于状态线程s1中。然而，结果是状态线程中的一个动作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 匹配，但它们与运行的状态线程不trav匹配。所以trav不能对它们做任何事情。

于 2018-04-14T21:22:43.610 回答