Search code examples
ocaml

Type info display mismatch in OCaml with zarith library

Why is the type info in the red box not: 'a -> 'a -> 'a -> 'a -> 'a?

enter image description here

I think all the parameters and the return value should be of the same type, and utop does confirm that they are all of Z.t type.

utop # let rec fib_acc = fun n -> fun n_1 -> fun n_2 -> fun acc ->
  if (Z.equal n Z.one) || (Z.equal n (Z.of_int 2)) 
  then acc
  else fib_acc (Z.add n Z.minus_one) n_2 (Z.add n_1 n_2) (Z.add n_1 n_2);;
val fib_acc : Z.t -> Z.t -> Z.t -> Z.t -> Z.t = <fun>
Solution

  • What do we know about the types of Z.add, Z.equal, Z.one, Z.minus_one and Z.of_int?

    You need that information if you want to conclude that n, n_1, n_2 and acc all have type Z.t.

    Without knowing the types of functions Z.add and Z.equal, we can conclude that acc and the return value have the same type, because of the then acc branch, and we can conclude that n_1 and n_2 have the same type, because n_2 in place of n_1 in the recursive call. This explains the type 'a -> 'b -> 'b -> 'c -> 'c.

    Presumably, utop has access to the types of Z.add and Z.equal, but the software which gives you the type hint 'a -> 'b -> 'b -> 'c -> 'c does not have access to that information.