What are the tradeoffs of using -rectypes?

Question

I have asked a question why my attempt to do a function chaining did not work: Make a function return itself after doing some work, the answer was: for a function to return itself you need recursive types enabled with -rectypes. This confused me. Why is this feature hidden behind a compiler flag? There must be a good reason not to enable it by default. So my question is: what are the tradeoffs when using this flag? Should I avoid it or can I safely use it for all my code and it is not enabled for compatibility with old code only?

Answer 1

In brief, recursive types are both confusing for many users and often avoidable for the expert users that might need them. This is why the -rectypes option has been never been the default since its introduction in OCaml 2.03 .

In term of errors, consider for instance, this erroneous implementation of the append function

let rec quasi_append l r = match l, r with
| [], r -> r
| l, [] -> l
| x :: l, r -> x @ quasi_append l r  

without -rectypes the type system catches the error:

Error: This expression has type 'a list list
       but an expression was expected of type 'a list
       The type variable 'a occurs inside 'a list

However, with -rectypes enabled, quasi_append is a valid function of type val quasi_append : ('a list as 'a) list -> 'a list -> 'a list that only works on list of ... list of ... empty lists:

quasi_append [[];[[[]]]; [[[[]]]] ] [[]] ===  [[[]]; [[[]]]; []]

Thus -rectypes introduces complex types even in code written by beginner (in the previous example the mistake was a single :: replaced by @).

Moreover, even for expert users, explicit recursive types can often be avoided. For instance, the function in your previous question can be written without recursive types by adding one recursive type definition

type 'a fix = Fix of ('a -> 'a fix) [@@unboxed] (* See footnote ¹ *)

Here, we use the fact that fix is a recursive algebraic type to hide the recursion behind the Fix constructor. Then, we only have to box the log function in a Fix constructor in the log function to avoid having an explicit recursive type:

let rec log x = Printf.printf "%d" x; Fix log

We can even define a helper application operator which unbox the function before applying it for us

let ($) (Fix f) x = f x

Finally, we can use the log by inserting $ between each application

let boxed_log = log 111 $ 222 $ 333 $ 444 

Using those kind of techniques, recursive types can be often avoided by expert users. Moreover, there is one exception for the need to use -rectypes: recursive objects and polymorphic variants . Both recursive objects and polymorphic variants often require recursive types, but it is easy to identify code that involves either of them. Thus recursive types are enabled by default for polymorphic variants types and object types. For instance, one may write an object with a log method that returns the whole object

let o = object
  method log x =
    Printf.printf "%d" x;
    {< >}
  end
let test = ((o#log 111)#log 222)#log 333

the type of o is then < log : int -> 'a > as 'a.

Consequently, the choice was made to left -rectypes for expert users that are certain that they need the added complexity (the proof assistant Coq relies on -rectypes for instance).

---

¹ The unboxed annotation tells the compiler that it can store the function directly in memory since there is only one constructor. Thus the type constructor only exists when typechecking.

Answer 2

If this option is disabled by default it's because it will make the OCaml compiler accept a lot of code that should usually be considered as wrong, giving them weird types, producing even weirder errors and error messages. Overall, it would more often confuse than be helpful. Which is why you need to explicitly enable it.

The documentation gives a good example of such a situation:

let included l1 l2 = 
   let rec mem x = function 
     | [] -> false 
     | hd::tail -> (tail=x) || (mem x hd) (* an error on purpose: hd and tail inverted *)
   in
   List.for_all (fun x -> mem x l2) l1

In this case, without the flag, the compiler will reject this, as it should; but without, it will be accepted, and you will have the following oddities:

# included [] [];;
- : bool = true
# included [1] [];;
Error: This expression has type int but an expression was expected of type
         ('a t as 'a) t
#