Reducing a recursively parameterized data type?

Learning
1

Suppose I have the following tree type:

type _ weirdtree =
  | Leaf : int -> int weirdtree
  | Node : ('a weirdtree * 'a weirdtree) -> 'a weirdtree weirdtree

Suppose I want to convert the tree into a list:

let rec list_of_weirdtree : 'a . 'a weirdtree -> int list = fun w ->
  match w with
  | Leaf n -> [n]
  | Node (l, r) -> (list_of_weirdtree l) @ (list_of_weirdtree r)

This results in the following error, with Node (l, r) underlined:

Error: This pattern matches values of type $0 weirdtree weirdtree
       but a pattern was expected which matches values of type int weirdtree
       The type constructor $0 would escape its scope

Which mostly makes sense to me. But is there a way to get this sort of function to typecheck? Most of the online results I get for the “type constructor would escape its scope” error seem to be solved by using an explicit polymorphic type annotation, but that doesn’t seem to do the trick here.

Thank you!

2

Note that it works as expected for a different definition of the weirdtree type:

type _ weirdtree =
  | Leaf : int -> int weirdtree
  | Node : ('a weirdtree * 'a weirdtree) -> 'a weirdtree

(Note the missing weirdtree at the end of the last line)
But I want to try to encode the height of the tree into the type, hence the difficulty.

3

You need both an explicit polymorphic annotation, for polymorphic recursion, and a locally abstract type (type a) for GADT matching. You can neatly combine both using let rec list_of_weirdtree : type a. a weirdtree -> int list = fun ....
In fact, it is commonly advised to always use the type a. syntax when writing polymorphic type annotations, even if you don’t actually need the locally abstract type.

4

That was it, thank you! I was confused about locally abstract types before but this makes a lot of sense.

5

I do have a follow-up question. If I change the weirdtree definition so that leafs can hold some variable type as follows:

type _ weirdtree =
  | Leaf : 'a -> 'a weirdtree
  | Node : ('a weirdtree * 'a weirdtree) -> 'a weirdtree weirdtree

Then is there still a way to get the typing of list_of_weirdtree to work out?

6

What would you expect the type of list_of_weirdtree to be ? 'a weirdtree -> 'a list is probably wrong, as you want the content of the leaves, which is not of type 'a if your tree has at least one node. 'a weirdtree -> 'b list is wrong too, as you can’t produce a list of any type from any weirdtree. Even trying to existentially quantify over 'b (instead of universally) wouldn’t work, as you wouldn’t be able to type the recursive call.

The usual solution is to add a type parameter to weirdtree, for instance ('elt, 'height) weirdtree, where 'elt is the type of things stored in leaves and 'height the one that encodes the height of the tree. Then list_of_weirdtree would have type type elt height . (elt, height) weirdtree -> elt list.

1 Like
7

That’s what I couldn’t figure out; I was wondering if there’s a way around it. The solution makes sense.

Very much appreciated!