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>
Concise example of exponential cost of ML type inference
lambda calculus;type theory;functional programming;type inference;type checking