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"代表"教堂数字")的定义,以便缩短解释并减少混乱.

您尝试应用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".

类似地,cn在cPred固定到类型时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