构造函数约束的设计选项：GADT compare PatternSynonym Required

编程问答 2022-04-23

问题描述

（这是 this answer 的后续，试图使 q 更精确。）

用例 构建/访问 Set 数据类型的构造函数。作为一个集合，不变量是“没有重复的”。为了实现这一点，我需要对元素类型设置 Eq 约束。 （更现实的是，该集合可能会实现为 BST 或哈希索引，这需要更严格的约束；在此处使用 Eq 以保持简单。）

  • 我想禁止构建即使是类型不可接受的空集合。
  • “现在认为对不需要约束的操作（数据类型构造或销毁）要求约束是不好的做法。相反，约束应该移动到更靠近“使用站点”的地方。”，引用这一点回答。
  • 好的，因此无需将约束“内置”到数据结构中。访问/解构操作（如showing 或计数元素）不一定需要 Eq。

然后考虑两种（或者说五种）可能的设计：

（我知道一些约束可以通过 deriving 来实现，尤其是 Foldable 来获得 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

  • 因此推断出类型 (\(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 是提供的约束，但需要为空。

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

  • 但是有一个错误：要约束一个元素，我需要在尾部的 NoCSet 中解开 CSet 然后重新包装一个 {{ 1}}。尝试仅使用 CSet 模式来做到这一点是错误的。相反：

    ConsSetC

  • 就“智能构造函数”而言，这很愚蠢。我做错了什么？

  • 推断出 insertCSet x (CSet xs) = ConsSetC x xs -- ConsSetC on rhs,to check for duplicates ，因此约束再次没有逃脱。

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

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

    insertCSet :: a -> CSet a -> CSet a

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

  • 推断 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 不同，即使它们在道德上是等效的。它确实拒绝尝试构建具有重复项的集合。

  • 推断出 ConsSetC2，因此存在的限制不会超出“使用网站”的范围。

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

(\(ConsSetC3 x xs) -> x) :: CSet p -> p

GHC 推断无可见约束 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 ; elemG :: a -> GADTSet a -> Bool。

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

(\(GADTConsSet x xs) -> x) :: GADTSet p -> p
  • GHC 不会抱怨缺少签名，而是推断 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 是提供的约束，但为空必需。
  • 推断 pattern ConsSetG :: () => Eq a => a -> GADTSet a -> GADTSet a，因此约束不会从“使用站点”中逃脱。

选项 2b。定义一个插入函数

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

问题

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

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

解决方法

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

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

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

{-# 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 的限制，而不是表明添加不必要的约束a la DatatypeContexts 实际上是好的编程习惯。看来至少还有其他一些人同意 this 是一项bug 而非一项功能。

对于您的前四个问题：

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

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

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

一种方法是用这个签名写一个方法：

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

说的是：

  • a 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 与 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

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

gadthaskellhaskellpattern-synonyms