[Haskell-cafe] forall & ST monad

[Kim-Ee Yeoh]

Wolfgang Jeltsch-2 wrote:
> 
> Am Montag, 16. Februar 2009 19:22 schrieb Wolfgang Jeltsch:
> 
>> First, I thought so too but I changed my mind. To my knowledge a type
>> (forall a. T[a]) -> T' is equivalent to the type exists a. (T[a] -> T').
>> It’s the same as in predicate logic – Curry-Howard in action.
> 
> Oops, this is probably not true. The statement holds for classical
> predicate 
> logic with only non-empty domains.

Here's a counterexample, regardless of whether you're using 
constructive or classical logic, that (forall a. T[a]) -> T' does 
not imply exists a. (T[a] -> T').

Let a not exist, but T' true. Done.

My apologies for not catching this earlier.

-- 
View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22126043.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.