Re: more detailed explanation about forall in Haskell

[Lars Lundgren]

On Fri, 12 May 2000, Jan Brosius wrote:

> >
> > Your example gave the same meaning to `b and forall.
> 
> NOT true : forall works on a proposition and delivers another proposition .
> And this should REMAIN so.
> 
> `b  on the contrary works on a type and delivers a new type.
> 
> Quite different things , I would say.
> 

Curry and Howard showed us that there is an isomorphism between types and
propositions (in intuitionistic logic). That validates the use of forall
in types.

(The isomorphism also covers expressions with a certain type witch
corresponds to constructive proofs of the corresponding formula)

/Lars L