Haskell递归数据类型的"默认行为"

Question

我正在尝试在Haskell中编写命题逻辑解算器.我用一种名为'Sentence'的递归数据类型表示逻辑表达式,它有几种不同操作的子类型 - 'AndSentence','OrSentence'等等.所以我猜这是一棵树,有几种类型的节点,每个都有0,1,或2个孩子.

它似乎工作,但一些代码是重复的,我认为应该有更好的方式来表达它.基本上我有几个函数,其中'默认行为'是让函数以递归方式对节点的子节点进行操作,从而触底于某些节点类型(通常是'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

这看起来像递归方案的一个很好的例子.

首先,我们将您的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办？非常粗略地,当应用于像in cata f这样的函数时,它构建了一个catamorphism,即一个函数

1. 将公式分为其子组件
2. 递归地应用于cata f找到的子组件
3. 将转换后的组件重新组合成公式
4. 通过最后一个公式(加工后的子公式),f以便最顶层的结缔组织受到影响

最后一步是做实际工作的那一步.在\case上述执行只是想要的转型.其他所有内容都由cata(以及Functor自动生成的实例)处理.

以上所述,我不建议任何人轻易搬到 recursion-schemes.使用cata可以导致非常优雅的代码,但它需要人们理解所涉及的机器,这可能无法立即掌握(它肯定不适合我).