haskell - 如何针对实例为递归数据类型的类型类进行模式匹配？

Question

此问题是 How to pattern match against a typeclass value? 的后续问题.

我正在启动一个关于一阶逻辑的宠物项目，并决定使用 Haskell 来实现此目的。我的第一个障碍是定义“一阶逻辑公式”，因此数据类型:

data Formula v  = Belong v v                      -- x in y
                | Bot                             -- False
                | Imply (Formula v) (Formula v)   -- p -> q
                | Forall v (Formula v)            -- forall x, p

但是，我不愿意根据实现细节编写代码，而宁愿抽象出细节，以防我改变主意，或者如果我想通过替代实现重用功能，因此类型类:

class FirstOrder m where
  belong    :: v -> v -> m v
  bot       :: m v
  imply     :: m v -> m v -> m v
  forall    :: v -> m v -> m v
  asFormula :: m v -> Formula v

我添加了最后一个函数 asFormula 以便使用 ViewPatterns (如上面链接中的建议)，以便能够对以下值进行模式匹配这个类型类。

现在假设我想定义一个简单的函数:

subst :: (FirstOrder m) => (v -> w) -> m v -> m w

根据给定映射f::v -> w 替换公式中的变量(感觉像fmap)，因此公式属于 x y 映射到 belong (f x) (f y) 等，然后使用 ViewPatterns:

subst f (asFormula -> Belong x y) = belong (f x) (f y)

到目前为止一切顺利...

但是，当尝试编写 subst f p->q = (subst f p) -> (subst f q) 时:

subst f (asFormula -> Imply p q)  = imply (subst f p) (subst f q)

我收到一个类型错误，仔细想想这是完全有道理的:模式匹配将 p 和 q 绑定(bind)到 Formula v< 类型的元素 而不是所需的类型 m v。

现在我可以看到问题了，甚至可以想出通过向类型类添加 fromFormula 函数以转换回类型 m v 来解决它的方法，但是我认为从性能的角度来看这是疯狂的(就像 asFormula 请注意一样疯狂)，为了保持代码通用性要付出巨大的代价。

所以我现在在这里，尝试通过自由代数(递归数据类型)上的结构递归来定义一个简单的函数，但我希望抽象出实现细节(并从类型类而不是数据类型中编写代码)我似乎处于一个不可能的境地。

有没有出路，或者我应该忘记抽象并使用递归数据类型？

Answer 1

这看起来过于笼统，但我们还是忽略它吧。

您可以使用显式 F-(co-) 代数和不动点来解决这个问题。

data FormulaF v k
   = Belong v v                      -- x in y
   | Bot                             -- False
   | Imply (k v) (k v)               -- p -> q
   | Forall v (k v)                  -- forall x, p

newtype Formula v = Formula (FormulaF v Formula)      
   -- fixed point. You might not need it, but it's nice to have.
   -- 

那么，你可以这样做

class FirstOrder m where
  belong    :: v -> v -> m v
  bot       :: m v
  imply     :: m v -> m v -> m v
  forall    :: v -> m v -> m v
  asFormula :: m v -> FormulaF v m

和

subst :: (FirstOrder m) => (v -> w) -> m v -> m w
subst f (asFormula -> Belong x y) = belong (f x) (f y)
subst f (asFormula -> Imply p q)  = imply (subst f p) (subst f q)

现在应该可以工作了，因为 asFormula 不会将整个 m v 递归地转换为完整的公式，而是转换为 FormulaF v m ，其中表面上看起来像一个公式(您模式匹配的第一个构造函数，如 Imply)，但内部仍然看起来像一个 m v。

如果你真的想追求这种过于笼统的方法，也许你应该看看recursion-schemes、F-代数和F-coalgebras，以及它们相关的cata-/ana-/hylo-/para-/无论态射。

最后，我建议避免尝试在 FP 中采用 OOP 设计模式。有时你可以用这种方式硬塞一些东西，但这通常是不惯用的。例如，在 Haskell 中，我们非常习惯具有固定数量的构造函数的类型(但是对它们进行操作的一组开放函数)，就像 OOP 接口(interface)中具有固定数量的方法(但是一组开放的子类)一样。人们可以尝试概括这一点，但它很复杂，并且应该仅在需要时才进行。