OCaml: ¿Hay alguna función con el tipo 'a ->' que no sea la función de identidad?

Question

Por cierto, esta no es una pregunta de tarea. Se crió en clase pero a mi maestra no se le ocurrió ninguna. Gracias.

Answer 1

¿Cómo se define la función identidad? Si sólo está pensando en la sintaxis, hay diferentes funciones de identidad, que todos tienen el tipo correcto:

let f x = x 
let f2 x = (fun y -> y) x 
let f3 x = (fun y -> y) (fun y -> y) x 
let f4 x = (fun y -> (fun y -> y) y) x 
let f5 x = (fun y z -> z) x x 
let f6 x = if false then x else x 

Hay algunas funciones aún más extraño:

let f7 x = if Random.bool() then x else x 
let f8 x = if Sys.argv < 5 then x else x 

Si se restringe a sí mismo a un subconjunto pura de OCaml (lo que descarta F7 y F8), todas las funciones que se pueden construir verificar una ecuación de observación que asegura, en un sentido, que lo que ellos calculan es la identidad: para todo valor f : 'a -> 'a, tenemos que f x = x

Esta ecuación no depende de la función específica, solo está determinada por el tipo. Hay varios teoremas (enmarcados en contextos diferentes) que formalizan la idea informal de que "una función polimórfica no puede cambiar un parámetro de tipo polimórfico, solo pasarlo". Véase, por ejemplo, el documento de Philip Wadler, Theorems for free!.

Lo bueno de esos teoremas es que no solo se aplican al caso 'a -> 'a, que no es tan interesante. Puede obtener un teorema del tipo ('a -> 'a -> bool) -> 'a list -> 'a list de una función de clasificación, que dice que su aplicación conmuta con el mapeo de una función monótona. Más formalmente, si tiene alguna función s con un tipo tal, a continuación, para todos los tipos u, v, funciones cmp_u : u -> u -> bool, cmp_v : v -> v -> bool, f : u -> v, y la lista li : u list, y si cmp_u u u' implica cmp_v (f u) (f u') (f es monótona), usted tiene:

map f (s cmp_u li) = s cmp_v (map f li) 

Esto es cierto cuando s es exactamente una función de clasificación, pero me parece impresionante poder demostrar que es cierto para cualquier función s con el mismo tipo.

Una vez que permitirá no terminación, ya sea divergente (bucle indefinidamente, al igual que con la let rec f x = f x función dada más arriba), o mediante el aumento de excepciones, por supuesto, puede tener cualquier cosa: usted puede construir una función del tipo 'a -> 'b y tipos ya no significas nada Usar Obj.magic : 'a -> 'b tiene el mismo efecto.

Existen formas más sanas de perder la equivalencia con la identidad: se puede trabajar en un entorno no vacío, con valores predefinidos accesibles desde la función. Considere, por ejemplo, la siguiente función:

let counter = ref 0 
let f x = incr counter; x 

Usted todavía que la propiedad de que para todo x, f x = x: si sólo tienen en cuenta el valor de retorno, su función sigue comporta como la identidad. Pero una vez que considera los efectos secundarios, ya no es equivalente a la identidad (sin efecto secundario): si sé counter, puedo escribir una función de separación que devuelva true cuando se le dé esta función f, y devolvería falso para funciones de identidad pura.

let separate g = 
    let before = !counter in 
    g(); 
    !counter = before + 1 

Si el contador está oculto (por ejemplo, mediante una firma módulo, o simplemente let f = let counter = ... in fun x -> ...), y ninguna otra función puede observar que, a continuación, podemos volver a no distinguir f y las funciones de identidad puros. Entonces la historia es mucho más sutil en presencia del estado local.

Answer 2

let rec f x = f (f x) 

Esta función nunca termina, pero tiene el tipo 'a -> 'a.

Si solo permitimos las funciones totales, la pregunta se vuelve más interesante. Sin utilizar trucos del mal, no es posible escribir una función total de tipo 'a -> 'a, pero trucos malignos son diversión así:

let f (x:'a):'a = Obj.magic 42 

Obj.magic es abominación mal del tipo 'a -> 'b que permite todo tipo de chanchullos para eludir el sistema de tipos .

Pensándolo bien, tampoco uno es total porque se bloqueará cuando se use con tipos de cajas.

Entonces la verdadera respuesta es: la función de identidad es la única función total del tipo 'a -> 'a.

Answer 3

lanzar una excepción también se le puede dar un tipo 'a -> 'a:

# let f (x:'a) : 'a = raise (Failure "aaa");; 
val f : 'a -> 'a = <fun> 

Answer 4

Si se limita a un cálculo λ razonablemente "normalizado" fuertemente normalizado, existe una única función de tipo ∀α α → α, que es la función de identidad. Puede probarlo examinando las posibles formas normales de un término de este tipo.

El artículo "Theorems for Free" de Philip Wadler de 1989 explica cómo las funciones que tienen tipos polimórficos satisfacen necesariamente ciertos teoremas (por ejemplo, una función tipo mapa conmuta con la composición).

Sin embargo, hay algunos problemas no intuitivos cuando se trata de mucho polimorfismo. Por ejemplo, hay un truco estándar para codificar tipos inductivos y recursión con polimorfismo impredicativo, representando un objeto inductivo (por ejemplo, una lista) usando su función de recursor. En algunos casos, hay términos que pertenecen al tipo de la función de recursor que no son funciones de recursor; hay un ejemplo en §4.3.1 de Christine Paulin's PhD thesis.