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

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