Too eager infering of ocaml optional function argument

Question

Consider this code:

let myFun
  ?(f: ('a -> int) = (fun x -> x))
  (x: 'a)
    : int =
  f x

Looks i can't call with another argument other than int. When I try to with this code:

let usage = myFun ~f:String.length "abcdef"

Ocaml emits this error message:

Error: This expression has type string -> int
       but an expression was expected of type int -> int
       Type string is not compatible with type int 

Looks like the inference will think 'a = int because of the default argument. It is the limitation of the language or is there a way how to write this so it compiles?

Answer 1

This issue is a limitation due to how optionals argument are implemented.

Essentially, function with optional argument are expanded during the type checking phase using the standard option type. For instance, your function:

let f ?(conv=(fun x -> x)) x = f x

becomes, more or less,

let f opt_conv =
let conv =
  match opt_conv with
  | None -> fun x -> x
  | Some f -> f in
 fun x -> conv x

Consequently, since the opt_conv has for type 'a->'a in the None branch, f must have for type ?conv:('a->'a) -> 'a -> 'a .

Looking at the expanded function, the problem comes from the fact that the Some branch and None should have different type to obtain your desired functionality.

For the sake of type riddles, having different types in different branch of a pattern matching is a sign that GADTs may bring a potential solution: one can define an extended option type as

type ('default,'generic) optional =
  | Default: ('default,'default) optional
  | Custom: 'a -> ('default,'a) optional

then it is possible to rewrite your function as

let f: type a. (int -> int, a -> int) optional -> a -> int =
fun conv x ->
  match conv with
  | Default -> x
  | Custom f -> f x

wich leads to the expected behavior:

f Default "hi" yields a type error whereas f (Custom int_of_string) "2" returns 2.

However, without the optional argument syntactic sugar machinery, this is not really useful.

None that it is perfectly possible to extend OCaml to use the GADT-laded optional type. However this can easily lead to atrocious type errors and the corresponding increase of complexity does not make for a very attractive extension.

Answer 2

The notation ?(f: ('a -> int) doesn't mean that parameter f has type 'a -> int, it is a type constraint that tells the type inference algorithm, that f should be a function that returns a value of type int. The 'a here means just - "I don't care, infer it yourself". It doesn't generalize your type variable. Thus, given your constraint, the compiler infers, that (1) the type of f is int -> int (because this is the only input that satisfies your default value), (2) the type of x is also int, as you constrained it yourself (it will be inferred to the same type anyway, because of type of f.

Also, the type system here is right, by disallowing anything except int as the x parameter. Consider the following example:

myFun "hello"

According to your desire, it should be valid, but what OCaml should do in this case?