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