GHCの型はキモイ

次の4つの型の意味

{-# OPTIONS -fglasgow-exts #-}
data Bot = Bot Bot
data Bot'
type Obj = forall a.a
data Obj' = forall a.Obj a

1つ目と2つ目は、大分前にコメントで教えてもらった技で、ボトムだけからなる型になるらしい(使用用途は知らない)。最後の二つで

z::Obj = (3::Integer)
w::Obj' = Obj (3::Integer)

wは問題ないけど、zは怒られる。まあ、そうだよな〜。てか、System Fなんかでは、forall a.aは、ボトムのみからなる型を意味するので、Objはボトムのみからなる型であってほしいような。しかし、そうだとすると、Dynamicを実現できるのは変じゃないかという気がする


Data.Dynamics見ると、言い訳が書いてあった。

type Obj = forall a . a
 -- Dummy type to hold the dynamically typed value.
 --
 -- In GHC's new eval/apply execution model this type must
 -- be polymorphic.  It can't be a constructor, because then
 -- GHC will use the constructor convention when evaluating it,
 -- and this will go wrong if the object is really a function.  On
 -- the other hand, if we use a polymorphic type, GHC will use
 -- a fallback convention for evaluating it that works for all types.
 -- (using a function type here would also work).

なんかGHCの実行モデルの都合が絡んでるらしい。多分、Objはvoid*みたいなもんで、あまり深く考えてはいけないというか、理論的には間違いなんだけど、うまくいくよ、と。んでもって、void*へのキャストに相当するのがunsafeCoerceという関数。そして、Dynamicは、型情報(TypeRep)と値(Obj)のペアによって実現されていると。結局、HaskellはCleanに比べて"unsafeな方法"が発達しているので(いや、Cleanを殆ど知らないので本当にそうかどうかは分からないけれども)、Dynamicをライブラリレベルで実現できるだけか