type inference in OCaml says my function is 'a list list -> list while it should be 'a list

user_12652009 0
Viewed 92

I am new to OCaml and have very little experience with functional programming. I have written the following function

let rec reverse l =
  match l with
  | [] -> []
  | h::rest -> (reverse rest) @ h

which is supposed to reverse the elements in a list, transforming [1;2;3] into [3;2;1] for instance. I don't know if the function will work but the issue is that OCaml infers that function to be of type 'a list list -> 'a list while I'd expect it to be an 'a list -> 'a list.

# reverse [1;2;3;4];;
Error: This expression has type int but an expression was expected of type 'a list
type-inference ocaml functional-programming
2 Answers

The concatenation operator @ expects both its operands to be lists.

When you write (reverse rest) @ h, it is immediately inferred that h must be a list. Since l = h::rest and h is a list, then l must be a list of lists.

Instead, try to replace (reverse rest) @ h with (reverse rest) @ [h]. This should work correctly.

However, note that the concatenation a @ b takes time linear in the length of a. Since you call this concatenation repeatedly, the overall complexity of your algorithm is quadratic. That's very slow. It is actually possible to reverse a list in linear time if you use an accumulator to build the reversed list progressively, using only :: and never @.

user_30807230

The OCaml typechecker always infers the best possible type for an implementation ((outside of advanced features like GADTs, higher-rank polymorphism and first class modules)).

Thus, if the inferred type of a function does not match your expectation, it means that there is an error in your implementation.

Here, the issue is that the type of (@) is 'a list -> 'a list -> 'a list. Thus reverse rest @ h implies that:

  • h is a list (thus l is a list of list of some element 'b).
  • reverse rest as the same type as h

Consequently, the type of reverse is 'b list list -> 'b list.

user_73693660
Related