A more concise example that illustrates that type inference can be very costly?
- by mrrusof
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>
