Función ML de tipo 'a ->' b

Nuestro profesor nos pidió que pensáramos en una función en OCaml que tenga el tipo

'a -> 'b

es decir, una función de un argumento que podría ser cualquier cosa, y que puede devolver una cosa diferente.

Pensé en usar raiseuna función que ignora su argumento:

let f x = raise Exit

Pero el profesor dijo que había una solución que no requiere ninguna función en la biblioteca estándar. Estoy confundido: ¿cómo puedes hacer un 'bsi no tienes uno en primer lugar?

_{Estoy preguntando aquí en lugar de en Stack Overflow porque quiero entender lo que está sucediendo, no quiero ver un programa sin ninguna explicación.}

El esqueleto es let f x = BODY. En BODY debe usar x solo de forma genérica (por ejemplo, no lo envíe a una función que espere números enteros), y debe devolver un valor de cualquier otro tipo. Pero, ¿cómo puede ser cierta la última parte? La única forma de satisfacer la declaración "para todos los tipos 'b, el valor devuelto es un valor de tipo 'b" es asegurarse de que la función no regrese. Hay exactamente dos posibilidades: fallas del CUERPO o no termina. La función raisefalla, lo siguiente no termina:

let rec f x = f x

Primero, algunas observaciones. Usando solo el cálculo lambda tipificado por núcleo no es posible obtenerlo 'a -> 'bporque el sistema de tipificación está en correspondencia (a través del isomorfismo de Curry Howard ) con las lógicas intuicionistas, y la fórmula correspondiente A → Bno es una tautología.

Otras extensiones, como las tuplas y los emparejamientos / condicionales, aún conservan cierta coherencia lógica agregando tipos de productos *que corresponden al conectivo lógico y , y tipos de suma |que corresponden al o . Nuevamente, no espere que produzcan ese 'a -> 'btipo, ya que permitiría probar alguna fórmula que no sea una tautología.

Entonces, sus únicas posibilidades son usar otras construcciones que escapen de las lógicas como raise(pero no está permitido en este caso) ... let rec¡ o ! La recursión permite crear programas que nunca terminan, y sus resultados pueden recibir un tipo de retorno arbitrario, ya que nunca se producirán. Ahora, si piensa en la función no terminante más trivial (la que se llama directamente a sí misma para devolver un resultado):

let rec f x = f x

Notarás que su tipo es exactamente 'a -> 'b : cualquiera que sea el argumento proporcionado, se puede suponer que el resultado (que nunca se calculará) tiene cualquier tipo.

Por supuesto, esta fno es una función interesante, pero ese es el punto. En OCaml, cualquier función cuyo tipo no parezca una fórmula válida es una función sospechosa.

Usando un compilador primitivo puedes escribir esto:

external magic: 'a -> 'b = "%identity"

(y, de hecho, la distribución del compilador proporciona esto, aunque no es parte del lenguaje). Este es un elenco de identidad inseguro.

Su profesor casi seguro no quiere esto. Sin embargo, este también es el único útil función con el tipo 'a -> 'bque conozco, y de hecho se usa en la distribución OCaml.