引数を自分自身に適用する関数？

Question

は、次のSML機能を考えてみましょう：

fn x => x x 

これは、次のエラー（ニュージャージー州のv110.72の標準ML）生成します。これは許可されていない理由

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

を私は一種の見ることができます - - 1つは、どのようなタイプのものを書き留めるかは分かりませんが、完全に無意味ではありません。たとえば、アイデンティティ関数を渡して戻すことができます。

この機能の名前はありますか？ （SMLで表現する方法はありますか？）

Answer 1

このような機能をML型のシステムで表現する方法はありません。第1のxと第2のx xの第2のものは、ある種類の_aに対してそれぞれ(_a -> _a) -> (_a -> _a)と_a -> _aという種類のその関数の異なるインスタンスでなければならないため、ID関数を使用しても機能しません。実際に

は、型システムは、型なしラムダ計算に

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

のような構造を禁止するように設計されています。

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

と、このような

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

Answer 2

機能は、多くの場合、固定小数点コンビネータに遭遇している期待される結果を得る：動的型付け言語のスキームでは、この関数を書くことができます。例えばY combinatorの1つの書式がλf.(λx.f (x x)) (λx.f (x x))と書かれています。固定小数点コンビネータは、追加の再帰的な構造を持たないタイプ化されていないラムダ計算で一般的な再帰を実装するために使用され、これはタイプ変換されていないラムダ計算チューリング完了の一部です。

人々がラムダ計算の上にナイーブな静的型システムであるsimply-typed lambda calculusを開発したとき、彼らはもはやそのような関数を書くことができないことを発見しました。実際、単純型のラムダ計算では一般的な再帰を実行することはできません。したがって、単純型のラムダ計算はもはやチューリング完全ではない。 （一つの興味深い副作用は、単純に、型付きラムダ計算中のプログラムが常に終了するということです。）

、このような名前の再帰関数として内蔵された再帰的なメカニズムの問題を克服するために、標準的なMLの必要性、などの

実静的に型付けされたプログラミング言語（ val recまたはfun）で定義され、再帰的なデータ型と呼ばれます。

再帰的データ型を使用して、必要なものをシミュレートすることは可能ですが、それほど美しくはありません。

基本的には、'a foo = 'a foo -> 'aのようなタイプを定義します。ただし、これは許可されていません。代わりに、データ型でラップ：

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

datatype 'a foo = Wrap of ('a foo -> 'a);は基本的には、Wrapとunwrapは'a fooと'a foo -> 'aの間で変換するために使用され、その逆も同様です。

x xの代わりに関数を呼び出す必要があるときはいつも、(unwrap x) x（またはunwrap x x）を明示的に記述する必要があります。すなわちunwrapは、それを元の値に適用できる関数に変換します。

P.S.別のML言語OCamlには、再帰型（通常は無効）を有効にするオプションがあります。 -rectypesフラグを持つインタプリタまたはコンパイラを実行すると、fun x -> x xのようなものを書くことができます。基本的には、バックグラウンドでは、タイプチェッカーは、再帰型を「ラップ」および「アンラップ」してから挿入する必要がある場所を特定します。私は、同様の再帰型の機能を持つ標準的なML実装は認識していません。