I don't even think that's just a joke, that's what dynamically typed languages are from a type theory point of view (well, I guess the type theory doesn't care

I don't even think that's just a joke, that's what dynamically typed languages are from a type theory point of view (well, I guess the type theory doesn't care if you call that type "hashtable" or "any" or "foobar").