Función que aplica su argumento a sí mismo?

Question

considera la siguiente función SML:

fn x => x x 

Esto produce el siguiente error (ml estándar de Nueva Jersey v110.72):

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

puedo especie de ver por qué esto no está permitido - - por un lado, no estoy seguro de cómo escribir qué tipo de letra sería, pero no es completamente absurdo; por ejemplo, podría pasarle la función de identidad y recuperarla.

¿Hay un nombre para esta función? (¿Hay alguna forma de expresarlo en SML?)

Answer 1

No hay forma de expresar esta función en un lenguaje con un sistema tipo ML. Incluso con la función de identidad no funcionaría, porque el primer x y el segundo en x x tendrían que ser instancias diferentes de esa función, del tipo (_a -> _a) -> (_a -> _a) y _a -> _a, respectivamente, para algún tipo _a.

De hecho, los sistemas de tipo están diseñados para prohibir construcciones como

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

en el cálculo lambda sin tipo. En el esquema de lenguaje de tipos dinámicos, puede escribir esta función:

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

y obtener el resultado esperado

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

Answer 2

funciones de este tipo se encuentran a menudo en los combinadores de punto fijo. p.ej. una forma del Y combinator se escribe λf.(λx.f (x x)) (λx.f (x x)). Los combinadores de punto fijo se utilizan para implementar la recursión general en cálculo lambda no tipeado sin construcciones recursivas adicionales, y esto es parte de lo que hace que el cálculo lambda no tipado sea completo.

Cuando las personas desarrollaron simply-typed lambda calculus, que es un ingenuo sistema de tipo estático encima del cálculo lambda, descubrieron que ya no era posible escribir tales funciones. De hecho, no es posible realizar una recursión general en el cálculo lambda de tipo simple; y por lo tanto, el cálculo lambda de tipo simple ya no es Turing-completo. (Un efecto secundario interesante es que los programas en escrito con sencillez cálculo lambda siempre terminar.)

lenguajes de programación real de tipo estático como necesidad ml estándar incorporados mecanismos recursivos para superar el problema, tales como las funciones recursivas con nombre (se definió con val rec o fun) y se denominaron tipos de datos recursivos.

Todavía es posible usar tipos de datos recursivos para simular algo como lo que quiere, pero no es tan bonito.

Básicamente, quiere definir un tipo como 'a foo = 'a foo -> 'a; sin embargo, esto no está permitido. En su lugar, lo envuelve en un tipo de datos: datatype 'a foo = Wrap of ('a foo -> 'a);

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

Básicamente, Wrap y unwrap se utilizan para transformar entre 'a foo y 'a foo -> 'a, y viceversa.

Cuando necesite llamar a una función sobre sí mismo, en lugar de x x, debe escribir explícitamente (unwrap x) x (o unwrap x x); es decir, unwrap lo convierte en una función que luego puede aplicar al valor original.

P.S. Otro lenguaje ML, OCaml, tiene una opción para habilitar tipos recursivos (normalmente desactivado); si ejecuta el intérprete o compilador con el indicador -rectypes, entonces es posible escribir cosas como fun x -> x x. Básicamente, entre bastidores, el verificador de tipos determina los lugares donde debe "ajustar" y "desenvolver" el tipo recursivo, y luego se los inserta por usted. No conozco ninguna implementación de ML estándar que tenga una funcionalidad similar de tipos recursivos.