It was brought to my attention that the cost of type inference in a functional language like OCaml can be very high. The claim is that there is a sequence of expressions such that for each expression the length of the corresponding type is exponential on the length of the expression. I devised the sequence below. My question is: do you know of a sequence with more concise expressions that achieves the same types? # fun a -> a;; - : 'a -> 'a = <fun> # fun b a -> b a;; - : ('a -> 'b) -> 'a -> 'b = <fun> # fun c b a -> c b (b a);; - : (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun> # fun d c b a -> d c b (c b (b a));; - : ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) -> (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'd = <fun> # fun e d c b a -> e d c b (d c b (c b (b a)));; - : (((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) -> (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) -> ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) -> (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'e = <fun> # fun f e d c b a -> f e d c b (e d c b (d c b (c b (b a))));; - : ((((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) -> (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) -> ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) -> (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'e -> 'f) -> (((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) -> (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'd -> 'e) -> ((('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'c -> 'd) -> (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'f = <fun>