Parámetros con nombre de Ocaml

Question

Intentando comprender el mecanismo de Ocaml para parámetros con nombre. Entiendo lo básico, pero el doc muestra un ejemplo como este:

# let f ~x ~y = x - y;; 
val f : x:int -> y:int -> int = <fun> 

# let x = 3 and y = 2 in f ~x ~y;; 
- : int = 1 

¿Qué está pasando exactamente en cuando solamente la tilde se utiliza en la aplicación? ¿Es solo una abreviatura de ~x:x, similar a las definiciones? Si es así, alguien puede explicar por qué esto:

# ListLabels.fold_left;; 
- : f:('a -> 'b -> 'a) -> init:'a -> 'b list -> 'a = <fun> 

# let add = (+) and i = 0 
in ListLabels.fold_left ~add ~i [1;2;3];; 

produce

- : f:((add:(int -> int -> int) -> i:int -> 'a) -> 
    int -> add:(int -> int -> int) -> i:int -> 'a) -> 
init:(add:(int -> int -> int) -> i:int -> 'a) -> 'a = <fun> 

Answer 1

El hombre dice "cuidado que funciona como ListLabels.fold_left cuyo tipo de resultado es que nunca será considerado como una variable de tipo como totalmente aplicada "

Esto es lo que sucede en su ejemplo. Ten en cuenta que es un poco complicado.

# ListLabels.fold_left;; 
- : f:('a -> 'b -> 'a) -> init:'a -> 'b list -> 'a = <fun> 

es sólo el uso clásico: ListLabels.fold_left TAKS 3 argumentos, a saber, una función marcada f, un inicializador init y una lista.

Ahora, en

let add = (+) and i = 0 
in ListLabels.fold_left ~add ~i [1;2;3];; 

la aplicación ListLabels.fold_left ~add ~i [1;2;3] se considera incompleta (como dice el hombre). Esto significa que `ListLabels.fold_left recibe primero su argumento unmed, [1;2;3] y devuelve una función del tipo f:('a -> int -> 'a) -> init:'a -> 'a. Vamos a llamar a esta función foo.

Puesto que usted está dando dos argumentos con nombre, etiquetados y addi, el tipo 'a se infiere que ser un tipo funcional, de tipo add:'c -> ~i:'d -> 'e.

Basándose en el tipo de las variables de add y i, el tipo 'c debe haber int -> int -> int, y 'd debe ser int.

Reemplazando esos valores en el tipo 'a, derivamos que el tipo 'a es add:(int -> int -> int) -> i:int -> 'e. y reemplazando esto en el tipo de foo (Me alegro de que es copiar y pegar ;-), su tipo es

f:((add:(int -> int -> int) -> i:int -> 'e) 
    -> int 
    -> (add:(int -> int -> int) -> i:int -> 'e)) 
-> init:(add:(int -> int -> int) -> i:int -> 'e) 
-> (add:(int -> int -> int) -> i:int -> 'e) 

Extracción paréntesis innecesarios, y alfa conversión (es decir, el cambio de nombre) 'e-'a, obtenemos

f:((add:(int -> int -> int) -> i:int -> 'a) 
    -> int 
    -> add:(int -> int -> int) -> i:int -> 'a) 
-> init:(add:(int -> int -> int) -> i:int -> 'a) 
-> add:(int -> int -> int) -> i:int -> 'a 

Ese es el tipo de foo. Pero recuerde que está pasando dos argumentos a foo, etiquetados ~add y ~i. Por lo tanto, el valor que obtiene al final no es del tipo add:(int -> int -> int) -> i:int -> 'a, sino del tipo 'a. Y todo el tipo de su ejemplo es, según lo devuelto por el compilador,

f:((add:(int -> int -> int) -> i:int -> 'a) 
    -> int 
    -> add:(int -> int -> int) -> i:int -> 'a) 
-> init:(add:(int -> int -> int) -> i:int -> 'a) 
-> 'a