haskell - 在 Haskell 中，我如何获取一个 m 元谓词和一个 n 元谓词并构造一个 (m+n) 元谓词？

Question

今天，我尝试使用类型类来归纳构造任意数量的谓词的函数，将任意类型的任意组合作为输入，返回相同类型但应用了一些基本操作的其他谓词。例如

conjunction (>2) even

将返回一个谓词，该谓词对于大于 2 的偶数计算为真，并且

conjunction (>=) (<=)

会返回=

一切都很好，让那部分工作，但它提出了一个问题，如果我想将两个谓词的连接定义为一个谓词，每个连接谓词的每个输入都需要一个输入，该怎么办？例如:

:t conjunction (>) not

将返回 Ord a => a -> a -> Bool -> Bool。这可以做到吗？如果是这样，怎么做？

Answer 1

我们需要TypeFamilies对于这个解决方案。

{-# LANGUAGE TypeFamilies #-}

这个想法是定义一个类 Pred对于 n 元谓词:

class Pred a where
  type Arg a k :: *
  split :: a -> (Bool -> r) -> Arg a r

问题在于重新调整谓词的参数，所以这就是该类的目标。关联类型 Arg应该通过替换最终 Bool 来访问 n 元谓词的参数与 k , 所以如果我们有一个类型

X = arg1 -> arg2 -> ... -> argn -> Bool

然后

Arg X k = arg1 -> arg2 -> ... -> argn -> k

这将允许我们构建 conjunction 的正确结果类型。要收集两个谓词的所有参数。

函数 split采用 a 类型的谓词和 Bool -> r 类型的延续并会产生 Arg a r 类型的东西. split 的想法如果我们知道如何处理 Bool我们最终从谓词中获得，然后我们可以在两者之间做其他事情( r)。

毫不奇怪，我们需要两个实例，一个用于 Bool一个用于目标已经是谓词的函数:

instance Pred Bool where
  type Arg Bool k = k
  split b k = k b

一个 Bool没有参数，所以 Arg Bool k只需返回 k .此外，对于 split ，我们有 Bool已经，所以我们可以立即应用延续。

instance Pred r => Pred (a -> r) where
  type Arg (a -> r) k = a -> Arg r k
  split f k x = split (f x) k

如果我们有一个 a -> r 类型的谓词，然后 Arg (a -> r) k必须以 a -> 开头，我们继续调用 Arg在 r 上递归.对于 split ，我们现在可以采用三个参数， x属于 a 类型.我们可以喂 x至 f然后调用 split结果上。

一旦我们定义了 Pred类，很容易定义 conjunction :

conjunction :: (Pred a, Pred b) => a -> b -> Arg a (Arg b Bool)
conjunction x y = split x (\ xb -> split y (\ yb -> xb && yb))

该函数接受两个谓词并返回 Arg a (Arg b Bool) 类型的内容。 .让我们看一下这个例子:

> :t conjunction (>) not
conjunction (>) not
  :: Ord a => Arg (a -> a -> Bool) (Arg (Bool -> Bool) Bool)

GHCi 没有扩展这种类型，但我们可以。类型等价于

Ord a => a -> a -> Bool -> Bool

这正是我们想要的。我们也可以测试一些例子:

> conjunction (>) not 4 2 False
True
> conjunction (>) not 4 2 True
False
> conjunction (>) not 2 2 False
False

请注意，使用 Pred类，编写其他函数(如 disjunction )也很简单。