OCaml line makes a mysterious mistake

When i execute the code

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

I expect to see abc3 output, but instead we get

 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 `;'. 

The interesting part is that if I change 2+2 to 2 , it starts.

Why is the code creating the error as is, but not deleted with +2 ?

+6
source share
1 answer

Combination of special OCaml tag for printf and value polymorphism.

As you probably know, Printf.printf does not accept string , but the data type is format . The OCaml type checker has a special rule for entering string literals for printf : if it is printed as format , if the context asks:

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

A system like OCaml has another trick called value polymorphism (more precisely, it is a softened value polymorphism). Its purpose is to correctly type expressions with side effects. I do not explain its details, but it limits polymorphism: some forms of expressions called "expansive" cannot have polymorphic types:

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

In the above example (fun x -> x) (fun x -> x) does not have a polymorphic type, and the identity function fun x -> x has. This is due to the form of the expression (fun x -> x) (fun x -> x) : it is "expansive." A strange variable of type '_a is a variable of monomorphic type: it can be instantiated by a certain type only once. On the other hand, polymorphic variables of type 'a can be created for a different type for each vlaue use.

Back to your code:

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

Here p has a polymorphic type ('a, out_channel, unit) format -> 'a . 'a can be created for more than one type, therefore p "abc"; p "%d" 3 p "abc"; p "%d" 3 is typical: a polymorphic type can be created for (unit, out_channel, unit) format -> unit for the first use p and (int -> unit, out_channel, unit) format -> int -> unit for the second use p .

As soon as you change the constant 2 to 2+2 , which is expansive, the whole expression also becomes expansive, and the text input changes:

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

Here p no longer has the polymorphic variables 'a , but is monomorphic '_a . This monomorphic variable is unified (created) to unit first time p used, and as a result, the type p becomes (unit, out_channel, unit) format -> unit . It can take only 1 argument, so entering the second use of p with 2 arguments is not performed.

One easy way to avoid this situation is to split your definition into two:

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

All Articles