どんなプログラミング言語にも“型”の概念はありますが、 制限が強過ぎたり（安全だが窮屈）、弱すぎたり（自由だが危険）、 ちょうどバランスの良い型システムの設計は難しいのです。
型推論はプログラマが楽をしつつ、安全なプログラムを作成するための仕組みです。 今後、主流の言語にも何らかの形で採用されると考えられます。
型推論の研究自体は抽象的なものなので、お見せできるようなデモはありませんが、 気分だけ示すために、（数学的な表記による）型推論のアルゴリズムを示します。