On Wed, 2009-01-21 at 13:38 -0600, Jake McArthur wrote:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
Gleb Alexeyev wrote: | Mauricio wrote: | |> data SomeNum = SN (forall a. a) | | [...] | | you cannot do anything to the value you extract
Maybe. Say you construct (SN x). If you later extract x, you can observe that it terminates (using seq, perhaps), assuming that it does terminate.
The definition you quoted is equivalent to data SomeNum where SN :: (forall a. a) -> SomeNum So if I say case y of SN x -> ... Then in the sequel (...) I can use x at whatever type I want --- it's polymorphic --- but whatever type I use it at, it cannot terminate. I think you meant to quote the definition data SomeNum = forall a. SN a which is equivalent to data SomeNum where SN :: forall a. a -> SomeNum in which case if I say case y of SN x -> ... then x is a perfectly monomorphic value, whose type happens to be a (fresh) constant distinct from all other types in the program. So I can't do anything useful with x, although as you say, it can be forced with seq. OTOH, you could do exactly the same thing with a normal judgment of type (), if you found a use for it. jcc