Parametri con nome Ocaml

Question

Tentativo di comprendere il meccanismo di Ocaml per i parametri denominati. Capisco le basi, ma il doc mostra un esempio come questo:

# 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 

Che cosa esattamente sta succedendo, quando solo la tilde viene utilizzato in applicazioni? È solo una scorciatoia per ~x:x, simile alle definizioni? Se è così, qualcuno può spiegare perché questo:

# 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

L'uomo dice "fate attenzione che funzioni come ListLabels.fold_left il cui tipo di risultato è una variabile di tipo non potrà mai essere considerato totalmente applicata ".

Ecco cosa succede nel tuo esempio. Attenzione, è un po 'coinvolto.

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

è solo l'uso tradizionale: ListLabels.fold_left taks 3 argomenti, cioè una funzione etichettato f, un inizializzatore init e un elenco.

Ora, in

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

l'applicazione ListLabels.fold_left ~add ~i [1;2;3] è considerato incompleta (come dice l'uomo). Ciò significa che `ListLabels.fold_left riceve per primo il suo argomento unamed, [1;2;3] e restituisce una funzione di tipo f:('a -> int -> 'a) -> init:'a -> 'a. Chiamiamo questa funzione foo.

Dal momento che si sta dando due argomenti con nome, etichettati add e i, il tipo di 'a è dedotta per essere un tipo funzionale, di tipo add:'c -> ~i:'d -> 'e.

In base al tipo delle variabili add e i, il tipo di 'c deve essere int -> int -> int, e 'd deve essere int.

Sostituendo tali valori nel tipo 'a, si ricava che il tipo 'a è add:(int -> int -> int) -> i:int -> 'e. E sostituzione di questo nel tipo di foo (Sono contento C'è copia-incolla ;-), il suo tipo è

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) 

Rimozione parentesi unecessary, e alfa conversione (cioè ridenominazione) 'e-'a, otteniamo

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 

Questo è il tipo di foo. Ma ricorda che stai passando due argomenti a foo, etichettati come ~add e ~i. Quindi il valore che ottieni alla fine non è di tipo add:(int -> int -> int) -> i:int -> 'a ma di tipo 'a. E l'intero tipo del tuo esempio è, come restituito dal compilatore,

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