型推論とか型理論とか

例えばこういうプログラムがあるわけです。

int i = 1;
float f = (float)i;

要はただの型キャストなんだけれども、これをOcamlだとこう書くことになります。

let i = 1 in
let f = float_of_int i in ...

このfloat_of_intという関数は、int -> float = <fun>という型を持ちます。さて、それに対してC言語などでは、(float)という型キャストは、どんな型からでもfloatにキャストできます。構造体だろうが、doubleだろうが、charだろうが、とりあえず何でも出来ます。で、どちらが良いのか、という話。
Ocamlでも、例えば'a -> floatとか、'a -> stringとか、そういう型が定義できればいいなあという話はあるのですけれども、本当にそれでいいのかなあという考え方も一方であります。つまりですよ、

int i = 1;
int i2 = (int)1;;

のようなプログラムをどこの馬鹿が書くというのだろうか、という話です。で、書いていたとしたら、警告出してくれてもいいんじゃないかなあと思ったり思わなかったり。っていうか型エラー出してくれても一向に構わないと思うのです。だって明らかに不要なコードだと思いませんか？
シミュレータのバグは実はこれに由来するものだったので、そんなことを考えてみました。