-----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. You still can't really do anything with the value, but you can at least observe something about its computation. The uses of this may be obscure (I can't think of any right now), but I wouldn't say they necessarily don't exist. - - Jake -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkl3eb8ACgkQye5hVyvIUKnGZgCcDvZKVmqcwjdx97MkPu3I5r3n KsUAn0IlCTwyCH5h5QTyDPvM1MkX36Hz =Ocgm -----END PGP SIGNATURE-----