将其参数应用于自身的函数？

发布于 2025-01-03 02:30:30 字数 340 浏览 4 评论 0原文

考虑以下 SML 函数：

fn x => x x

这会产生以下错误（新泽西州标准 ML v110.72）：

stdIn:1.9-1.12 Error: operator is not a function [circularity]
  operator: 'Z
  in expression:
    x x

我可以理解为什么不允许这样做 - 首先，我不太确定如何写下它的内容类型将是——但这并不是完全无意义的；例如，我可以将身份函数传递给它并取回它。

这个函数有名字吗？（有没有办法用SML来表达？）

原文

Consider the following SML function:

fn x => x x

This produces the following error (Standard ML of New Jersey v110.72):

stdIn:1.9-1.12 Error: operator is not a function [circularity]
  operator: 'Z
  in expression:
    x x

I can sort of see why this isn't allowed -- for one, I'm not really sure how to write down what its type would be -- but it's not completely nonsensical; for instance, I could pass the identity function to it and get it back.

Is there a name for this function? (Is there a way to express it in SML?)

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

梦情居士 2025-01-10 02:30:30

无法用具有类似 ML 类型系统的语言来表达此功能。即使使用恒等函数，它也不起作用，因为 x 中的第一个 x 和第二个 x x 必须是该函数的不同实例，类型为 ( _a->_a)->; (_a -> _a) 和 _a -> _a，分别针对某些类型_a。

事实上，类型系统被设计为禁止像

(λx . x x) (λx . x x)

无类型 lambda 演算那样的构造。在动态类型语言Scheme中，可以编写这样的函数：

(define (apply-to-self x) (x x))

并得到预期的结果

> (define (id x) x)
> (eq? (apply-to-self id) id)
#t

There is no way to express this function in a language with an ML-like type system. Even with the identity function it wouldn't work, because the first x and the second in x x would have to be different instances of that function, of type (_a -> _a) -> (_a -> _a) and _a -> _a, respectively, for some type _a.

In fact, type systems are designed to forbid constructs like

(λx . x x) (λx . x x)

in the untyped lambda calculus. In the dynamically typed language Scheme, you can write this function:

(define (apply-to-self x) (x x))

and get the expected result

> (define (id x) x)
> (eq? (apply-to-self id) id)
#t

回复收藏 0 原文

嗳卜坏 2025-01-10 02:30:30

像这样的函数经常在定点组合器中遇到。例如，Y 组合器的一种形式写作λf.(λx. f (xx)) (λx.f (xx))。定点组合器用于在无类型 lambda 演算中实现一般递归，而无需任何额外的递归构造，这也是使无类型 lambda 演算图灵完备的一部分。

当人们开发简单类型 lambda 演算时，这是一个基于 lambda 演算的朴素静态类型系统，他们发现不再可能编写这样的函数。事实上，在简单类型的 lambda 演算中不可能执行一般的递归；因此，简单类型的 lambda 演算不再是图灵完备的。（一个有趣的副作用是，简单类型 lambda 演算中的程序总是终止。）

真正的静态类型编程语言（如标准 ML）需要内置递归机制来克服该问题，例如命名递归函数（用 val rec 或 fun 定义）和命名递归数据类型。

仍然可以使用递归数据类型来模拟您想要的东西，但它并不那么漂亮。

基本上，您想要定义一个类似 'a foo = 'a foo ->; 的类型。 'a;然而，这是不允许的。相反，您可以将其包装在数据类型中： datatype 'a foo = Wrap of ('a foo -> 'a);

datatype 'a foo = Wrap of ('a foo -> 'a);
fun unwrap (Wrap x) = x;

基本上，Wrap 和 unwrap code> 用于在 'a foo 和 'a foo ->; 之间进行转换。 'a，反之亦然。

每当您需要调用函数本身时，您必须显式编写 (unwrap x) x （或 unwrap x x），而不是 x x ;即 unwrap 将其转换为一个函数，然后您可以将其应用于原始值。

PS 另一种 ML 语言 OCaml 有一个启用递归类型的选项（通常禁用）；如果您使用 -rectypes 标志运行解释器或编译器，则可以编写类似 fun x ->; 的内容。 x x 。基本上，在幕后，类型检查器会找出需要“包装”和“展开”递归类型的位置，然后为您插入它们。我不知道有任何标准 ML 实现具有类似的递归类型功能。

Functions like this are often encountered in fixed-point combinators. e.g. one form of the Y combinator is written λf.(λx.f (x x)) (λx.f (x x)). Fixed-point combinators are used to implement general recursion in untyped lambda calculus without any additional recursive constructs, and this is part of what makes untyped lambda calculus Turing-complete.

When people developed simply-typed lambda calculus, which is a naive static type system on top of lambda calculus, they discovered that it was no longer possible to write such functions. In fact, it is not possible to perform general recursion in simply-typed lambda calculus; and thus, simply-typed lambda calculus is no longer Turing-complete. (One interesting side effect is that programs in simply-typed lambda calculus always terminate.)

Real statically-typed programming languages like Standard ML need built-in recursive mechanisms to overcome the problem, such as named recursive functions (defined with val rec or fun) and named recursive datatypes.

It is still possible to use recursive datatypes to simulate something like what you want, but it is not as pretty.

Basically, you want to define a type like 'a foo = 'a foo -> 'a; however, this is not allowed. You instead wrap it in a datatype: datatype 'a foo = Wrap of ('a foo -> 'a);

datatype 'a foo = Wrap of ('a foo -> 'a);
fun unwrap (Wrap x) = x;

Basically, Wrap and unwrap are used to transform between 'a foo and 'a foo -> 'a, and vice versa.

Whenever you need to call a function on itself, instead of x x, you have to explicitly write (unwrap x) x (or unwrap x x); i.e. unwrap turns it into a function that you can then apply to the original value.

P.S. Another ML language, OCaml, has an option to enable recursive types (normally disabled); if you run the interpreter or compiler with the -rectypes flag, then it is possible to write things like fun x -> x x. Basically, behind the scenes, the type-checker figures out the places where you need to "wrap" and "unwrap" the recursive type, and then inserts them for you. I am not aware of any Standard ML implementation that has similar recursive types functionality.

回复收藏 0 原文

~没有更多了~