Linea di OCaml produce errore misterioso

Question

Quando eseguo il codice

let (a,p) = (2+2, Printf.printf) in p "abc"; p "%d" 3 ;; 

Mi aspetto di vedere l'uscita abc3, ma avere invece

File "f.ml", line 1, characters 46-47: 
Error: This function has type (unit, out_channel, unit) format -> unit 
     It is applied to too many arguments; maybe you forgot a `;'. 

La parte divertente è che se cambio 2+2-2 , corre.

Perché il codice genera un errore così com'è, ma non con +2 rimosso?

Answer 1

Una combinazione del trucco di battitura speciale di OCaml per printf e il polimorfismo del valore.

Come probabilmente sapete, Printf.printf non richiede string ma il tipo di dati format. OCaml tipo checker ha una regola speciale per la digitazione di stringhe letterali per printf: se viene digitato come format se il contesto richiede:

# "%d";; 
- : string = "%d" 
# ("%d" : _format);; 
- : (int -> 'a, 'b, 'a) format = ... 

sistema di tipo OCaml ha un altro valore trucco chiamato polimorfismo (più precisamente, è il valore rilassato polimorfismo). Il suo scopo è di digitare correttamente le espressioni con gli effetti collaterali. Non mi spiego i suoi dettagli, ma limita il polimorfismo: alcune forme di espressioni chiamate "espansivo" non può avere tipi polimorfici:

# fun x -> x;; 
- : 'a -> 'a = <fun> 
# (fun x -> x) (fun x -> x) 
- : '_a -> '_a = <fun> 

In quanto sopra, (fun x -> x) (fun x -> x) ha nessun tipo polimorfico, mentre la funzione identità fun x -> x ha. Ciò è dovuto alla forma dell'espressione di (fun x -> x) (fun x -> x): è "espansiva". La strana variabile di tipo '_a è una variabile di tipo monomorfico: può essere istanziata ad alcuni tipi solo una volta. D'altra parte, le variabili polimorfiche come 'a possono essere istanziate a un tipo diverso per ciascun uso della vlaue.

Torniamo al codice:

# let (a, p) = (2, Printf.printf);; 
val a : int 
val p : ('a, out_channel, unit) format -> 'a 

Qui, p ha un tipo polimorfico ('a, out_channel, unit) format -> 'a. 'a può essere istanziato a più di un tipo quindi p "abc"; p "%d" 3 è tipizzabile: il tipo polimorfico può essere istanziato a (unit, out_channel, unit) format -> unit per il primo utilizzo di p e (int -> unit, out_channel, unit) format -> int -> unit per il secondo utilizzo di p.

Una volta che si cambia la costante 2-2+2, che è espansivo, l'intera espressione diventa troppo espansivo, e le variazioni di battitura:

# let (a, p) = (2+2, Printf.printf);; 
val a : int 
val p : ('_a, out_channel, unit) format -> '_a 

Qui, p non ha più polimorfa variabili 'a ma monomorfa '_a. Questa variabile monomorfica è unificata (istanziata) a unit al primo utilizzo di p e, di conseguenza, il tipo p diventa (unit, out_channel, unit) format -> unit. Può richiedere solo 1 argomento, pertanto la digitazione del secondo uso di p con 2 argomenti non riesce.

Un modo semplice per evitare questa situazione è quello di dividere la sua definizione in due:

let a = 2 + 2 in 
let p = Printf.printf in 
p "abc"; p "%d" 3