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

Question

今天我玩了使用类型类来归纳地构造任何arity谓词的函数,将任何类型的任意组合作为输入,返回相同类型的其他谓词但应用了一些基本操作.例如

conjunction (>2) even

会返回一个谓词,对于大于2的偶数,它的计算结果为真

conjunction (>=) (<=)

会返回=

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

:t conjunction (>) not

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

Answer 1

我们需要TypeFamilies这个解决方案.

{-# LANGUAGE TypeFamilies #-}

我们的想法是Pred为n-ary谓词定义一个类:

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

问题在于重新调整谓词的参数,所以这就是本课程的目标.相关类型Arg应该通过更换最终授予访问权限n元谓词的参数Bool有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

A 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)也很简单.