con recursión mutua

Question

He estado pensando acerca de cómo funciona la inferencia de tipos en el siguiente programa de OCaml:

let rec f x = (g x) + 5 
and g x = f (x + 5);; 

Por supuesto, el programa es bastante inútil (bucle para siempre), pero ¿qué pasa con los tipos? OCaml dice:

val f : int -> int = <fun> 
val g : int -> int = <fun> 

Esto es exactamente ser mi intuición, pero ¿cómo el algoritmo de inferencia de tipos sabe esto?

Diga el algoritmo considera "f" en primer lugar: la única limitación que puede llegar es que el tipo de retorno de "g" debe ser "int", y por lo tanto su propio tipo de retorno es también "int". Pero no puede inferir el tipo de su argumento mediante la definición de "f".

Por otro lado, si considera "g" primero, puede ver que el tipo de su propio argumento debe ser "int". Pero sin haber considerado "f" antes, no puede saber que el tipo de retorno de "g" también es "int".

¿Cuál es la magia detrás de esto?

Answer 1

Supongamos que el algoritmo considera "f" primero: la única restricción que puede obtener es que el tipo de retorno de "g" debe ser "int", y por lo tanto su propio tipo de retorno también es "int". Pero no puede inferir el tipo de su argumento mediante la definición de "f".

No se puede inferir a un tipo concreto, pero puede inferir algo. A saber: el tipo de argumento de f debe ser el mismo que el tipo de argumento de g. Así que, básicamente, después de mirar f, ocaml sabe lo siguiente acerca de los tipos:

for some (to be determined) 'a: 
f: 'a -> int 
g: 'a -> int 

Después de mirar g sabe que debe haber 'aint.

Para una mirada más profunda sobre cómo funciona el algoritmo de inferencia de tipo, puede leer el artículo de Wikipedia sobre Hindley-Milner type inference o this blog post, que parece ser mucho más amigable que el artículo de Wikipedia.

Answer 2

Aquí está mi modelo mental de lo que sucede, que puede o no coincidir con la realidad.

let rec f x = 

Ok, en este punto sabemos que f es una función que toma el argumento x. Así tenemos:

f: 'a -> 'b 
x: 'a 

por alguna 'a y 'b. Siguiente:

(g x) 

Ok, ahora sabemos g es una función que se puede aplicar a x, así que agregamos

g: 'a -> 'c 

a nuestra lista de información. Continuo...

(g x) + 5 

Aha, el tipo de retorno de g debe ser int, por lo que ahora hemos resuelto 'c=int. En este punto tenemos:

f: 'a -> 'b 
x: 'a 
g: 'a -> int 

Pasando ...

and g x = 

Ok, hay una diferente x aquí, vamos a suponer que el código original tenía y lugar, para mantener las cosas más evidentes. Es decir, vamos a volver a escribir el código como

and g y = f (y + 5);; 

Ok, así que estamos en

and g y = 

por lo que ahora nuestra información es:

f: 'a -> 'b 
x: 'a 
g: 'a -> int 
y: 'a 

desde y es un argumento a g .. .y seguimos yendo:

f (y + 5);; 

y esto nos dice desde y+5 que y tiene tipo int, que resuelve 'a=int. Y dado que este es el valor de retorno de g, que ya sabemos debe ser int, esto resuelve 'b=int. Eso fue una gran cantidad en un solo paso, si el código fuera

and g y = 
    let t = y + 5 in 
    let r = f t in 
    f r;; 

entonces la primera línea mostraría y es un int, resolviendo así para 'a, y luego la siguiente línea diría que r tiene tipo 'b, y luego la última línea es la devolución de g, que resuelve 'b=int.