# Why aren't polymorphic type variables inferred? **URL:** \ **Category:** Learning\ **Created:** [December 22, 2024, 7:47pm UTC](https://discuss.ocaml.org/t/why-arent-polymorphic-type-variables-inferred/15834 "2024-12-22T19:47:59Z")\ **Posts on this page:** 7\ **Page:** 1
**Author:** ![ninjaaron](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ninjaaron/32/1885_2.png) [@ninjaaron](https://discuss.ocaml.org/u/ninjaaron)\ **Post date:** [December 22, 2024, 7:47pm UTC](https://discuss.ocaml.org/t/why-arent-polymorphic-type-variables-inferred/15834/1 "2024-12-22T19:47:59Z")
I’ve been implementing a [finger tree](https://www.staff.city.ac.uk/~ross/papers/FingerTree.pdf) the past few days (yes, I know there is one in batteries). It has a type like this: ```ocaml type 'a node = | Node2 of 'a * 'a | Node3 of 'a * 'a * 'a type 'a finger_tree = | Empty | Single of 'a | Deep of 'a list * 'a node finger_tree * 'a list ``` As you can see, the `Deep` member of `finger_tree` contains a reference to a finger tree of a different type, which in turn means that functions operating on these objects recursively use _polymorfic recursion_; i.e. the recursive call will be to a type that is different than the input type. For example: ```ocaml let rec fold_left : 'a. ('b -> 'a -> 'b) -> 'b -> 'a finger_tree -> 'b = fun f acc t -> match t with | Empty -> acc | Single x -> f acc x | Deep (pr,mid,sf) -> let f' = List.fold_left f and f'' = fold_left (Node.fold_left f) in f' (f'' (f' acc pr) mid) sf ``` I understand why the polymorphic annotation is needed here (`'a.` in the type signature—which is not well documented, by the way) in terms of OCaml’s normal behavior. What I don’t understand is why the types necessary for polymorphic recursion cannot be inferred. Why is that? ---
**Author:** ![liate](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/liate/32/5551_2.png) [@liate](https://discuss.ocaml.org/u/liate)\ **Post date:** [December 22, 2024, 9:33pm UTC](https://discuss.ocaml.org/t/why-arent-polymorphic-type-variables-inferred/15834/2 "2024-12-22T21:33:25Z")
Type inference of polymorphic recursion is undecidable. (Source: [Wikipedia](https://en.m.wikipedia.org/wiki/Polymorphic_recursion), IIRC also the Okasaki book.) You could probably add some heuristics to the type inference engine for some common cases, but that would be complicated, I’d bet it would cause much worse type errors, and people don’t use polymorphic recursion all that often (even though it is cool and useful!). Haskell, and then OCaml, choose to just not and require type annotations when programmers actually mean polymorphic recursion. ---
**Author:** ![yawaramin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yawaramin/32/3384_2.png) [@yawaramin](https://discuss.ocaml.org/u/yawaramin)\ **Post date:** [December 22, 2024, 9:49pm UTC](https://discuss.ocaml.org/t/why-arent-polymorphic-type-variables-inferred/15834/3 "2024-12-22T21:49:56Z")
> [@ninjaaron](#): > > `'a.` in the type signature—which is not well documented, by the way) Seems to be documented here: [OCaml - Polymorphism and its limitations](https://ocaml.org/manual/5.2/polymorphism.html#ss:explicit-polymorphism) Is anything missing? ---
**Author:** ![ninjaaron](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ninjaaron/32/1885_2.png) [@ninjaaron](https://discuss.ocaml.org/u/ninjaaron)\ **Post date:** [December 22, 2024, 9:57pm UTC](https://discuss.ocaml.org/t/why-arent-polymorphic-type-variables-inferred/15834/4 "2024-12-22T21:57:11Z")
I guess I was looking in the wrong spot: [OCaml - Types](https://ocaml.org/manual/5.2/types.html). 😑 ---
**Author:** ![ninjaaron](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ninjaaron/32/1885_2.png) [@ninjaaron](https://discuss.ocaml.org/u/ninjaaron)\ **Post date:** [December 22, 2024, 9:59pm UTC](https://discuss.ocaml.org/t/why-arent-polymorphic-type-variables-inferred/15834/5 "2024-12-22T21:59:52Z")
That’s a good answer. Why don’t we do it like Haskell, where simply adding the type annotation allows for polymorphic type variables? Why do we need `a.`? Maybe this is a stupid question, since OCaml does many things differently than Haskell and tends to favor explicitness and verbosity (relatively speaking). ---
**Author:** ![liate](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/liate/32/5551_2.png) [@liate](https://discuss.ocaml.org/u/liate)\ **Post date:** [December 22, 2024, 10:46pm UTC](https://discuss.ocaml.org/t/why-arent-polymorphic-type-variables-inferred/15834/6 "2024-12-22T22:46:26Z")
The direct reason is right above the section @yawaramin linked: normal type variable instantiation is shared with the recursive calls (so it’s trying to unify `'a` with `'a node`), while explicitly polymorphic type variables are instantiated per call. I’m not sure _why_ it does it this way, though; I’d guess it makes type checking significantly faster or simpler, or is connected with some type inference improvements? Maybe it makes some features OCaml has that Haskell doesn’t work better? ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [December 23, 2024, 7:24am UTC](https://discuss.ocaml.org/t/why-arent-polymorphic-type-variables-inferred/15834/7 "2024-12-23T07:24:04Z")
> [@ninjaaron](#): > > Why don’t we do it like Haskell, where simply adding the type annotation allows for polymorphic type variables? This is exactly what the annotation ```ocaml let rec fold_left : 'a. ('b -> 'a -> 'b) -> 'b -> 'a finger_tree -> 'b ``` is doing with an explicit universal quantification of the type variable `'a`. Without such quantification, OCaml type variables are variables that scope other the whole definition (aka unification type variables) which allow to write ```ocaml val f: (Format.formatter -> int -> unit as 'printer) -> 'printer ``` or ```ocaml module M = struct type t = A | B end let z = let y : 'a = M.A in (y, (B:'a)) ``` It is debatable that this is the optimal default behavior, but it is at least an explicit one.