將其參數應用於自身的函數？

考慮以下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

我有點明白爲什麼這是不允許的 - - 一方面，我不確定如何寫下它的類型 - 但它並不完全沒有意義;例如，我可以將身份函數傳遞給它並將其取回。

是否有這個功能的名稱？（有沒有辦法在SML中表達它？）

來源

2012-02-06 Ismail Badawi

如果任何人有興趣，我發現這被稱爲[U Combinator（見頁面底部）]（http://www.ucombinator.org/），但無法找到更多關於它的信息。 – 2012-02-06 16:09:08

我不知道它被稱爲U combinator，但正如該頁面所述，它用於構建我在答案中提供的無類型lambda微積分的（顯然最短的）非終止程序。 – 2012-02-06 16:18:48

沒有辦法用ML類型的系統在語言中表達這個功能。即使使用身份識別功能也無法使用，因爲第一個x和x x中的第二個必須是該功能的不同實例，分別爲(_a -> _a) -> (_a -> _a)和_a -> _a，某些類型爲_a。

事實上，類型系統都設計在了無類型演算禁止構建體像

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

。在動態類型語言計劃，你可以寫這個函數：

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

，並得到預期的結果

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

來源

2012-02-06 15:35:44

「，因爲x x中的第一個x和第二個必須是該函數的**不同實例**：出於好奇，那麼懶惰評估的語言怎麼樣？除此之外，我不確定SML中是否有類似「實例」的內容（除非有副作用）。這個問題只是一個打字問題（沒有類型，通常沒有意義，但並不總是）。 – Hibou57 2014-09-17 00:49:36

@ Hibou57舉例來說，我的意思是泛型函數的一個不同的具體類型實例。 – 2014-09-20 10:44:24

這樣的功能往往在固定點組合遇到。例如Y combinator的一種形式被寫爲λf.(λx.f (x x)) (λx.f (x x))。定點組合器用於在無類型lambda演算中實現一般遞歸，而無需任何額外的遞歸構造，這是使非類型化lambda演算Turing-complete成爲可能的一部分。

當人們開發simply-typed lambda calculus，這是一個天真的靜態類型系統的頂端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使用'a foo和'a foo -> 'a之間轉換，反之亦然。

無論何時您需要調用函數本身而不是x x，您都必須明確編寫(unwrap x) x（或unwrap x x）;即unwrap將其變成可以應用於原始值的功能。

P.S.另一個ML語言OCaml有一個選項來啓用遞歸類型（通常是禁用的）;如果您使用-rectypes標誌運行解釋器或編譯器，則可以編寫諸如fun x -> x x之類的內容。基本上，在幕後，類型檢查器計算出需要「包裝」和「解開」遞歸類型的位置，然後將它們插入到您的位置。我不知道任何具有類似遞歸類型功能的標準ML實現。

來源

2012-02-07 05:42:25 newacct

「我不知道有任何標準ML實現具有類似的遞歸類型功能」：SML的定義不允許它，所以沒有實現永遠不會有這個。將它包裝成數據類型的需求可能是有道理的。看一個像''a f ='a f - >'a'這樣的類型定義，我認爲這是一種重寫規則或一種評估，而不是一種類型。但可能是我對此有偏見。 – Hibou57 2014-09-17 00:58:56

將其參數應用於自身的函數？

回答

相關問題