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

[apfelmus]

Stefan Holdermans wrote:
> 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?

Oh, what a mistake .. >< . Of course, a /\ a = a /= True. But there are
real tautologies like (a -> a) that can be used instead. I just wanted
to avoid introducing a primitive constant ⊤ denoting truth when it
already can be expressed in the logic. From now on, let's say ⊤ := (a->a).

What I wanted to say is that the Curry-Howards correspondence of first
order propositional logic does not assign a meaning to types like () or
Int that are not built from type variables and the logical connectives.
But I think it can be adapted to assign them the proposition ⊤. The
translation of lambda-terms to proofs would then replace every primitive
constant like 1 or 2 or () with the proof (id :: ⊤) and eradicate
pattern matches and conditionals. From a computational point of view,
this correspondence is not very interesting then.

Regards,
apfelmus