haskell - Haskell 递归数据类型的“默认行为”

Question

我正在尝试用 Haskell 编写一个命题逻辑求解器。我使用名为“Sentence”的递归数据类型表示逻辑表达式，该数据类型具有用于不同操作的多个子类型 -“AndSentence”、“OrSentence”等。所以我猜它是一棵具有多种类型节点的树，每个节点都有 0、1、或 2 个 child 。

它似乎有效，但有些代码有点重复，我认为应该有更好的方式来表达它。基本上，我有几个函数，其中“默认行为”是让函数递归地作用于节点的子节点，在某些节​​点类型(通常是“AtomicSentences”，即叶子)上触底。所以我写了一个像这样的函数:

imply_remove :: Sentence Symbol -> Sentence Symbol
imply_remove (ImplySentence s1 s2) = OrSentence (NotSentence (imply_remove s1)) (imply_remove s2)
imply_remove (AndSentence s1 s2) = AndSentence (imply_remove s1) (imply_remove s2)
imply_remove (OrSentence s1 s2) = OrSentence (imply_remove s1) (imply_remove s2)
imply_remove (NotSentence s1) = NotSentence (imply_remove s1)
imply_remove (AtomicSentence s1) = AtomicSentence s1

我想要一种更简洁的方式来编写“AndSentence”、“OrSentence”和“NotSentence”的行。

仿函数似乎与我想要的类似，但没有成功...我想对子树进行操作，而不是对子树的每个节点中包含的某些值进行操作。

有正确的方法吗？或者更自然的方式来构建我的数据？

Answer 1

这看起来是 recursion-schemes 的一个很好的案例.

首先，我们将您的 Sentence sym 类型描述为类型级定点 一个合适的仿函数。

{-# LANGUAGE DeriveFunctor, LambdaCase #-}

import Data.Functor.Foldable  -- from the recursion-schemes package

-- The functor describing the recursive data type
data SentenceF sym r
   = AtomicSentence sym
   | ImplySentence r r
   | AndSentence r r
   | OrSentence r r
   | NotSentence r
   deriving (Functor, Show)

-- The original type recovered via a fixed point
type Sentence sym = Fix (SentenceF sym)

上面的 Sentence sym 类型与您的原始类型几乎相同，只是所有内容都必须包装在 Fix 内。 调整原始代码以使用这种类型是完全机械的: 我们以前使用 (Constructor ...)，现在使用 Fix (Constructor ...)。例如

type Symbol = String

-- A simple formula: not (p -> (p || q))
testSentence :: Sentence Symbol
testSentence = 
   Fix $ NotSentence $
      Fix $ ImplySentence
         (Fix $ AtomicSentence "p")
         (Fix $ OrSentence
            (Fix $ AtomicSentence "p")
            (Fix $ AtomicSentence "q"))

这是您的原始代码，其中包含冗余(由于额外的 Fixes 而变得更糟)。

-- The original code, adapted
imply_remove :: Sentence Symbol -> Sentence Symbol
imply_remove (Fix (ImplySentence s1 s2)) =
  Fix $ OrSentence (Fix $ NotSentence (imply_remove s1)) (imply_remove s2)
imply_remove (Fix (AndSentence s1 s2)) =
  Fix $ AndSentence (imply_remove s1) (imply_remove s2)
imply_remove (Fix (OrSentence s1 s2)) =
  Fix $ OrSentence (imply_remove s1) (imply_remove s2)
imply_remove (Fix (NotSentence s1)) =
  Fix $ NotSentence (imply_remove s1)
imply_remove (Fix (AtomicSentence s1)) =
  Fix $ AtomicSentence s1

让我们通过评估 imply_remove testSentence 来执行测试:结果正是我们所期望的:

 -- Output: not ((not p) || (p || q))
 Fix (NotSentence
   (Fix (OrSentence
      (Fix (NotSentence (Fix (AtomicSentence "p"))))
      (Fix (OrSentence
         (Fix (AtomicSentence "p"))
         (Fix (AtomicSentence "q")))))))

现在，让我们使用从递归方案借用的核武器:

imply_remove2 :: Sentence Symbol -> Sentence Symbol
imply_remove2 = cata $ \case
   -- Rewrite ImplySentence as follows
   ImplySentence s1 s2 -> Fix $ OrSentence (Fix $ NotSentence s1) s2
   -- Keep everything else as it is (after it had been recursively processed)
   s -> Fix s

如果我们运行测试 imply_remove2 testSentence，我们会得到与原始代码相同的输出。

cata 是做什么的？非常粗略地，当应用于像这样的函数时 在cata f中，它构建了一个变形，即一个函数

1. 将公式分解为其子组件
2. 递归地将cata f应用于找到的子组件
3. 将转换后的组件重新组合成公式
4. 将最后一个公式(带有已处理的子公式)传递给 f，以便影响最上面的连接词

最后一步是进行实际工作的步骤。上面的 \case 仅执行所需的转换。其他一切都由 cata 处理(以及自动生成的 Functor 实例)。

综上所述，我不建议任何人轻易搬到 递归方案。使用 cata 可以生成非常优雅的代码，但它需要人们了解所涉及的机制，而这可能不会立即掌握(这肯定不适合我)。