如何实现对 `UnionM [UnionM SymInteger]` 进行操作的函数？

Question

这是关于 Grisette 图书馆。

首先让我解释一下我对为什么我们需要这个怪物的理解。本质上，我想处理

SymInteger

列表。但是，AFAIU，只要操作的结果不是一个简单的值（如

SymInteger

或

UnionM

）并且它是例如一个条件（例如，结果），您就需要将

2

包装到

"a"

中

mrgIf

）。

现在，假设我们要创建一个函数，它接受两个

[SymInteger]

并返回一个

[SymInteger]

，该函数具有两个列表的元素最大值。我们不能做以下事情：

pickLargest :: [SymInteger] -> [SymInteger] -> [SymInteger]
-- skip simple cases
pickLargest (x:xs) (y:ys) = (mrgIf (x .> y) x y) : (sumSym xs ys)

因为

mrgIf

返回

UnionM SymInteger

而不是

SymInteger

。因此，我们需要

[UnionM SymInteger]

才能使我们的函数具有通用性，如下所示：

pickLargest :: [UnionM SymInteger] -> [UnionM SymInteger] -> [UnionM SymInteger]
-- ...
pickLargest (x:xs) (y:ys) = (mrgIf (x .> y) x y) : (pickLargest xs ys)

现在，假设我还想创建一个函数，从列表中删除一个元素（如果存在）。我无法使用 symDrop，因为它需要

SymInteger

而不是

UnionM SymInteger

。因此，以下内容将不起作用：

myVar :: [UnionM SymInteger]
myVar = pickLargest ["a", "b"] ["c", "d"]

dropOnSym = print (symDrop (head myVar) myVar)

因为

head myVar

具有类型

UnionM SymInteger

（和 AFAIU，它也不起作用 如果我想根据

symDrop

的结果调用

symDrop

）。最后，因为我们不知道结果列表的长度，所以需要将其包装在

UnionM

中。

因此，我发现实现 symListDrop 的唯一方法是：

symListDrop :: UnionM [UnionM SymInteger] -> UnionM SymInteger -> UnionM [UnionM SymInteger]
symListDrop m_ls m_el = do
  ls <- m_ls
  case ls of
    [] -> mrgReturn []
    (x:_) -> mrgIf (x .== m_el) 
                (symListDrop m_ls m_el)
                (mrgBind (symListDrop m_ls m_el) (\ys -> mrgReturn (x : ys)))

我担心只是我真的很努力......特别是，我必须打开

UnionM

的包装这一事实似乎很可疑。另外，在这样的简单调用中：

dropOnConc :: IO ()
dropOnConc = print (symListDrop (mrgReturn [1, 2, 3]) 2)

似乎陷入了无限递归。

那么，您对如何实现此功能有什么建议，或者对这些问题进行建模的不同方式吗？

Answer 1

感谢您对 Grisette 库的兴趣，我是它的作者。我刚刚设置了 GitHub 讨论，因此可以在那里进行进一步的讨论。

TL；博士

如果您还没有查看过，最近已经为 Grisette 构建了一个小型教程。

大多数情况下您不必使用

UnionM SymInteger

，并且您的

pickLargest

可以使用

mrgIte

来实现。

pickLargest :: [SymInteger] -> [SymInteger] -> [SymInteger]
-- skip simple cases
pickLargest (x:xs) (y:ys) = (mrgIte (x .> y) x y) : (sumSym xs ys)

symDrop

不是您需要的。您可能想升级到最新的 Grisette 并使用

mrgDelete

。

symMax

那里也有卖。

使用

symMax

，存在更简单的解决方案：

pickLargest :: [SymInteger] -> [SymInteger] -> [SymInteger]
pickLargest = zipWith symMax

你的

symListDrop

使用相同的操作数调用自身，这就是它无限递归的原因。

在讨论

SymInteger

之前

我有第一个问题要问你，

symDrop

是你想要的功能吗？它的语义就像

drop

中的

base

，其中第二个

SymInteger

是从列表头部删除的元素数量，而不是要删除的元素。

我建议您升级到最新的 Grisette 软件包（从今天起v0.5.0.1），该软件包可在 Hackage 或 Stackage nightly snapshots 上找到。

Data.List

中的几乎所有函数都有符号版本，而

mrgDelete

函数可能就是您想要的。请预计版本之间会出现一些不兼容性，因为某些函数使用更一致的命名方案重命名，例如，

symDrop

已重命名为

mrgDrop

，因为它返回一个联合。文档中还提供了操作员的（估计）复杂性。

SimpleMergeable

和

mrgIte

引入了

UnionM

容器来处理复杂数据结构的多路径执行。这些数据结构本身不具备处理路径条件的能力，因此我们将它们存储在

UnionM

容器中的多个分支中。

但是，某些数据结构，例如符号基元类型（

SymBool

、

SymInteger

等）、符号基元类型元组（

(SymBool, SymInteger)

）能够自行保存路径条件。这些数据结构实现了

SimpleMergeable

类型类，该类提供了

mrgIte

功能。

mrgIte :: (SimpleMergeable a) => SymBool -> a -> a -> a

乍一看可能会令人困惑，因为我们有两个不同的“分割路径”版本，但这实际上是故意的，并且

mrgIf

和

mrgIte

具有不同的语义。

mrgIf

类似于控制流结构，例如 C 中的

if

语句，而

mrgIte

是用于构建表达式的三元运算符，例如 C 中的

?:

。

如果您确实需要与

UnionM SymInteger

...

合作

有时，使用简单可合并类型的

UnionM

是不可避免的，例如，当您有一个内部使用

UnionM

的通用数据结构时。 Grisette 提供了与它们一起工作的助手（例如

(.#)

和

onUnion

），类型签名如下：

onUnion :: (SimpleMergeable r, Mergeable a) => (a -> r) -> UnionM a -> r

对于无限递归

您的函数正在调用自身 (

symListDrop m_ls m_el

)，并在最后一行中使用完全相同的操作数。

您原来问题的实现

现在，假设我们要创建一个函数，它接受两个

[SymInteger]

并返回一个

[SymInteger]

，该函数具有两个列表的按元素最大值。

这可以使用

zipWith

和

symMax

以及最新的 Grisette 来实现：

pickLargest :: [SymInteger] -> [SymInteger] -> [SymInteger]
pickLargest = zipWith symMax