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

funciones listas haskell

Question

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

Answer 1

Lanzar una excepción también puede darle un tipo ''a -> ''a :

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

Answer 2

¿Cómo defines las funciones de identidad? Si solo está considerando la sintaxis, existen diferentes funciones de identidad, que todas 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 funciones incluso más extrañas:

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

Si te limitas a un subconjunto puro de OCaml (que descarta f7 y f8), todas las funciones que puedes construir verifican una ecuación observacional que garantiza, en cierto sentido, que lo que computan es la identidad: para todo el valor f : ''a -> ''a , tenemos ese fx = 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 lo pasa". ¡Ver por ejemplo el papel de Philip Wadler, Theorems gratis! .

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 (''a -> ''a -> bool) -> ''a list -> ''a list tipo de (''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 con ese tipo, para todos los tipos u, v , funciones cmp_u : u -> u -> bool , cmp_v : v -> v -> bool , f : u -> v , y lista li : u list , y si cmp_u u u'' implica cmp_v (fu) (f u'') (f es monótona), tienes:

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 con el mismo tipo.

Una vez que permite la no terminación, ya sea por divergencia (bucle indefinido, como con la función let rec fx = fx dada anteriormente), o al elevar excepciones, por supuesto puede tener cualquier cosa: puede construir una función de tipo ''a -> ''b , y los tipos ya no significan nada. Usando Obj.magic : ''a -> ''b tiene el mismo efecto.

Hay maneras más seguras de perder la equivalencia con la identidad: podría trabajar dentro de 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 tiene la propiedad de que para todo x, fx = x : si solo considera el valor de retorno, su función aún se comporta como la identidad. Pero una vez que considera los efectos secundarios, ya no es equivalente a la identidad (libre de efectos secundarios): si conozco el counter , puedo escribir una función de separación que devuelve true cuando se le da 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 de módulo, o simplemente let f = let counter = ... in fun x -> ... ), y ninguna otra función puede observarlo, entonces nuevamente no podemos distinguir f y las funciones de identidad pura. Entonces la historia es mucho más sutil en presencia del estado local.

Answer 3

let rec f x = f (f x)

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

Si solo permitimos funciones totales, la pregunta se vuelve más interesante. Sin usar trucos malvados, no es posible escribir una función total de tipo ''a -> ''a , pero los trucos malvados son divertidos así que:

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

Obj.magic es una abominación maligna de tipo ''a -> ''b que permite todo tipo de travesuras eludir el sistema de tipos.

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

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

Answer 4

Si se restringe a un cálculo λ de tipo "razonable" fuertemente normalizador, 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 de Philip Wadler de 1989 titulado "Teoremas de forma gratuita" 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, al representar un objeto inductivo (por ejemplo, una lista) utilizando 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 la tesis doctoral de Christine Paulin .