[Haskell-cafe] Re: Existencial quantification and polymorphic datatypes (actually, components...)

[Jonathan Cast]

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