anyway type checking is 100% a syntactic op. how could it be otherwise?

even with dynamic langs. why does 1/0 fail at runtime? because the hw rejects it - a syntax error. not because "1/0 is undefined". just the opposite - it's undefined because it does not syntax-check.

i had no idea The Matrix was set in Chicago.

polymorphism uses universal types (forall X . T); there's another class of types called "existential types" (exists X. T) I'm having problem understanding when existential types is ever useful

https://wiki.haskell.org/Existential_type claims to be about existential types, yet there's no exists and it's all 'forall'

I get it now. The key point I was missing is: forall x. ( Q(x) => P ) === (exists x. Q(x)) => P and this is why I was "seeing all the forall, but no exists"

@qqq Agda and Idris are both pretty great for learning type theory, if you are interested

I only have (very limited) experience with Agda though

but have heard very good things about Idris

https://github.com/LuxLang/lux looks interesting