Funzione che applica il proprio argomento a se stesso?

Question

Si consideri la seguente funzione SML:

fn x => x x 

Questo produce il seguente errore (Standard ML del New Jersey v110.72):

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

posso sorta di capire perché questo non è consentito - - per esempio, non sono sicuro di come scrivere quale sarebbe il suo tipo - ma non è completamente privo di senso; per esempio, potrei passare la funzione di identità e riprenderlo.

Esiste un nome per questa funzione? (C'è un modo per esprimerlo in SML?)

Answer 1

Non c'è modo di esprimere questa funzione in una lingua con un sistema di tipo simile a ML. Anche con la funzione Identity non funzionerebbe, perché il primo x e il secondo in x x dovrebbero essere diverse istanze di tale funzione, di tipo (_a -> _a) -> (_a -> _a) e _a -> _a, rispettivamente, per alcuni tipo _a.

Infatti, i sistemi di tipo sono progettati per impedire costrutti come

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

nel lambda calcolo tipizzato. Nello schema linguaggio tipizzato in modo dinamico, è possibile scrivere questa funzione:

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

e ottenere il risultato previsto

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

Answer 2

Le funzioni di questo tipo sono spesso incontrate nella combinatori a virgola fissa. per esempio. una forma di Y combinator è scritta λf.(λx.f (x x)) (λx.f (x x)). I combinatori a virgola fissa vengono utilizzati per implementare la ricorsione generale nel calcolo lambda non tipizzato senza alcun costrutto ricorsivo aggiuntivo, e questo fa parte di ciò che rende il calcolo lambda non tipizzato Turing-completo.

Quando le persone hanno sviluppato simply-typed lambda calculus, che è un sistema di tipo statico ingenuo in cima al calcolo lambda, hanno scoperto che non era più possibile scrivere tali funzioni. Infatti, non è possibile eseguire la ricorsione generale in lambda calcolo semplice; e quindi, il calcolo lambda semplicemente tipizzato non è più completo di Turing. (Un effetto collaterale interessante è che i programmi in modo semplice, digitato lambda calcolo sempre terminare.)

reale staticamente tipizzato linguaggi di programmazione come necessità standard ML built-in meccanismi ricorsivi per superare il problema, come ad esempio funzioni ricorsive nome (definito con val rec o fun) e con tipi di dati ricorsivi denominati.

È ancora possibile utilizzare tipi di dati ricorsivi per simulare qualcosa di simile a ciò che si desidera, ma non è così bello.

Fondamentalmente, si desidera definire un tipo come 'a foo = 'a foo -> 'a; tuttavia, questo non è permesso. È invece avvolgerla in un tipo di dati: datatype 'a foo = Wrap of ('a foo -> 'a);

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

Fondamentalmente, Wrap e unwrap sono utilizzati per trasformare tra 'a foo e 'a foo -> 'a, e viceversa.

Ogni volta che è necessario chiamare una funzione su sé stesso, invece di x x, è necessario scrivere esplicitamente (unwrap x) x (o unwrap x x); Ad esempio, unwrap lo trasforma in una funzione che è possibile applicare al valore originale.

P.S. Un altro linguaggio ML, OCaml, ha un'opzione per abilitare i tipi ricorsivi (normalmente disabilitati); se si esegue l'interprete o il compilatore con il flag -rectypes, è possibile scrivere cose come fun x -> x x. Fondamentalmente, dietro le quinte, il type-checker individua i punti in cui è necessario "avvolgere" e "scartare" il tipo ricorsivo, e quindi inserirli per te. Non sono a conoscenza di alcuna implementazione di standard ML con funzionalità di tipi ricorsivi simili.