F#中的教堂数字

Question

我一直在尝试在 F# 中实现教堂数字。他们在大学的一门课程中被简要介绍过，从那以后我可能已经陷入了困境。我有工作的前任、继任者、添加和操作，但我不能让减法工作。我正在尝试执行多次应用前任的减法 b。我发现奇怪的是，我的代码中的倒数第二行有效，但我认为等效的最后一行无效。类型不匹配。

我对 F# 非常陌生，因此我们将不胜感激。谢谢。

//Operations on tuples
let fst (a,b) = a
let snd (a,b) = b
let pair a b = (a,b)

//Some church numerals
let c0 (f:('a -> 'a)) = id
let c1 (f:('a -> 'a)) = f 
let c2 f = f << f
let c3 f = f << f << f
let c4 f = f << f << f << f

// Successor and predecessor
let cSucc (b,(cn:('a->'a)->('a->'a))) = if b then (b, fun f -> f << (cn f)) else (true, fun f -> (cn f))
let cPred (cn:('a->'a)->('a->'a)) = fun f -> snd (cn cSucc (false, c0)) f
//let cSucc2 cn = fun f -> f << (cn f)

// Add, Multiply and Subtract church numerals
let cAdd cn cm = fun f -> cn f << cm f
let cMult cn cm = cn >> cm
let cSub cn cm = cm cPred cn

//Basic function for checking validity of numeral operations
let f = (fun x -> x + 1)

//This works
(cPred << cPred) c3 f 0

//This doesn't
c2 cPred c3 f 0

这是给出的类型不匹配错误（Intellisense 说这是代码最后一行的 cPred 错误）。我可以看到输出类型被推断错误。有没有办法修复它，或者我编写这个实现的方式有什么根本错误？

'((bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> (bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)'    
but given a
    '((bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> ('a -> 'a) -> 'a -> 'a'    
The types ''a' and 'bool * (('a -> 'a) -> 'a -> 'a)' cannot be unified.

Answer 1

在下面的解释中，我将假设type CN<'a> = ('a -> 'a) -> 'a -> 'a 的定义（其中“CN”代表“教会数字”）以缩短解释并减少混乱。

您尝试将c2 应用于cPred 失败，因为c2 需要'a -> 'a 类型的参数，但cPred 不是这样的函数。

您可能期望cPred 与预期类型匹配，因为您已将其声明为CN<'a> -> CN<'a>，但这不是真正的类型。因为您将参数cn 应用于bool*CN<'a> -> bool*CN<'a> 类型（这是cSucc 的类型），所以编译器推断cn 的类型必须为CN<bool*CN<'a>>，因此cPred 的类型为@987654337 @，与 c2 所期望的不匹配。

所有这一切都归结为一个事实：当您将函数作为值传递时，它们会失去它们的通用性。

考虑一个更简单的例子：

let f (g: 'a -> 'a list) = g 1, g "a"

这样的定义不会编译，因为'a是f的参数，而不是g的参数。因此，对于f的给定执行，必须选择特定的'a，并且不能同时是int和string，因此，g不能同时应用于@987654348 @ 和"a"。

同样，cPred 中的cn 被固定为bool*CN<'a> -> bool*CN<'a> 类型，从而使cPred 的类型本身与CN<_> 不兼容。

在简单的情况下，有一个明显的解决方法：传递g 两次。

let f g1 g2 = g1 1, g2 "a"
let g x = [x]
f g g
// > it : int list * string list = [1], ["a"]

这样，g 两次都将失去通用性，但它将专门用于不同的类型 - 第一个实例为 int -> int list，第二个实例为 string -> string list。

但是，这只是一半的措施，仅适用于最简单的情况。一般的解决方案将要求编译器了解我们希望'a 是g 的参数，而不是f 的参数（这通常称为"higher-rank type"）。在 Haskell（更具体地说，GHC）中，有一个 straightforward way to do this，启用了 RankNTypes 扩展：

f (g :: forall a. a -> [a]) = (g 1, g "a")
g x = [x]
f g
==> ([1], ["a"])

在这里，我通过在类型声明中包含forall a 来明确告诉编译器参数g 有自己的泛型参数a。

F# 对此没有明确的支持，但它确实提供了可用于实现相同结果的不同功能 - 接口。接口可能具有泛型方法，并且这些方法在传递接口实例时不会失去泛型。所以我们可以像这样重新编写上面的简单示例：

type G = 
    abstract apply : 'a -> 'a list

let f (g: G) = g.apply 1, g.apply "a"
let g = { new G with override this.apply x = [x] }
f g
// it : int list * string list = ([1], ["a"])

是的，声明这种“高级函数”的语法很繁琐，但这就是 F# 必须提供的全部内容。

因此，将此应用于您的原始问题，我们需要将CN 声明为接口：

type CN = 
    abstract ap : ('a -> 'a) -> 'a -> 'a

然后我们可以构造一些数字：

let c0 = { new CN with override __.ap f x = x }
let c1 = { new CN with override __.ap f x = f x }
let c2 = { new CN with override __.ap f x = f (f x) }
let c3 = { new CN with override __.ap f x = f (f (f x)) }
let c4 = { new CN with override __.ap f x = f (f (f (f x))) }

然后cSucc 和cPred：

let cSucc (b,(cn:CN)) = 
    if b 
    then (b, { new CN with override __.ap f x = f (cn.ap f x) }) 
    else (true, cn)

let cPred (cn:CN) = snd (cn.ap cSucc (false, c0))

请注意，cPred 现在已推断出 CN -> CN 的类型，这正是我们所需要的。
算术函数：

let cAdd (cn: CN) (cm: CN) = { new CN with override __.ap f x = cn.ap f (cm.ap f x) }
let cMult (cn: CN) (cm: CN) = { new CN with override __.ap f x = cn.ap cm.ap f x }
let cSub (cn: CN) (cm: CN) = cm.ap cPred cn

注意，所有这些都得到了CN -> CN -> CN 的推断类型，正如预期的那样。

最后，你的例子：

let f = (fun x -> x + 1)

//This works
((cPred << cPred) c3).ap f 0

//This also works now
(c2.ap cPred c3).ap f 0