⊥しか取りえないってのは間違い。 MkT :: forall a. a -> Tはどんな値でも取ってT型を返す関数。 全称量化することで、型パラメータaが取り得る全ての型に共通の性質だけにしか言及できなくなる。 で、結局の所、⊥か、それ以外の何かが入ってる、としか言えなくなる。 (もちろんisBottomみたいな関数は定義できないから、実質何が入ってるかは不明) forallが積集合云々ってのは、このことを言いたいんじゃないかと思う、多分。
一応、 foo (MkT x) = x :: T -> a bar (MkT x) = id x :: T -> a dup (MkT x) = (x, x) :: T -> (a, a) みたいな関数は定義できる。 まぁT型の定義じゃ意味のある関数は定義できないけれど、値を取り出して関数適用するだけならおｋだから、 型制約付けといたり、関数とセットで入れとくと、OOPっぽいポリモーフィズムできるようになったりする。 ttp://www.kotha.net/ghcguide_ja/latest/data-type-extensions.html#existential-quantification
