1

（这是这个答案的后续，试图让 q 更精确。）

用例构造函数来构建/访问Set数据类型。作为一个集合，不变量是“无重复”。为了实现这一点，我需要Eq对元素类型进行约束。（更现实地，该集合可能被实现为 BST 或哈希索引，这将需要一个更严格的约束；使用Eq这里来保持简单。）

  • 我想禁止建立一个不可接受的类型的空集。
  • “现在认为对不需要约束的操作（数据类型构造或破坏）进行约束是不好的做法。相反，约束应该移近“使用站点”。”，引用该答案。
  • 好的，因此无需将约束“内置”到数据结构中。访问/解构的操作（如showing 或计数元素）不一定需要Eq.

然后考虑两种（或更确切地说是五种）可能的设计：

（我知道一些约束可以通过deriving, esp Foldableto get来实现elem。但我会在这里手动编码，所以我可以看到 GHC 想要的最小约束。）

选项 1：对数据类型没有限制

data NoCSet a  where                             -- no constraints on the datatype
  NilSet_ :: NoCSet a
  ConsSet_ :: a -> NoCSet a -> NoCSet a

选项 1a。使用 PatternSynonym 作为“智能构造函数”

    pattern NilSet :: (Eq a) => () => NoCSet a
    pattern NilSet  = NilSet_

    pattern ConsSet x xs <- ConsSet_ x xs  where
      ConsSet x xs | not (elemS x xs) = ConsSet_ x xs 

    elemS x NilSet_                     = False
    elemS x (ConsSet_ y ys) | x == y    = True        -- infers (Eq a) for elemS
                            | otherwise = elemS x ys

  • GHC 推断约束elemS :: Eq t => t -> NoCSet t -> Bool。但它并没有推断出ConsSet使用它的约束。相反，它拒绝该定义：

    * No instance for (Eq a) arising from a use of `elemS'
  Possible fix:
    add (Eq a) to the "required" context of
      the signature for pattern synonym `ConsSet'

  • 好的，我会这样做，使用明确为空的“提供”约束：

    pattern ConsSet :: (Eq a) => () => ConsType a    -- Req => Prov'd => type; Prov'd is empty, so omittable

  • 因此推断 type (\(ConsSet x xs) -> x) :: Eq a => NoCSet a -> a，因此约束从析构函数（也从elemS）中“逃脱”，无论我在“使用站点”是否需要它。

选项 1b。将 GADT 构造函数包装为“智能构造函数”的模式同义词

    data CSet a where CSet :: Eq a => NoCSet a -> CSet a   -- from comments to the earlier q

    pattern NilSetC = CSet NilSet_                         -- inferred Eq a provided
    pattern ConsSetC x xs <- CSet (ConsSet_ x xs)  where   -- also inferred Eq a provided
      ConsSetC x xs | not (elemS x xs) = CSet (ConsSet_ x xs)

  • GHC 不会抱怨缺少签名，会推断pattern ConsSetC :: () => Eq a => a -> NoCSet a -> CSet a出提供的约束，但需要为空。

  • Inferred (\(ConsSetC x xs) -> x) :: CSet p -> p，因此约束不会从“使用站点”中逃脱。

  • 但是有一个错误：要 Cons 一个元素，我需要解开尾部NoCSet内部的内部CSet然后重新包装一个CSet. 并且尝试仅使用模式来做到这一点ConsSetC是错误的。反而：

    insertCSet x (CSet xs) = ConsSetC x xs    -- ConsSetC on rhs, to check for duplicates

  • 作为“智能构造函数”，这很愚蠢。我究竟做错了什么？

  • 推断insertCSet :: a -> CSet a -> CSet a，所以约束也没有逃脱。

选项 1c。将 GADT 构造函数包装为“更智能的构造函数”的模式同义词

  • 与选项 1b 相同的设置，除了这个怪物作为 Cons 模式的 ViewPattern

    pattern ConsSetC2 x xs <- ((\(CSet (ConsSet_ x' xs')) -> (x', CSet xs')) -> (x, xs))  where
  ConsSetC2 x (CSet xs) | not (elemS x xs) = CSet (ConsSet_ x xs)

  • GHC 不会抱怨缺少签名，而是pattern ConsSetC2 :: a -> CSet a -> CSet a完全没有限制地推断。我很紧张。但它确实正确地拒绝了构建具有重复项的集合的尝试。

  • 推断(\(ConsSetC2 x xs) -> x) :: CSet a -> a，因此不存在的约束不会从“使用站点”中逃脱。

  • 编辑：啊，我可以得到一个不那么可怕的ViewPattern表情来工作

    pattern ConsSetC3 x xs <- (CSet (ConsSet_ x (CSet -> xs)))  where
  ConsSetC3 x (CSet xs) | not (elemS x xs) = CSet (ConsSet_ x xs)

  • 奇怪地推断pattern ConsSetC3 :: () => Eq a => a -> CSet a -> CSet a——所以提供的约束是可见的，不像 with ConsSetC2，即使它们在道德上是等价的。它确实拒绝尝试构建具有重复项的集合。

  • 推断(\(ConsSetC3 x xs) -> x) :: CSet p -> p，因此存在的约束不会脱离“使用站点”。

选项 2：数据类型的 GADT 约束

data GADTSet a  where
  GADTNilSet  :: Eq a =>                   GADTSet a
  GADTConsSet :: Eq a => a -> GADTSet a -> GADTSet a

elemG x GADTNilSet                     = False
elemG x (GADTConsSet y ys) | x == y    = True              -- no (Eq a) 'escapes'
                           | otherwise = elemG x ys

GHC 推断没有可见的约束elemG :: a -> GADTSet a -> Bool；(\(GADTConsSet x xs) -> x) :: GADTSet p -> p.

选项 2a。使用 PatternSynonym 作为 GADT 的“智能构造函数”

    pattern ConsSetG x xs <- GADTConsSet x xs  where
      ConsSetG x xs | not (elemG x xs) = GADTConsSet x xs -- does infer Provided (Eq a) for ConsSetG
  • GHC 不会抱怨缺少签名，会推断pattern ConsSetG :: () => Eq a => a -> GADTSet a -> GADTSet a出提供的约束，但需要为空。
  • Inferred (\(ConsSetG x xs) -> x) :: GADTSet p -> p，因此约束不会从“使用站点”中逃脱。

选项 2b。定义插入函数

    insertGADTSet x xs | not (elemG x xs) = GADTConsSet x xs   -- (Eq a) inferred
  • GHC 推断insertGADTSet :: Eq a => a -> GADTSet a -> GADTSet a；所以Eq已经逃脱了，即使它没有逃脱elemG.

问题

  • 有了insertGADTSet，为什么约束会逃脱？它仅用于elemG检查，但elemG' 类型不会暴露约束。
  • 使用构造函数GADTConsSet, GADTNilSet，有一个约束“一直”包裹在数据结构中。这是否意味着数据结构比 with 具有更大的内存占用ConsSet_, NilSet_？
  • 使用构造函数GADTConsSet, GADTNilSet，它a“一直向下”是相同的类型。Eq a每个节点是否重复相同的字典？还是共享？
  • 相比之下，模式ConsSetC/constructor CSet/Option 1b 仅包装一个字典（？），因此它的内存占用比GADTSet结构（？）
  • insertCSetunwrapping 和 wrapping 对性能有影响CSet吗？
  • ConsSetC2在构建方向上似乎有效；展开和包装CSets 会影响性能吗？但更糟糕的是，在访问/遍历节点时会影响展开/包装性能吗？

（对于我的用例，我觉得在这些选项中没有灌篮高手。）

4

2 回答 2

2

我认为在任何现实情况下，不允许创建具有“不可接受”类型的空集是很重要的。至少部分是因为缺乏这种DatatypeContexts被认为是不好的做法的现实场景。说真的，试着想象这样的限制如何可能有助于避免现实世界的编程错误。也就是说，尝试想象使用您的类型和函数的人如何（1）编写一个错误的程序，（2）“意外”使用一组函数，但（3）以某种方式让它以某种方式进行类型检查如果只有Eq对NilSet. 一旦程序员试图对那个集合做任何使它非空的事情（即任何需要Eq功能），它不会进行类型检查，那么您到底想防止什么？您想阻止只需要空函数集的人使用您的类型吗？为什么？是怨恨吗？......这是怨恨，不是吗？

考虑到您的各种选择，将约束放在 GADT 中对我来说是不合适且不必要的。GADT 中的约束点是允许销毁以动态和/或有条件地将实例字典带入范围，基于运行时案例匹配。您不需要此功能。特别是，您不需要在每个Cons根据选项 2 的节点。但是，根据选项 1(b)，您也不需要数据类型中的字典。最好使用将字典传递给函数的普通非 GADT 机制，而不是在数据类型中携带它们。如果您尝试选项 1(b)，我预计您将错过许多专业化和优化的机会。部分原因可能是 GADT 本质上更难优化，但使用 GADT 优化代码的工作也比使用非 GADT 的代码少得多。您的一些问题表明您非常关心小的性能提升。如果是这样，远离 GADT 通常是个好主意！

选项 1(a) 是一个合理的解决方案。如果没有对 的不必要的 Eq 约束Nil，并且将插入函数折叠到模式定义中，您将得到如下内容：

{-# LANGUAGE PatternSynonyms #-}

data Set a = Nil | Cons_ a (Set a) deriving (Show)

pattern Cons :: (Eq a) => a -> Set a -> Set a
pattern Cons x xs <- Cons_ x xs
  where Cons x xs = go xs
          where go Nil = Cons_ x xs
                go (Cons_ y ys) | x == y = xs
                                | otherwise = go ys

正如设计的那样，这似乎是一个使用模式的完美惯用、直接、智能的构造函数实现。

确实，不幸的是，该约束适用于破坏，而实际上并不需要它。理想情况下，GHC 将允许Cons单独指定用作构造函数的约束，而不是假设它们是销毁所需约束和提供约束的组合。

这将允许我们编写如下内容：

pattern Cons :: a -> Set a -> Set a
pattern Cons x xs <- Cons_ x xs
  where Cons :: Eq a => a -> Set a -> Set a  -- <== only need Eq here
        Cons x Nil = Cons_ x Nil
        Cons x rest@(Cons_ y xs) | x == y = rest
                                 | otherwise = Cons_ y (Cons x xs)

然后Cons用作析构函数的用法可以不受约束，而用作构造函数可以利用Eq a约束。我认为这是一种限制，PatternSynonyms而不是表明添加不必要的约束实际上是一种很好的编程实践。 DatatypeContexts看起来至少其他一些人同意这是一个错误而不是一个功能。

对于您的前四个问题：

  • 在选项 2(b) 中，insertGADTSet需要将Eq a字典插入到GADTConsSetRHS 的构造函数中的字典槽中。因此，Eq a约束来自GADTConsSet构造函数的使用。
  • 是的，GADT 约束成为数据类型中的附加字段。在选项 2 中，将指向Eq a字典的指针添加到集合中的每个节点。
  • 字典本身是共享的，但每个节点都包含自己的字典指针。
  • 是的，对于该类型，每个值CSet只有一个指向字典的指针。CSet
于 2021-06-18T21:11:27.663 回答
-1

我相信选项 1b 是您最好的选择。当然，我可能有偏见，因为我是在你的另一个问题上提出这个建议的人。

为了解决您用模式同义词指出的问题，让我们假设我们没有模式同义词。我们如何解构 Cons 集？

一种方法是使用此签名编写方法：

openSetC :: CSet a -> (Eq a => a -> CSet a -> r) -> (Eq a => r) -> r

其中说，鉴于：

  • 一个CSet a，
  • 一个函数，它接受：一个证明Eq a，一个a，和另一个CSet a，并返回一些任意类型，
  • 和一个函数，它接受一个证明Eq a并返回相同的任意类型，

我们可以产生一个任意类型的值。由于类型是任意的，我们知道值来自调用函数，或者来自该类型的给定值。这个函数的约定是它调用第一个函数并返回它的结果当且仅当集合是ConsSet_，否则，如果它是NilSet_，它调用第二个函数。

如果你稍微眯眼，你会发现这个函数在某种意义上“等同于”模式匹配CSet。您根本不需要模式匹配；你可以用这个函数做任何你可以用模式匹配做的事情。

它的实现非常简单：

openSetC (CSet (ConsSet_ x xs)) k _ = k x (CSet xs)
openSetC (CSet NilSet_) _ z = z

现在考虑这个函数的另一种形式，它完成所有相同的事情，但可能更容易使用。

请注意，该类型forall r . (a -> r) -> (b -> r) -> r与Either a b. 另请注意，x0 -> y0 -> r它与 . 同构（或足够接近）(x0, y0) -> r。最后请注意，C a => r它与 where 同构Dict (C a) -> r：

data Dict c where Dict :: c => Dict c

如果我们利用这些同构，我们可以用openSetC不同的方式写成：

openSetC' :: CSet a -> Either (a, CSet a, Dict (Eq a)) (Dict (Eq a))
openSetC' (CSet (ConsSet_ x xs)) = Left (x, CSet xs, Dict)
openSetC' (CSet NilSet_) = Right Dict

现在有趣的部分：使用ViewPatterns，我们可以直接使用此功能轻松编写带有您想要的签名的模式。这很简单，因为我们已经设置了openSetC'与您想要的模式类型匹配的类型：

pattern ConsSetC :: () => Eq a => a -> CSet a -> CSet a
pattern ConsSetC x xs <- (openSetC' -> Left (x, xs, Dict))

   -- included for completeness, but the expression form of the pattern synonym is not at issue here
   where
     ConsSetC x (CSet xs) | not (elemS x xs) = CSet (ConsSet_ x xs)
                          | otherwise        = CSet xs

至于您的其他问题，我强烈建议将它们分成不同的帖子，以便它们都有针对性的答案。

于 2021-06-18T16:41:49.467 回答