F# 中的教会数字

Question

我一直在尝试在 F# 中实现教堂数字。他们在大学的一门课程中被简要介绍过，从那以后我可能有点陷入困境。我有工作的 Predecessor、Successor、Add 和 Operations，但我无法工作。我正在尝试多次实施减法 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"代表"Church Numeral"）以缩短解释并减少混乱。

您尝试将 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 得到 CN<bool*CN<'a>> -> CN<'a> 的类型，这与 c2 期望的不匹配。

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

考虑一个更简单的例子：

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

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

类似地，cPred 中的 cn 固定为 bool*CN<'a> -> bool*CN<'a> 类型，从而使 cPred 本身的类型与 CN<_>.[=68 不兼容=]

在简单的情况下，有一个明显的解决方法：传递 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"). In Haskell (more specifically, GHC), there is a 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"])

是的，声明这样的语法 "higher-rank functions" 很繁琐，但这就是 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

F# 中的教会数字

Church Numerals in F#

f#

functional-programming

type-inference

lambda-calculus

church-encoding