[Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence

[Stefan Holdermans]

Apfelmus,

> Types like () or Int do not have a logical counterpart in
> propositional logic, although they can be viewed as a constant  
> denoting
> truth. In other words, they may be thought of as being short-hand for
> the type expression (a,a) (where a is a fresh variable).

Could you explain this? I can see () corresponding to True; but  
you're not suggesting that True <=> (a, a), are you?

> System F is closest to Haskell and corresponds to a second order
> intuitionistic propositional logic (?).

Not propositional of course, but second-order indeed.

Cheers,

   Stefan