Peter Hercek wrote:
But Haskell with Control.Exception extension has more values of all types since they can be thrown and later caught and investigated at that place.
Maybe the last sentence of section 2.1 (_|_ Bottom) of "Haskell/Denotational semantics" should be clarified better.
http://en.wikibooks.org/wiki/Haskell/Denotational_semantics#.E2.8A.A5_Bottom
So when trying to use Curry-Howard isomorphism for something in Haskell, one sould be pretty carefull what features of are being used.
Definitely. And that surfaces even in quite innocently looking programs and statements about them. The introductory example of the following technical report may be amusing in that respect: http://wwwtcs.inf.tu-dresden.de/~voigt/TUD-FI08-08.pdf Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de