如何在没有"let rec"的情况下定义y-combinator？

Question

在几乎所有的例子中,ML类型语言中的y-combinator都是这样编写的:

let rec y f x = f (y f) x
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1))

这可以按预期工作,但使用时定义y组合器感觉就像是作弊let rec ....

我想使用标准定义在不使用递归的情况下定义此组合器:

Y = ?f·(?x·f (x x)) (?x·f (x x))

直接翻译如下:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;

然而,F#抱怨它无法弄清楚类型:

  let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;
  --------------------------------^

C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a
    'a    
but given a
    'a -> 'b    
The resulting type would be infinite when unifying ''a' and ''a -> 'b'

如何在不使用F#的情况下编写y-combinator let rec ...？

Answer 1

由于编译器所指出的,没有任何类型的可分配给x这样的表达(x x)是良好的类型(这是不完全正确,您可以键入明确x的obj->_-见我的最后一段).您可以通过声明递归类型来解决此问题,以便非常相似的表达式可以工作:

type 'a Rec = Rec of ('a Rec -> 'a)

现在Y-combinator可以写成:

let y f =
  let f' (Rec x as rx) = f (x rx)
  f' (Rec f')

不幸的是,你会发现这不是很有用,因为F#是一种严格的语言,所以你尝试使用这个组合器定义的任何函数都会导致堆栈溢出.相反,您需要使用Y-combinator(\f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y)))的应用顺序版本:

let y f =
  let f' (Rec x as rx) = f (fun y -> x rx y)
  f' (Rec f')

另一种选择是使用显式懒惰来定义正常顺序的Y组合子:

type 'a Rec = Rec of ('a Rec -> 'a Lazy)
let y f =
  let f' (Rec x as rx) = lazy f (x rx)
  (f' (Rec f')).Value

这样做的缺点是递归函数定义现在需要一个惰性值的显式力(使用Value属性):

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1)))

但是,它具有以下优点:您可以使用惰性语言定义非函数递归值:

let ones = y (fun ones -> LazyList.consf 1 (fun () -> ones.Value))

作为最后的替代方案,您可以尝试通过使用装箱和向下转换来更好地逼近无类型的lambda演算.这会给你(再次使用Y-combinator的应用订单版本):

let y f =
  let f' (x:obj -> _) = f (fun y -> x x y)
  f' (fun x -> f' (x :?> _))

这有一个明显的缺点,它会导致不需要的装箱和拆箱,但至少这完全是内部的实现,并且永远不会导致运行时失败.

Answer 2

我会说这是不可能的,并且问为什么,我会手动并调用简单输入lambda演算具有规范化属性的事实.简而言之,简单类型的lambda演算的所有项都终止(因此Y不能在简单类型的lambda演算中定义).

F#的类型系统并不完全是简单类型lambda演算的类型系统,但它足够接近.F#没有let rec真正接近简单类型的lambda演算 - 并且,重申一下,在那种语言中你不能定义一个不终止的术语,也不包括定义Y.

换句话说,在F#中,"let rec"至少需要是一个语言原语,因为即使你能够从其他原语定义它,你也无法输入这个定义.将它作为原语允许您(除其他外)为该原语提供特殊类型.

编辑:kvb在他的回答中表明,类型定义(简单类型的lambda演算中缺少的一个特征,但存在于let-rec-less F#中)允许得到某种递归.非常聪明.