OCaml type inference does not yield expected type for function arguments

user_17654046 0
Viewed 71

This is a homework. I know I shouldn't ask this here but explanation would be welcomed. :)

My code looks like that:

let some_function f x = match x with 
  | (k, v) -> fun k -> f k

f should be a function and x is a list of tuples. My compiler (?) says it's ('a -> 'b) -> 'c * 'd -> 'a -> 'b but it should be ('a -> 'b) -> 'a * 'b -> 'a -> 'b

You don't need to tell me the solution just explain me why it's 'c * 'd and not 'a * 'b

type-inference ocaml function
1 Answers

First off, when you write this:

let some_function f x = match x with 
  | (k, v) -> fun k -> f k

You can pattern match directly in the function arguments.

let some_function f (k, v) = 
  fun k -> f k

Secondly, the v is never used, so let's get red of that by using _.

let some_function f (k, _) = 
  fun k -> f k

This does exactly the same thing and gives us something easier to reason about.

However, the k in fun k -> f k shadows the k in the tuple argument to the function, so you're not really using that one either.

So we really have:

let some_function f (_, _) = 
  fun k -> f k

The concrete types of these are not known, so f is inferred to be a function that takes a value of type 'a and returns a value of type 'b. Therefore f is 'a -> 'b.

That tuple that you never use? It has a type, but we can't know anything about those types from the rest of the function, so the inferred type is 'c * 'd.

We can simplify this one step further. fun k -> f k is equivalent to just writing f, so your function can be equivalently rewritten:

let some_function f (_, _) = f

Though this doesn't allow OCaml to infer that f is a function, so the type signature becomes:

'a -> 'b * 'c -> 'a
user_152613150
Related