Hindley-Milner型推論の実行時間最悪ケース

code:ocaml --version

The OCaml toplevel, version 4.06.0

code:worst.ml

let f x = (x, x) in

let f x = f (f x) in

let f x = f (f x) in

let f x = f (f x) in

let f x = f (f x) in

let f x = f (f x) in

f 1

$ \tau_0 = int \ast int

$ \tau_n = \tau_{n - 1} \ast \tau_{n - 1}

型が爆発的に大きくなるのに伴って単一化にも時間がかかるようになる？

この式をOCaml REPLに投げると応答に1分以上かかる

手元の環境では1時間経っても応答しなかった

Hindley-Milner型推論をするwebサービスにこのような式を投げるとタイムアウトすると思う

こういうのを投げまくるとDoS攻撃になりそう

TaPLの22章で言及されてた

In the worst case, it is just as inefficient as textually expanding the corresponding let construct in the program’s source code, and leads to exponential time complexity. In practice, however, the unification constraint U is often compact because it was simplified before the environment frame let x : σ in [] was created, which explains why the solver usually performs well.

型が複雑でなく、かつ型推論に時間がかかるケース

code:comp_ids.ml

let id x = x in

let f x = id id id id id id id id id id id id id id id id id id id id id id id id id id id id id id x in

f 1

この式の型はintである

手元の環境では応答を返すまで26分ほどかかった