Function same_shape (t1 : 'a tree) (t2 : 'b tree) gets compiled to same_shape : 'a tree -> 'a tree -> bool

Learning
1

I’m trying to make a function which compares two binary trees, to see if they have the same shape or not.

I created a type type 'a tree = | Node of 'a * 'a tree * 'a tree | Leaf. This way I can create a node with a value, and two branches.

I then wrote this function:

let rec same_shape (t1 : 'a tree) (t2 : 'b tree) =
match t1, t2 with
| Leaf, Node(_, _, _) | Node(_, _, _), Leaf -> false
| Node(_, x1, y1), Node(_, x2, y2) -> same_shape x1 x2 && same_shape y2 y2
| Leaf, Leaf -> true;;

which compiles as

val same_shape : 'a tree -> 'a tree -> bool = <fun>

The problem is when I try to compare an int tree with a string tree, I get the following error

Error: This expression has type string but an expression was expected of type
         int

I’m pretty sure that this is because the function is compiled as 'a tree -> 'a tree -> bool, but I do not want the node value to matter. So my question is, how can I write my function as a 'a tree -> 'b tree -> bool function?

2

Hi, OCaml infers types according to the implementation. In this case it unified the 'a and the 'b types into a single type because it saw that the implementation is treating them as the same type.

This means you have a bug in your implementation. Check this: same_shape y2 y2

Just to be clear, the annotationsof (t1 : 'a tree) (t2 : 'b tree) were actually ignored during the typechecking process. If you want annotations that will actually cause a type error, use an interface (either a file or a signature). E.g.,

module M : sig
  val same_shape : _ tree -> _ tree -> bool
end = struct
  let rec same_shape t1 t2 = match t1, t2 with
    | Leaf, Node (_, _, _) | Node (_, _, _), Leaf -> false
    | Node (_, x1, y1), Node (_, x2, y2) -> same_shape x1 x2 && same_shape y1 y2
    | Leaf, Leaf -> true
end
3

I wondered, reading your explanation, if that was all there was to it. So …

# let rec same_shape : 'a 'b .'a tree -> 'b tree -> bool = fun t1 t2 ->
match t1, t2 with
| Leaf, Node(_, _, _) | Node(_, _, _), Leaf -> false
| Node(_, x1, y1), Node(_, x2, y2) -> same_shape x1 x2 && same_shape y2 y2
| Leaf, Leaf -> true;;
val same_shape : 'a tree -> 'b tree -> bool = <fun>

The only change was to put the type-constraint on the recursive function definition directly. So even if one intended the bug you found, you could still get the indifference to the node-type.

Obviously this isn’t the right way to do it, and the natural way is the one that will expose the bug.

4

The annotation is not ignored during typechecking, it is just perfectly valid to infer that 'a = 'b from the call to

same_shape y1 y2

It is the issue with unification type variables which have a semantics that is not well adapted for debugging purpose.
Locally abstract types are a better fit than unification variables for such purpose. For instance,

let same_shape (type a b) =
  let rec same_shape (t1 : a tree) (t2 : b tree) =
  match t1, t2 with
  | Leaf, Node(_, _, _) | Node(_, _, _), Leaf -> false
  | Node(_, x1, y1), Node(_, x2, y2) -> same_shape x1 x2 && same_shape y2 y2
  | Leaf, Leaf -> true
  in
  same_shape

fails with

6 |   | Node(_, x1, y1), Node(_, x2, y2) -> same_shape x1 x2 && same_shape y2 y2
                                                                           ^^
Error: This expression has type b tree but an expression was expected of type
         a tree
       Type b is not compatible with type a
3 Likes
5

Ok, after doing some testing, I’m even more confused. I rewrote the function, and it magically worked. Does anyone know what I did differently?

Rewritten function:

let rec same_shape' (t1 : 'a tree) (t2 : 'b tree) =
match t1, t2 with
| Leaf, Node(_, _, _) | Node(_, _, _), Leaf -> false
| Node(_, x1, y1), Node(_, x2, y2) -> same_shape x1 x2 && same_shape y2 y2
| Leaf, Leaf -> true;;
val same_shape' : 'a tree -> 'b tree -> bool = <fun>

Also, thanks for all the help so far. This is still an odd language to me, so this really helps.

6

Did you notice that there is a typo in your function: You probably wanted to write

same_shape y1 y2

instead of

same_shape y2 y2

Your version forces the compiler to set 'a = 'b i.e. 'a and 'b must be the same type. Otherwise the code is not type correct for the compiler.

Regards
Helmut

7

Ah… I feel dumb now.

Thanks a lot!

8

Just fyi, that’s what I said earlier :wink:

1 Like
9

The glories of code review!

1 Like