∃は抽象型（abstract type）にあたります。とか超遅レス。∃α．τは「ある型αが存在して、αについては、型τの値（関数など）が利用できる」ということなので。とっくに解決してそうですが。
あと、型を値の集合とみなすこと自体はOKなのですが（というかイデアルだろうとCPOだろうと一応は集合なので）、関数型を集合論の→で解釈すると矛盾するということです。濃度とか。
あと、JavaのGenerics関係は、OderskyのGJコンパイラをSunが買収しただけなので、「影響」どころではないです。
