[leshow]

Can you explain what you mean by comparing universal and existential quantification to dynamic languages? Existential quantification is often used in statically typed languages and can be valuable in some cases (no pun intended). In Rust, for instance, you can say fn f() -> impl Fn(u8) -> u8 or something similar. This is existential quantification, because you're saying that f returns a type that is some Fn(u8) -> u8. This can expressiveness can be powerful in a type system. I don't see how it relates to dynamic languages.

[evincarofautumn]

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.

[leshow]

I see what you were getting at now, thanks.