| I’m not referring to existentially quantified types—which are definitely useful & interesting in statically typed languages. What I mean is that with static types you can prove universal properties of functions. If you give me an unknown function f : ∀T. T → T in a statically typed language, then I know it always returns a value of the same type as its argument. With some assumptions (purity, parametricity, halting) I even know it must be the identity function. Whereas doing what I’m suggesting in a dynamically typed language, running inference dynamically, I could only recover existential properties: that there are some types for which f returns a value of the same type as its input. So I could recover more and more information (in the form of an intersection type) by calling the function with different inputs: f : int → int f : (int → int) ∧ (string → string) f : (int → int) ∧ (string → string) ∧ (Foo → Foo) But I could never arrive at ∀T. T → T, because that’s essentially an infinite intersection. ETA: actually I might not even be able to get this much information; I only know the output type for each input value, not each input type. |