3

我一直在尝试在 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.
4

1 回答 1

5

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

您尝试对c2to的应用cPred失败，因为c2需要一个 type 的参数'a -> 'a，但cPred不是这样的函数。

您可能希望cPred匹配预期的类型，因为您已将其声明为CN<'a> -> CN<'a>，但这不是真正的类型。因为您将参数cn应用于 type bool*CN<'a> -> bool*CN<'a>（它是 的类型cSucc），所以编译器推断cn必须具有 type of 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"。

类似地，cnincPred固定为 type 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（这通常被称为“更高等级的类型”）。在 Haskell（更具体地说，GHC）中，有一种简单的方法可以做到这一点，并RankNTypes启用扩展：

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

在这里，我通过在类型声明中包含参数来明确告诉编译器该参数g具有自己的泛型参数。aforall 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
于 2018-01-17T03:36:28.720 回答