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.
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.